Genuine ordinary-space L² translations and closedness of their full derivative.

@[reducible, inline]

noncomputable abbrev EulerLpTranslation.L2Space (V : Type u_2) [NormedAddCommGroup V] : AddSubgroup (EulerSmoothLimit.Space →ₘ[MeasureTheory.volume] V)

L² space: an abbreviation for Lp V 2 (volume : Measure Space).

Equations

• EulerLpTranslation.L2Space V = MeasureTheory.Lp V 2 MeasureTheory.volume

noncomputable def EulerLpTranslation.translation {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : EulerSmoothLimit.Space) : ↥(L2Space V) →ₗᵢ[ℝ] ↥(L2Space V)

Translation, given by Lp.compMeasurePreservingₗᵢ ℝ (fun x : Space => x+a) (measurePreserving_add_right volume a).

Equations

• EulerLpTranslation.translation a = MeasureTheory.Lp.compMeasurePreservingₗᵢ ℝ (fun (x : EulerSmoothLimit.Space) => x + a) ⋯

theorem EulerLpTranslation.translation_ae {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : EulerSmoothLimit.Space) (u : ↥(L2Space V)) : ↑↑((translation a) u) =ᵐ[MeasureTheory.volume] fun (x : EulerSmoothLimit.Space) => ↑↑u (x + a)

@[simp]

theorem EulerLpTranslation.translation_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : ↥(L2Space V)) : (translation 0) u = u

theorem EulerLpTranslation.translation_add {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (a b : EulerSmoothLimit.Space) (u : ↥(L2Space V)) : (translation a) ((translation b) u) = (translation (a + b)) u

theorem EulerLpTranslation.translation_continuous {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : ↥(L2Space V)) : Continuous fun (a : EulerSmoothLimit.Space) => (translation a) u

theorem EulerLpTranslation.translation_norm_le {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : EulerSmoothLimit.Space) : ‖(translation a).toContinuousLinearMap‖ ≤ 1

theorem EulerLpTranslation.translation_hasFDerivAt_all {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : ↥(L2Space V)) (D : EulerSmoothLimit.Space →L[ℝ] ↥(L2Space V)) (h : HasFDerivAt (fun (a : EulerSmoothLimit.Space) => (translation a) u) D 0) (a : EulerSmoothLimit.Space) : HasFDerivAt (fun (b : EulerSmoothLimit.Space) => (translation b) u) ((translation a).toContinuousLinearMap ∘SL D) a

theorem EulerLpTranslation.translation_orbits_tendstoUniformly {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {ι : Type u_2} {l : Filter ι} (u : ι → ↥(L2Space V)) (v : ↥(L2Space V)) (hu : Filter.Tendsto u l (nhds v)) : TendstoUniformly (fun (n : ι) (a : EulerSmoothLimit.Space) => (translation a) (u n)) (fun (a : EulerSmoothLimit.Space) => (translation a) v) l

theorem EulerLpTranslation.translation_derivatives_tendstoUniformly {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {ι : Type u_2} {l : Filter ι} (D : ι → EulerSmoothLimit.Space →L[ℝ] ↥(L2Space V)) (D₀ : EulerSmoothLimit.Space →L[ℝ] ↥(L2Space V)) (hD : Filter.Tendsto D l (nhds D₀)) : TendstoUniformly (fun (n : ι) (a : EulerSmoothLimit.Space) => (translation a).toContinuousLinearMap ∘SL D n) (fun (a : EulerSmoothLimit.Space) => (translation a).toContinuousLinearMap ∘SL D₀) l

theorem EulerLpTranslation.translation_hasFDerivAt_limit {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : ℕ → ↥(L2Space V)) (D : ℕ → EulerSmoothLimit.Space →L[ℝ] ↥(L2Space V)) (u₀ : ↥(L2Space V)) (D₀ : EulerSmoothLimit.Space →L[ℝ] ↥(L2Space V)) (h : ∀ (n : ℕ), HasFDerivAt (fun (a : EulerSmoothLimit.Space) => (translation a) (u n)) (D n) 0) (hu : Filter.Tendsto u Filter.atTop (nhds u₀)) (hD : Filter.Tendsto D Filter.atTop (nhds D₀)) : HasFDerivAt (fun (a : EulerSmoothLimit.Space) => (translation a) u₀) D₀ 0

Convergent ordinary L² fields and their actual translation derivatives have the expected derivative in the limit.