Fixed finite-order bounds for genuine ordinary L² derivative words.

theorem EulerOrdinarySobolev.jet_norm_le_word_sum {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerLpTranslation.SmoothL2Field V) (n : ℕ) : ‖A.jetLp n‖ ≤ ∑ w : Fin n → Fin 3, ‖(wordField A w).toLp‖

theorem EulerOrdinarySobolev.wordBound_mono {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {s r : ℕ} {M : ℝ} {A : EulerLpTranslation.SmoothL2Field V} (h : WordBound s M A) (hrs : r ≤ s) : WordBound r M A

theorem EulerOrdinarySobolev.wordBound_nonneg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {s : ℕ} {M : ℝ} {A : EulerLpTranslation.SmoothL2Field V} (h : WordBound s M A) : 0 ≤ M

theorem EulerOrdinarySobolev.wordBound_jet_norm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {s n : ℕ} {M : ℝ} {A : EulerLpTranslation.SmoothL2Field V} (h : WordBound s M A) (hn : n ≤ s) : ‖A.jetLp n‖ ≤ 3 ^ n * M

theorem EulerOrdinarySobolev.wordBound_toLp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {s : ℕ} {M : ℝ} {A : EulerLpTranslation.SmoothL2Field V} (h : WordBound s M A) : ‖A.toLp‖ ≤ M

theorem EulerOrdinarySobolev.wordBound_derivative {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {s : ℕ} {M : ℝ} {A : EulerLpTranslation.SmoothL2Field V} (h : WordBound s M A) (hs : 1 ≤ s) : ‖A.derivative.toLp‖ ≤ 3 * M

theorem EulerOrdinarySobolev.wordBound_map {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {s : ℕ} {M : ℝ} {A : EulerLpTranslation.SmoothL2Field V} (h : WordBound s M A) (L : V →L[ℝ] W) (hL : ‖L‖ ≤ 1) : WordBound s M (EulerLpTranslation.SmoothL2Field.mapField L A)

theorem EulerOrdinarySobolev.field_lpNorm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerLpTranslation.SmoothL2Field V) : MeasureTheory.lpNorm A.field 2 MeasureTheory.volume = ‖A.toLp‖

theorem EulerOrdinarySobolev.real_pointwise_H2 (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : ‖A.field x‖ ≤ EulerSmoothSobolev.smoothEmbeddingConstant * ∑ j ∈ Finset.range 3, ‖A.jetLp j‖

theorem EulerOrdinarySobolev.wordBound_pointwise {M : ℝ} {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (h : WordBound 2 M A) (x : EulerSmoothLimit.Space) : ‖A.field x‖ ≤ 13 * EulerSmoothSobolev.smoothEmbeddingConstant * M

theorem EulerOrdinarySobolev.norm_coordinate_le (i : Fin 3) : ‖EuclideanSpace.proj i‖ ≤ 1

theorem EulerOrdinarySobolev.wordBound_coordinate {s : ℕ} {M : ℝ} {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (h : WordBound s M A) (i : Fin 3) : WordBound s M (EulerLpTranslation.SmoothL2Field.mapField (EuclideanSpace.proj i) A)