Genuine classical spatial words have exactly the strong L² word norms

Each derivative of the canonical smooth representative is identified with the corresponding actual L² translation derivative. Consequently finite Hq sums and external ordered-word sums transfer with constant one, including uniform time evaluation. There is no tensor-to-word radius conversion.

Strong ordinary L² spatial derivatives are the classical derivatives of the reconstructed field.

theorem EulerMeanSmoothRepresentative.representative_pointwise_translation_hasDerivAt (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) (v x : EulerSmoothLimit.Space) : HasDerivAt (fun (t : ℝ) => representative u hu (x + t • v)) ((fderiv ℝ (representative u hu) x) v) 0

theorem EulerMeanSmoothRepresentative.orbitDerivative_ae_fderiv (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) (v : EulerSmoothLimit.Space) : ↑↑(orbitDerivative u v) =ᵐ[MeasureTheory.volume] fun (x : EulerSmoothLimit.Space) => (fderiv ℝ (representative u hu) x) v

No prior L² integrability of the classical derivative is assumed.

theorem EulerMeanSmoothRepresentative.fderiv_representative_apply (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) (v x : EulerSmoothLimit.Space) : (fderiv ℝ (representative u hu) x) v = representative (orbitDerivative u v) ⋯ x

The classical directional derivative is exactly the reconstructed strong derivative.

theorem EulerMeanSmoothRepresentative.representative_directional_memLp (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) (v : EulerSmoothLimit.Space) : MeasureTheory.MemLp (fun (x : EulerSmoothLimit.Space) => (fderiv ℝ (representative u hu) x) v) 2 MeasureTheory.volume

theorem EulerMeanSmoothRepresentative.representative_fderiv_memLp (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) : MeasureTheory.MemLp (fderiv ℝ (representative u hu)) 2 MeasureTheory.volume

The full classical first derivative is genuinely square-integrable.

noncomputable def EulerMeanClassicalWordBounds.ordinaryWord {ι : Type u_1} (directions : ι → EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.L2) {n : ℕ} (w : Fin n → ι) : ↥EulerMeanSolenoidal.L2

The actual strong L² spatial derivative for an ordered word.

Equations

• EulerMeanClassicalWordBounds.ordinaryWord directions u w = EulerParameterWordGevrey.wordDerivative directions (fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) u) w 0

@[simp]

theorem EulerMeanClassicalWordBounds.ordinaryWord_zero {ι : Type u_1} (directions : ι → EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.L2) (w : Fin 0 → ι) : ordinaryWord directions u w = u

theorem EulerMeanClassicalWordBounds.ordinaryWord_snoc {ι : Type u_1} (directions : ι → EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) {n : ℕ} (w : Fin n → ι) (i : ι) : ordinaryWord directions u (Fin.snoc w i) = ordinaryWord directions (EulerMeanSmoothRepresentative.orbitDerivative u (directions i)) w

Adding a last direction is the genuine strong directional derivative.

theorem EulerMeanClassicalWordBounds.ordinaryWord_translation {ι : Type u_1} (directions : ι → EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) {n : ℕ} (w : Fin n → ι) (a : EulerSmoothLimit.Space) : (EulerMeanSolenoidal.translation a) (ordinaryWord directions u w) = EulerParameterWordGevrey.wordDerivative directions (fun (b : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation b) u) w a

The translated strong word is the same actual word at any base point.

theorem EulerMeanClassicalWordBounds.ordinaryWord_smooth {ι : Type u_1} (directions : ι → EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) {n : ℕ} (w : Fin n → ι) : EulerMeanSmoothRepresentative.SmoothOrbit (ordinaryWord directions u w)

Every strong word itself has the genuine smooth spatial orbit.

theorem EulerMeanClassicalWordBounds.representative_congr {u v : ↥EulerMeanSolenoidal.L2} (h : u = v) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) (hv : EulerMeanSmoothRepresentative.SmoothOrbit v) : EulerMeanSmoothRepresentative.representative u hu = EulerMeanSmoothRepresentative.representative v hv

