Tame products of genuine ordinary derivatives. The low norm is H³ and the high norm has any integer order at least three. The only interpolation input is the integration-by-parts theorem in OrdinaryWordInterpolation.

noncomputable def EulerOrdinarySobolev.wordPointBound (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (k : ℕ) : ℝ

Word point bound, given by smoothEmbeddingConstant*(∑ j ∈ range 3, (3 : ℝ)^j*wordMaximum (k+j) A).

Equations

• EulerOrdinarySobolev.wordPointBound A k = EulerSmoothSobolev.smoothEmbeddingConstant * ∑ j ∈ Finset.range 3, 3 ^ j * EulerOrdinarySobolev.wordMaximum (k + j) A

theorem EulerOrdinarySobolev.wordPointBound_nonneg (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (k : ℕ) : 0 ≤ wordPointBound A k

theorem EulerOrdinarySobolev.wordPointBound_product (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (m : ℕ) (M N : ℝ) (hM : WordBound 3 M A) (hN : WordBound m N A) {a b : ℕ} (ha : a + 2 ≤ m) (hb : b ≤ m) (hab : a + b ≤ m + 1) : wordPointBound A a * wordMaximum b A ≤ 13 * EulerSmoothSobolev.smoothEmbeddingConstant * M * N

theorem EulerOrdinarySobolev.coordinateProduct_word_left (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) {k l : ℕ} (w : Fin k → Fin 3) (v : Fin l → Fin 3) (i : Fin 3) : ‖(coordinateProduct i (wordField A w) (wordField A v)).toLp‖ ≤ wordPointBound A k * wordMaximum l A

theorem EulerOrdinarySobolev.coordinateProduct_word_right (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) {k l : ℕ} (w : Fin k → Fin 3) (v : Fin l → Fin 3) (i : Fin 3) : ‖(coordinateProduct i (wordField A w) (wordField A v)).toLp‖ ≤ wordPointBound A l * wordMaximum k A

theorem EulerOrdinarySobolev.coordinateProduct_tame (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (m : ℕ) (hm : 3 ≤ m) (M N : ℝ) (hM : WordBound 3 M A) (hN : WordBound m N A) {k l : ℕ} (hk : 1 ≤ k) (hl : 1 ≤ l) (hkl : k + l ≤ m + 1) (w : Fin k → Fin 3) (v : Fin l → Fin 3) (i : Fin 3) : ‖(coordinateProduct i (wordField A w) (wordField A v)).toLp‖ ≤ h3ProductConstant * M * N

theorem EulerOrdinarySobolev.tame_outer_product (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) (hl : 1 ≤ l) (horder : n + k + l ≤ m + 1) (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 A v)) a).toLp‖ ≤ 2 ^ n * h3ProductConstant * M * N