The middle H³ product uses genuine H¹×H¹→L². All other distributions use H² point evaluation. The constant is independent of the fields and contains no fourth derivative of either H³ argument.

noncomputable def EulerOrdinarySobolev.h3ProductConstant : ℝ

H3 product constant, given by 1+13*smoothEmbeddingConstant+4*(1+3*(sobolevConstant : ℝ))^2.

Equations

• EulerOrdinarySobolev.h3ProductConstant = 1 + 13 * EulerSmoothSobolev.smoothEmbeddingConstant + 4 * (1 + 3 * ↑EulerMeanCutoffCurl.sobolevConstant) ^ 2

theorem EulerOrdinarySobolev.h3ProductConstant_nonneg : 0 ≤ h3ProductConstant

theorem EulerOrdinarySobolev.h3ProductConstant_left : 13 * EulerSmoothSobolev.smoothEmbeddingConstant ≤ h3ProductConstant

theorem EulerOrdinarySobolev.h3ProductConstant_middle : 4 * (1 + 3 * ↑EulerMeanCutoffCurl.sobolevConstant) ^ 2 ≤ h3ProductConstant

theorem EulerOrdinarySobolev.scalarProduct_h1_bound (A : EulerLpTranslation.SmoothL2Field ℝ) (B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : ‖(scalarProduct A B).toLp‖ ≤ 4 * (‖A.toLp‖ + ↑EulerMeanCutoffCurl.sobolevConstant * ‖A.derivative.toLp‖) * (‖B.toLp‖ + ↑EulerMeanCutoffCurl.sobolevConstant * ‖B.derivative.toLp‖)

theorem EulerOrdinarySobolev.coordinateProduct_h2_left (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (M N : ℝ) (hA : WordBound 2 M A) (hB : WordBound 0 N B) (i : Fin 3) : ‖(coordinateProduct i A B).toLp‖ ≤ h3ProductConstant * M * N

theorem EulerOrdinarySobolev.coordinateProduct_h2_right (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (M N : ℝ) (hA : WordBound 0 M A) (hB : WordBound 2 N B) (i : Fin 3) : ‖(coordinateProduct i A B).toLp‖ ≤ h3ProductConstant * M * N

theorem EulerOrdinarySobolev.coordinateProduct_h1 (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (M N : ℝ) (hA : WordBound 1 M A) (hB : WordBound 1 N B) (i : Fin 3) : ‖(coordinateProduct i A B).toLp‖ ≤ h3ProductConstant * M * N

theorem EulerOrdinarySobolev.coordinateProduct_mixed (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (M N : ℝ) {s t k l : ℕ} (hA : WordBound s M A) (hB : WordBound t N B) (w : Fin k → Fin 3) (v : Fin l → Fin 3) (i : Fin 3) (hmargin : k + 2 ≤ s ∧ l ≤ t ∨ k ≤ s ∧ l + 2 ≤ t ∨ k + 1 ≤ s ∧ l + 1 ≤ t) : ‖(coordinateProduct i (wordField A w) (wordField B v)).toLp‖ ≤ h3ProductConstant * M * N

theorem EulerOrdinarySobolev.coordinateProduct_directional (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (i j : Fin 3) : (coordinateProduct i A B).directionalField (axis j) = (coordinateProduct i (A.directionalField (axis j)) B).addField (coordinateProduct i A (B.directionalField (axis j)))

theorem EulerOrdinarySobolev.word_coordinateProduct_recurrence (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) {n k l : ℕ} (a : Fin (n + 1) → Fin 3) (w : Fin k → Fin 3) (v : Fin l → Fin 3) (i : Fin 3) : wordField (coordinateProduct i (wordField A w) (wordField B v)) a = (wordField (coordinateProduct i (wordField A (Fin.cons (a (Fin.last n)) w)) (wordField B v)) (Fin.init a)).addField (wordField (coordinateProduct i (wordField A w) (wordField B (Fin.cons (a (Fin.last n)) v))) (Fin.init a))

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

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