The genuine spatial H³ difference-energy estimate for ordinary Euler. The pressure term vanishes exactly. The constant uses only the reference H⁴ norm and the H³ norm of the difference.

theorem EulerOrdinarySobolev.wordField_neg (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) {n : ℕ} (w : Fin n → Fin 3) : wordField (fieldNeg A) w = fieldNeg (wordField A w)

theorem EulerOrdinarySobolev.wordBound_add {s : ℕ} {M N : ℝ} {A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (hA : WordBound s M A) (hB : WordBound s N B) : WordBound s (M + N) (A.addField B)

noncomputable def EulerOrdinarySobolev.differenceRhs (U W P : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Difference rhs, given by fieldNeg (addField (addField (advectionField (addField U W) W) (advectionField W U)) P).

Equations

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

theorem EulerOrdinarySobolev.differenceRhs_field (U W P : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : (differenceRhs U W P).field x = -(fderiv ℝ W.field x) (U.field x + W.field x) - (fderiv ℝ U.field x) (W.field x) - P.field x

theorem EulerOrdinarySobolev.differenceRhs_pairing (U W P : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence (U.addField W).field x = 0) (hW : W.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) (hP : P.toLp ∈ EulerMeanSolenoidal.gradientSpace) {n : ℕ} (w : Fin n → Fin 3) : inner ℝ (wordField W w).toLp (wordField (differenceRhs U W P) w).toLp = -inner ℝ (transportCommutator (U.addField W) W w).toLp (wordField W w).toLp - inner ℝ (wordField (advectionField W U) w).toLp (wordField W w).toLp

theorem EulerOrdinarySobolev.differenceRhs_word_bound (U W P : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (M X : ℝ) (hU : WordBound 4 M U) (hWb : WordBound 3 X W) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence (U.addField W).field x = 0) (hW : W.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) (hP : P.toLp ∈ EulerMeanSolenoidal.gradientSpace) {n : ℕ} (hn : n ≤ 3) (w : Fin n → Fin 3) : inner ℝ (wordField W w).toLp (wordField (differenceRhs U W P) w).toLp ≤ 45 * h3ProductConstant * (M + X) * X ^ 2

noncomputable def EulerOrdinarySobolev.energyProduction (W Q : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : ℝ

Energy production, given by 2*(∑ n ∈ range 4, ∑ w : Fin n → Fin 3, ⟪(wordField W w).toLp,(wordField Q w).toLp⟫_ℝ).

Equations

• EulerOrdinarySobolev.energyProduction W Q = 2 * ∑ n ∈ Finset.range 4, ∑ w : Fin n → Fin 3, inner ℝ (EulerOrdinarySobolev.wordField W w).toLp (EulerOrdinarySobolev.wordField Q w).toLp

theorem EulerOrdinarySobolev.difference_energy_bound (U W P : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (M : ℝ) (hU : WordBound 4 M U) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence (U.addField W).field x = 0) (hW : W.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) (hP : P.toLp ∈ EulerMeanSolenoidal.gradientSpace) : energyProduction W (differenceRhs U W P) ≤ 3600 * h3ProductConstant * (M + √(wordEnergy 3 W)) * wordEnergy 3 W