Genuine L² interpolation of ordinary derivative words. Integration by parts gives log-convexity of the largest norm at each order. This yields endpoint product estimates without a change of Sobolev order.

noncomputable def EulerOrdinarySobolev.wordMaximum (n : ℕ) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : ℝ

Word maximum, given by (univ : Finset (Fin n → Fin 3)).sup' univ_nonempty (fun w => ‖(wordField A w).toLp‖).

Equations

• EulerOrdinarySobolev.wordMaximum n A = Finset.univ.sup' ⋯ fun (w : Fin n → Fin 3) => ‖(EulerOrdinarySobolev.wordField A w).toLp‖

theorem EulerOrdinarySobolev.word_norm_le_maximum (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) {n : ℕ} (w : Fin n → Fin 3) : ‖(wordField A w).toLp‖ ≤ wordMaximum n A

theorem EulerOrdinarySobolev.wordMaximum_nonneg (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (n : ℕ) : 0 ≤ wordMaximum n A

theorem EulerOrdinarySobolev.wordMaximum_le {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} {s n : ℕ} {M : ℝ} (h : WordBound s M A) (hn : n ≤ s) : wordMaximum n A ≤ M

theorem EulerOrdinarySobolev.wordMaximum_logconvex (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (n : ℕ) : wordMaximum (n + 1) A ^ 2 ≤ wordMaximum n A * wordMaximum (n + 2) A

theorem EulerOrdinarySobolev.wordMaximum_product_le (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (m : ℕ) (M N : ℝ) (hM : WordBound 3 M A) (hN : WordBound m N A) {a b : ℕ} (ha : a ≤ m) (hb : b ≤ m) (hab : a + b ≤ m + 3) : wordMaximum a A * wordMaximum b A ≤ M * N

theorem EulerOrdinarySobolev.wordMaximum_directional (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (n : ℕ) (i : Fin 3) : wordMaximum n (A.directionalField (axis i)) ≤ wordMaximum (n + 1) A

theorem EulerOrdinarySobolev.wordMaximum_wordField (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) {k : ℕ} (w : Fin k → Fin 3) (n : ℕ) : wordMaximum n (wordField A w) ≤ wordMaximum (n + k) A

theorem EulerOrdinarySobolev.jet_norm_le_wordMaximum (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (n : ℕ) : ‖A.jetLp n‖ ≤ 3 ^ n * wordMaximum n A

theorem EulerOrdinarySobolev.wordField_jet_maximum (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) {k : ℕ} (w : Fin k → Fin 3) (n : ℕ) : ‖(wordField A w).jetLp n‖ ≤ 3 ^ n * wordMaximum (k + n) A

theorem EulerOrdinarySobolev.wordField_pointwise_maximum (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) {k : ℕ} (w : Fin k → Fin 3) (x : EulerSmoothLimit.Space) : ‖(wordField A w).field x‖ ≤ EulerSmoothSobolev.smoothEmbeddingConstant * ∑ j ∈ Finset.range 3, 3 ^ j * wordMaximum (k + j) A