theorem EulerMeanClassicalWordBounds.representative_word {ι : Type u_1} (directions : ι → EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) {n : ℕ} (w : Fin n → ι) (x : EulerSmoothLimit.Space) : EulerParameterWordGevrey.wordDerivative directions (EulerMeanSmoothRepresentative.representative u hu) w x = EulerMeanSmoothRepresentative.representative (ordinaryWord directions u w) ⋯ x

Pointwise equality between the actual classical derivative word and the canonical representative of the corresponding genuine strong L² derivative.

theorem EulerMeanClassicalWordBounds.ordinaryWord_ae {ι : Type u_1} (directions : ι → EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) {n : ℕ} (w : Fin n → ι) : ↑↑(ordinaryWord directions u w) =ᵐ[MeasureTheory.volume] EulerParameterWordGevrey.wordDerivative directions (EulerMeanSmoothRepresentative.representative u hu) w

No integrability of classical derivatives is assumed: it follows from the solved field's genuine smooth L² orbit.

theorem EulerMeanClassicalWordBounds.classicalWord_memLp {ι : Type u_1} (directions : ι → EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) {n : ℕ} (w : Fin n → ι) : MeasureTheory.MemLp (EulerParameterWordGevrey.wordDerivative directions (EulerMeanSmoothRepresentative.representative u hu) w) 2 MeasureTheory.volume

noncomputable def EulerMeanClassicalWordBounds.classicalWordLp {ι : Type u_1} (directions : ι → EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) {n : ℕ} (w : Fin n → ι) : ↥EulerMeanSolenoidal.L2

The L² class of the literal classical derivative of the smooth representative.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem EulerMeanClassicalWordBounds.classicalWordLp_eq {ι : Type u_1} (directions : ι → EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) {n : ℕ} (w : Fin n → ι) : classicalWordLp directions u hu w = ordinaryWord directions u w

noncomputable def EulerMeanClassicalWordBounds.classicalBaseSize {ι : Type u_1} [Fintype ι] (directions : ι → EulerSmoothLimit.Space) (q : ℕ) (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) : ℝ

The finite sum definition of the actual classical Hq seminorms.

Equations

• EulerMeanClassicalWordBounds.classicalBaseSize directions q u hu = ∑ k ∈ Finset.range (q + 1), ∑ w : Fin k → ι, ‖EulerMeanClassicalWordBounds.classicalWordLp directions u hu w‖

theorem EulerMeanClassicalWordBounds.classicalBaseSize_eq {ι : Type u_1} [Fintype ι] (directions : ι → EulerSmoothLimit.Space) (q : ℕ) (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) : classicalBaseSize directions q u hu = EulerParameterWordGevrey.baseSize directions q (fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) u) 0

noncomputable def EulerMeanClassicalWordBounds.classicalBlockSize {ι : Type u_1} [Fintype ι] (directions : ι → EulerSmoothLimit.Space) (q : ℕ) (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) (n : ℕ) : ℝ

Sum of actual classical Hq sizes of the external derivative fields. representative_word identifies those fields with derivatives of the original representative.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerMeanClassicalWordBounds.classicalBlockSize_eq {ι : Type u_1} [Fintype ι] (directions : ι → EulerSmoothLimit.Space) (q : ℕ) (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) (n : ℕ) : classicalBlockSize directions q u hu n = EulerParameterWordGevrey.block directions q (fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) u) n 0

Exact identification with the blocks used by the genuine inverse estimate.

theorem EulerMeanClassicalWordBounds.path_classicalBlockSize_le {ι : Type u_1} [Fintype ι] (directions : ι → EulerSmoothLimit.Space) (q : ℕ) (T : ℝ) (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) (t : ↑(Set.Icc 0 T)) (n : ℕ) : classicalBlockSize directions q (p t) ⋯ n ≤ EulerParameterWordGevrey.block directions q (fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) n 0

Uniform time evaluation transfers all genuine classical Hq derivative words with constant one, and without a radius change.