Actual finite coordinate derivatives of ordinary smooth L² fields. The word fields retain all genuine L² derivatives; no Sobolev regularity or distributional derivative is postulated.

noncomputable def EulerOrdinarySobolev.axis (i : Fin 3) : EulerSmoothLimit.Space

Axis, given by EuclideanSpace.single i 1.

Equations

• EulerOrdinarySobolev.axis i = EuclideanSpace.single i 1

@[simp]

theorem EulerOrdinarySobolev.axis_norm (i : Fin 3) : ‖axis i‖ = 1

theorem EulerOrdinarySobolev.field_ext {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {A B : EulerLpTranslation.SmoothL2Field V} (h : A.field = B.field) : A = B

def EulerOrdinarySobolev.wordField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerLpTranslation.SmoothL2Field V) {n : ℕ} : (Fin n → Fin 3) → EulerLpTranslation.SmoothL2Field V

Word field as an element of {n : ℕ} → (Fin n → Fin 3) → SmoothL2Field V | 0, _ => A | _+1, w => (wordField A (Fin.tail w)).directionalField (axis (w 0)).

Equations

• EulerOrdinarySobolev.wordField A x_2 = A
• EulerOrdinarySobolev.wordField A w = (EulerOrdinarySobolev.wordField A (Fin.tail w)).directionalField (EulerOrdinarySobolev.axis (w 0))

@[simp]

theorem EulerOrdinarySobolev.wordField_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerLpTranslation.SmoothL2Field V) (w : Fin 0 → Fin 3) : wordField A w = A

@[simp]

theorem EulerOrdinarySobolev.wordField_cons {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerLpTranslation.SmoothL2Field V) {n : ℕ} (w : Fin n → Fin 3) (i : Fin 3) : wordField A (Fin.cons i w) = (wordField A w).directionalField (axis i)

theorem EulerOrdinarySobolev.wordField_field {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerLpTranslation.SmoothL2Field V) {n : ℕ} (w : Fin n → Fin 3) : (wordField A w).field = EulerParameterWordGevrey.wordDerivative axis A.field w

theorem EulerOrdinarySobolev.wordField_snoc {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerLpTranslation.SmoothL2Field V) {n : ℕ} (w : Fin n → Fin 3) (i : Fin 3) : wordField A (Fin.snoc w i) = wordField (A.directionalField (axis i)) w

theorem EulerOrdinarySobolev.wordField_map {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) (A : EulerLpTranslation.SmoothL2Field V) {n : ℕ} (w : Fin n → Fin 3) : wordField (EulerLpTranslation.SmoothL2Field.mapField L A) w = EulerLpTranslation.SmoothL2Field.mapField L (wordField A w)

theorem EulerOrdinarySobolev.wordField_add {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A B : EulerLpTranslation.SmoothL2Field V) {n : ℕ} (w : Fin n → Fin 3) : wordField (A.addField B) w = (wordField A w).addField (wordField B w)

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

noncomputable def EulerOrdinarySobolev.wordSize {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (s : ℕ) (A : EulerLpTranslation.SmoothL2Field V) : ℝ

Word size, given by ∑ n ∈ range (s+1), ∑ w : Fin n → Fin 3, ‖(wordField A w).toLp‖.

Equations

• EulerOrdinarySobolev.wordSize s A = ∑ n ∈ Finset.range (s + 1), ∑ w : Fin n → Fin 3, ‖(EulerOrdinarySobolev.wordField A w).toLp‖

noncomputable def EulerOrdinarySobolev.wordEnergy {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (s : ℕ) (A : EulerLpTranslation.SmoothL2Field V) : ℝ

Word energy, given by ∑ n ∈ range (s+1), ∑ w : Fin n → Fin 3, ‖(wordField A w).toLp‖^2.

Equations

• EulerOrdinarySobolev.wordEnergy s A = ∑ n ∈ Finset.range (s + 1), ∑ w : Fin n → Fin 3, ‖(EulerOrdinarySobolev.wordField A w).toLp‖ ^ 2

def EulerOrdinarySobolev.WordBound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (s : ℕ) (M : ℝ) (A : EulerLpTranslation.SmoothL2Field V) : Prop

Word bound, given by ∀ n ≤ s, ∀ w : Fin n → Fin 3, ‖(wordField A w).toLp‖ ≤ M.

Equations

• EulerOrdinarySobolev.WordBound s M A = ∀ n ≤ s, ∀ (w : Fin n → Fin 3), ‖(EulerOrdinarySobolev.wordField A w).toLp‖ ≤ M

theorem EulerOrdinarySobolev.wordEnergy_nonneg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (s : ℕ) (A : EulerLpTranslation.SmoothL2Field V) : 0 ≤ wordEnergy s A

theorem EulerOrdinarySobolev.word_norm_sq_le_energy {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerLpTranslation.SmoothL2Field V) {n s : ℕ} (hn : n ≤ s) (w : Fin n → Fin 3) : ‖(wordField A w).toLp‖ ^ 2 ≤ wordEnergy s A

theorem EulerOrdinarySobolev.wordBound_sqrt_energy {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (s : ℕ) (A : EulerLpTranslation.SmoothL2Field V) : WordBound s (√(wordEnergy s A)) A

theorem EulerOrdinarySobolev.wordBound_wordField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {s k : ℕ} {M : ℝ} {A : EulerLpTranslation.SmoothL2Field V} (h : WordBound (k + s) M A) (w : Fin k → Fin 3) : WordBound s M (wordField A w)

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

theorem EulerOrdinarySobolev.mapField_norm_le {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) (A : EulerLpTranslation.SmoothL2Field V) : ‖(EulerLpTranslation.SmoothL2Field.mapField L A).toLp‖ ≤ ‖L‖ * ‖A.toLp‖