The actual ordinary H³ transport commutator, without derivative loss.

theorem EulerOrdinarySobolev.advection_directional (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (v : EulerSmoothLimit.Space) : (advectionField A B).directionalField v = (advectionField A (B.directionalField v)).addField (advectionField (A.directionalField v) B)

noncomputable def EulerOrdinarySobolev.transportCommutator (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) {n : ℕ} (w : Fin n → Fin 3) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Transport commutator, given by fieldSub (wordField (advectionField A B) w) (advectionField A (wordField B w)).

Equations

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

theorem EulerOrdinarySobolev.transportCommutator_zero (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (w : Fin 0 → Fin 3) : (transportCommutator A B w).toLp = 0

theorem EulerOrdinarySobolev.transportCommutator_snoc (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) {n : ℕ} (w : Fin n → Fin 3) (j : Fin 3) : transportCommutator A B (Fin.snoc w j) = (wordField (advectionField (A.directionalField (axis j)) B) w).addField (transportCommutator A (B.directionalField (axis j)) w)

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

theorem EulerOrdinarySobolev.source_advection_outer (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (M N : ℝ) (hA : WordBound 3 M A) (hB : WordBound 4 N B) {n : ℕ} (hn : n ≤ 3) (a : Fin n → Fin 3) : ‖(wordField (advectionField A B) a).toLp‖ ≤ 3 * 2 ^ n * h3ProductConstant * M * N

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

theorem EulerOrdinarySobolev.transportCommutator_bound (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (M N : ℝ) (hA : WordBound 3 M A) (hB : WordBound 3 N B) {n : ℕ} (hn : n ≤ 3) (w : Fin n → Fin 3) : ‖(transportCommutator A B w).toLp‖ ≤ 3 * (2 ^ n - 1) * h3ProductConstant * M * N