Positive external-order commutators in actual fixed-order Sobolev blocks.

def EulerH6Pressure.zeroJet (period : ℝ) [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} (q : ℕ) : EulerSpatialSobolevInverse.SpatialJet period directions q 0

The zero field has a genuine strong Sobolev jet at every finite order.

Equations

• EulerH6Pressure.zeroJet period 0 = EulerSpatialSobolevInverse.SpatialJet.zero 0
• EulerH6Pressure.zeroJet period q.succ = EulerSpatialSobolevInverse.SpatialJet.succ (fun (x : Fin 4) => 0) (fun (x : Fin 4) => EulerH6Pressure.zeroJet period q) ⋯

theorem EulerH6Pressure.zeroJet_norm (period : ℝ) [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} (q : ℕ) : (zeroJet period q).sobolevNorm = 0

@[simp]

theorem EulerH6Pressure.sobolevSize_zero (period : ℝ) [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} (q : ℕ) : sobolevSize period q 0 = 0

noncomputable def EulerH6Pressure.commutatorJet {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s q n : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period directions s A) (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (w : Fin n → Fin 4) (h : n + q ≤ s) : EulerSpatialSobolevInverse.SpatialJet period directions q ((EulerSpatialSobolevInverse.SpatialJet.multiply K J).word w - A.operator (J.word w))

An actual base-order Sobolev jet for the external product commutator.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerH6Pressure.commutatorBlock {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period directions s A) (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (q n : ℕ) : ℝ

Sum of the actual base Sobolev norms of the external product commutators.

Equations

• EulerH6Pressure.commutatorBlock K J q n = ∑ w : Fin n → Fin 4, EulerH6Pressure.sobolevSize period q ((EulerSpatialSobolevInverse.SpatialJet.multiply K J).word w - A.operator (J.word w))

theorem EulerH6Pressure.commutatorBlock_zero {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period directions s A) (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) : commutatorBlock K J q 0 = 0

theorem EulerH6Pressure.commutatorBlock_nonneg {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s q n : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period directions s A) (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) : 0 ≤ commutatorBlock K J q n

theorem EulerH6Pressure.commutatorBlock_truncate {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s q n : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period directions (s + 1) A) (J : EulerSpatialSobolevInverse.SpatialJet period directions (s + 1) f) (h : n ≤ s) : commutatorBlock K.truncate J.truncate q n = commutatorBlock K J q n

Truncation preserves every valid external commutator as an actual L² field.

theorem EulerH6Pressure.commutatorBlock_succ_le {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s q n : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period directions (s + 1) A) (J : EulerSpatialSobolevInverse.SpatialJet period directions (s + 1) f) (h : n + q ≤ s) : commutatorBlock K J q (n + 1) ≤ match K, J with | EulerSpatialSobolevInverse.CoefficientJet.succ derivatives lowerA derivative_eq, EulerSpatialSobolevInverse.SpatialJet.succ derivatives_1 lowerF hasDeriv => ∑ i : Fin 4, (commutatorBlock K.truncate (lowerF i) q n + blockNorm period (EulerSpatialSobolevInverse.SpatialJet.multiply (lowerA i) J.truncate) q n)

The external commutator recurrence uses a fixed Sobolev norm at every leaf.

theorem EulerH6Pressure.commutatorBlock_bound {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s q n : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period directions s A) (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (h : n + q ≤ s) : commutatorBlock K J q n ≤ EulerJetProductBounds.commutatorConvolution (coefficientBlock period K q) (blockNorm period J q) n

The complete external commutator estimate has only positive coefficient derivative orders.