Actual all-order translation regularity from ordinary square-integrable spatial derivatives.

theorem EulerLpTranslation.derivativeMap_translation {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (D : ↥(L2Space (EulerSmoothLimit.Space →L[ℝ] V))) (a : EulerSmoothLimit.Space) : EulerLpDerivative.derivativeMap MeasureTheory.volume ((translation a) D) = (translation a).toContinuousLinearMap ∘SL EulerLpDerivative.derivativeMap MeasureTheory.volume D

structure EulerLpTranslation.SmoothL2Field (V : Type u) [NormedAddCommGroup V] [NormedSpace ℝ V] : Type u

The hypotheses are ordinary derivatives of a concrete smooth function, not translation-orbit regularity.

• field : EulerSmoothLimit.Space → V

  Underlying field of SmoothL2Field, of type Space → V.

• smooth : ContDiff ℝ (↑⊤) self.field
• integrable (n : ℕ) : MeasureTheory.MemLp (iteratedFDeriv ℝ n self.field) 2 MeasureTheory.volume

theorem EulerLpTranslation.SmoothL2Field.memLp {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) : MeasureTheory.MemLp A.field 2 MeasureTheory.volume

noncomputable def EulerLpTranslation.SmoothL2Field.toLp {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) : ↥(L2Space V)

To Lᵖ, given by A.memLp.toLp A.field.

Equations

• A.toLp = MeasureTheory.MemLp.toLp A.field ⋯

theorem EulerLpTranslation.SmoothL2Field.toLp_ae {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) : ↑↑A.toLp =ᵐ[MeasureTheory.volume] A.field

noncomputable def EulerLpTranslation.SmoothL2Field.jetLp {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) (n : ℕ) : ↥(L2Space (EulerSmoothLimit.Space [×n]→L[ℝ] V))

Jet Lᵖ, given by (A.integrable n).toLp (iteratedFDeriv ℝ n A.field).

Equations

• A.jetLp n = MeasureTheory.MemLp.toLp (iteratedFDeriv ℝ n A.field) ⋯

noncomputable def EulerLpTranslation.SmoothL2Field.derivative {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) : SmoothL2Field (EulerSmoothLimit.Space →L[ℝ] V)

Derivative, bundling field, smooth, integrable.

Equations

• A.derivative = { field := fderiv ℝ A.field, smooth := ⋯, integrable := ⋯ }

theorem EulerLpTranslation.SmoothL2Field.translation_hasFDerivAt {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) (a : EulerSmoothLimit.Space) : HasFDerivAt (fun (b : EulerSmoothLimit.Space) => (translation b) A.toLp) (EulerLpDerivative.derivativeMap MeasureTheory.volume ((translation a) A.derivative.toLp)) a

theorem EulerLpTranslation.SmoothL2Field.translation_fderiv {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) : (fderiv ℝ fun (a : EulerSmoothLimit.Space) => (translation a) A.toLp) = fun (a : EulerSmoothLimit.Space) => (EulerLpDerivative.derivativeBundling MeasureTheory.volume) ((translation a) A.derivative.toLp)

theorem EulerLpTranslation.SmoothL2Field.translation_contDiff {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (translation a) A.toLp

Genuine all-order smoothness of the translation orbit follows from the ordinary spatial L² jets.

theorem EulerLpTranslation.SmoothL2Field.norm_jetLp_zero {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) : ‖A.jetLp 0‖ = ‖A.toLp‖

theorem EulerLpTranslation.SmoothL2Field.norm_derivative_jetLp {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) (n : ℕ) : ‖A.derivative.jetLp n‖ = ‖A.jetLp (n + 1)‖

theorem EulerLpTranslation.SmoothL2Field.norm_iteratedFDeriv_translation_le {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (translation b) A.toLp) a‖ ≤ ‖A.jetLp n‖

Translation jets are controlled with constant one by the actual ordinary spatial L² jets.