Compact approximation proves actual translation differentiability for noncompact smooth L² fields.

The genuine L² derivative of translations of compact smooth ordinary-space fields.

noncomputable def EulerLpTranslation.compactField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hc : HasCompactSupport f) (hf : ContDiff ℝ (↑⊤) f) : ↥(L2Space V)

Compact field, given by (hf.continuous.memLp_of_hasCompactSupport hc).toLp f.

Equations

• EulerLpTranslation.compactField f hc hf = MeasureTheory.MemLp.toLp f ⋯

noncomputable def EulerLpTranslation.compactDerivative {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hc : HasCompactSupport f) (hf : ContDiff ℝ (↑⊤) f) : ↥(L2Space (EulerSmoothLimit.Space →L[ℝ] V))

Compact derivative, given by ((hf.fderiv_right (m := ∞) (by simp)).continuous.memLp_of_hasCompactSupport (hc.fderiv ℝ)).toLp (fderiv ℝ f).

Equations

• EulerLpTranslation.compactDerivative f hc hf = MeasureTheory.MemLp.toLp (fderiv ℝ f) ⋯

theorem EulerLpTranslation.compactField_ae {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hc : HasCompactSupport f) (hf : ContDiff ℝ (↑⊤) f) : ↑↑(compactField f hc hf) =ᵐ[MeasureTheory.volume] f

theorem EulerLpTranslation.compactDerivative_ae {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hc : HasCompactSupport f) (hf : ContDiff ℝ (↑⊤) f) : ↑↑(compactDerivative f hc hf) =ᵐ[MeasureTheory.volume] fderiv ℝ f

theorem EulerLpTranslation.compact_increment_bound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hc : HasCompactSupport f) (hf : ContDiff ℝ (↑⊤) f) : ∃ (M : EulerSmoothLimit.Space → ℝ), MeasureTheory.MemLp M 2 MeasureTheory.volume ∧ (∀ (x : EulerSmoothLimit.Space), 0 ≤ M x) ∧ ∀ (a : EulerSmoothLimit.Space), ‖a‖ ≤ 1 → ∀ (x : EulerSmoothLimit.Space), ‖f (x + a) - f x‖ ≤ M x * ‖a‖

A single compactly supported L² function dominates every small translation increment.

theorem EulerLpTranslation.compactField_hasFDerivAt {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hc : HasCompactSupport f) (hf : ContDiff ℝ (↑⊤) f) : HasFDerivAt (fun (a : EulerSmoothLimit.Space) => (translation a) (compactField f hc hf)) (EulerLpDerivative.derivativeMap MeasureTheory.volume (compactDerivative f hc hf)) 0

Ordinary Fréchet differentiation and L² translation differentiation agree on compact smooth fields.

noncomputable def EulerLpTranslation.cutoffLp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) : ↥(L2Space V)

Cutoff Lᵖ, given by compactField (cutoffField f n) (cutoffField_compact f n) (cutoffField_smooth f hf n).

Equations

• EulerLpTranslation.cutoffLp f hf n = EulerLpTranslation.compactField (EulerLpTranslation.cutoffField f n) ⋯ ⋯

noncomputable def EulerLpTranslation.cutoffDerivativeLp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) : ↥(L2Space (EulerSmoothLimit.Space →L[ℝ] V))

Cutoff derivative Lᵖ, given by compactDerivative (cutoffField f n) (cutoffField_compact f n) (cutoffField_smooth f hf n).

Equations

• EulerLpTranslation.cutoffDerivativeLp f hf n = EulerLpTranslation.compactDerivative (EulerLpTranslation.cutoffField f n) ⋯ ⋯

theorem EulerLpTranslation.cutoffLp_ae {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) : ↑↑(cutoffLp f hf n) =ᵐ[MeasureTheory.volume] cutoffField f n

theorem EulerLpTranslation.cutoffDerivativeLp_ae {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) : ↑↑(cutoffDerivativeLp f hf n) =ᵐ[MeasureTheory.volume] fderiv ℝ (cutoffField f n)

theorem EulerLpTranslation.cutoffLp_tendsto {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (hLp : MeasureTheory.MemLp f 2 MeasureTheory.volume) : Filter.Tendsto (cutoffLp f hf) Filter.atTop (nhds (MeasureTheory.MemLp.toLp f hLp))

theorem EulerLpTranslation.cutoffDerivativeLp_tendsto {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (hLp : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hDLp : MeasureTheory.MemLp (fderiv ℝ f) 2 MeasureTheory.volume) : Filter.Tendsto (cutoffDerivativeLp f hf) Filter.atTop (nhds (MeasureTheory.MemLp.toLp (fderiv ℝ f) hDLp))

theorem EulerLpTranslation.smooth_hasFDerivAt {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (hLp : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hDLp : MeasureTheory.MemLp (fderiv ℝ f) 2 MeasureTheory.volume) : HasFDerivAt (fun (a : EulerSmoothLimit.Space) => (translation a) (MeasureTheory.MemLp.toLp f hLp)) (EulerLpDerivative.derivativeMap MeasureTheory.volume (MeasureTheory.MemLp.toLp (fderiv ℝ f) hDLp)) 0

No compact support assumption is needed once the actual field and its actual derivative lie in L².