Integer-order Euler transport energy with a genuine H³ coefficient. The pressure and top transport term cancel. All remaining products are controlled by the proved L² interpolation of derivative words.

theorem EulerOrdinarySobolev.tame_advection_outer (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (m : ℕ) (hm : 3 ≤ m) (M N : ℝ) (hM : WordBound 3 M A) (hN : WordBound m N A) {n k l : ℕ} (hk : 1 ≤ k) (horder : n + k + l ≤ m) (a : Fin n → Fin 3) (w : Fin k → Fin 3) (v : Fin l → Fin 3) : ‖(wordField (advectionField (wordField A w) (wordField A v)) a).toLp‖ ≤ 3 * 2 ^ n * h3ProductConstant * M * N

theorem EulerOrdinarySobolev.tame_transportCommutator_word (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (m : ℕ) (hm : 3 ≤ m) (M N : ℝ) (hM : WordBound 3 M A) (hN : WordBound m N A) {n l : ℕ} (horder : n + l ≤ m) (a : Fin n → Fin 3) (v : Fin l → Fin 3) : ‖(transportCommutator A (wordField A v) a).toLp‖ ≤ 3 * (2 ^ n - 1) * h3ProductConstant * M * N

theorem EulerOrdinarySobolev.tame_transportCommutator (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (m : ℕ) (hm : 3 ≤ m) (M N : ℝ) (hM : WordBound 3 M A) (hN : WordBound m N A) {n : ℕ} (hn : n ≤ m) (w : Fin n → Fin 3) : ‖(transportCommutator A A w).toLp‖ ≤ 3 * (2 ^ n - 1) * h3ProductConstant * M * N

noncomputable def EulerOrdinarySobolev.eulerRhs (A P : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Euler rhs, given by fieldNeg (addField (advectionField A A) P).

Equations

• EulerOrdinarySobolev.eulerRhs A P = EulerOrdinarySobolev.fieldNeg ((EulerOrdinarySobolev.advectionField A A).addField P)

theorem EulerOrdinarySobolev.eulerRhs_field (A P : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : (eulerRhs A P).field x = -(fderiv ℝ A.field x) (A.field x) - P.field x

theorem EulerOrdinarySobolev.eulerRhs_pairing (A P : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence A.field x = 0) (hA : A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) (hP : P.toLp ∈ EulerMeanSolenoidal.gradientSpace) {n : ℕ} (w : Fin n → Fin 3) : inner ℝ (wordField A w).toLp (wordField (eulerRhs A P) w).toLp = -inner ℝ (transportCommutator A A w).toLp (wordField A w).toLp

noncomputable def EulerOrdinarySobolev.tameEnergyConstant (m : ℕ) : ℝ

Tame energy constant, given by 6*h3ProductConstant*(∑ n ∈ range (m+1), (6 : ℝ)^n).

Equations

• EulerOrdinarySobolev.tameEnergyConstant m = 6 * EulerOrdinarySobolev.h3ProductConstant * ∑ n ∈ Finset.range (m + 1), 6 ^ n

theorem EulerOrdinarySobolev.tameEnergyConstant_nonneg (m : ℕ) : 0 ≤ tameEnergyConstant m

noncomputable def EulerOrdinarySobolev.integerEnergyProduction (m : ℕ) (A Q : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : ℝ

Integer energy production, given by 2*(∑ n ∈ range (m+1), ∑ w : Fin n → Fin 3, ⟪(wordField A w).toLp,(wordField Q w).toLp⟫_ℝ).

Equations

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

theorem EulerOrdinarySobolev.eulerRhs_word_tame (A P : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (m : ℕ) (hm : 3 ≤ m) (M : ℝ) (hM : WordBound 3 M A) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence A.field x = 0) (hA : A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) (hP : P.toLp ∈ EulerMeanSolenoidal.gradientSpace) {n : ℕ} (hn : n ≤ m) (w : Fin n → Fin 3) : inner ℝ (wordField A w).toLp (wordField (eulerRhs A P) w).toLp ≤ 3 * 2 ^ n * h3ProductConstant * M * wordEnergy m A

theorem EulerOrdinarySobolev.integer_energy_tame (A P : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (m : ℕ) (hm : 3 ≤ m) (M : ℝ) (hM : WordBound 3 M A) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence A.field x = 0) (hA : A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) (hP : P.toLp ∈ EulerMeanSolenoidal.gradientSpace) : integerEnergyProduction m A (eulerRhs A P) ≤ tameEnergyConstant m * M * wordEnergy m A