Normalized bump averages

This file defines averaging against a normalized smooth bump for a strongly continuous family of linear isometries on a real normed space. The resulting continuous linear operator is a contraction, commutes with continuous linear maps that intertwine the isometry families, and converges strongly to the value of the family at zero as the bump radius shrinks to zero.

Main declarations

• TauCeti.normedBumpAverageL: normalized-bump averaging for a strongly continuous family of linear isometries on a normed space.
• TauCeti.normedBumpAverageL_comm: an intertwining continuous linear map commutes with normalized-bump averaging.
• TauCeti.norm_normedBumpAverageL_le_one: normalized-bump averaging is a contraction.
• TauCeti.tendsto_normedBumpAverageL: normalized-bump averages converge strongly as their radii shrink to zero.

References

L. C. Evans, Partial Differential Equations, Chapter 5, §5.3.1; H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Proposition 4.21.

noncomputable def TauCeti.normedBumpAverageL {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (phi : ContDiffBump 0) (mu : MeasureTheory.Measure E) [MeasureTheory.IsLocallyFiniteMeasure mu] [mu.IsOpenPosMeasure] (T : E → F ≃ₗᵢ[ℝ] F) (hT : ∀ (f : F), Continuous fun (h : E) => (T h) f) : F →L[ℝ] F

Averaging a strongly continuous family of linear isometries against the normalized form of a smooth bump centred at zero, as a continuous linear operator. The continuity hypothesis makes the compactly supported integrand Bochner integrable. As with MeasureTheory.average, completeness is needed only for the integral to have its usual value, and is therefore assumed by the convergence theorem rather than this definition.

Equations

• TauCeti.normedBumpAverageL phi mu T hT = { toFun := TauCeti.normedBumpAverage✝ phi mu T, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

theorem TauCeti.normedBumpAverageL_apply {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (phi : ContDiffBump 0) (mu : MeasureTheory.Measure E) [MeasureTheory.IsLocallyFiniteMeasure mu] [mu.IsOpenPosMeasure] (T : E → F ≃ₗᵢ[ℝ] F) (hT : ∀ (f : F), Continuous fun (h : E) => (T h) f) (f : F) : (normedBumpAverageL phi mu T hT) f = ∫ (t : E), phi.normed mu t • (T (-t)) f ∂mu

The defining Bochner-integral formula for normedBumpAverageL.

theorem TauCeti.map_normedBumpAverageL {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace F] [CompleteSpace G] (A : F →L[ℝ] G) (phi : ContDiffBump 0) (mu : MeasureTheory.Measure E) [MeasureTheory.IsLocallyFiniteMeasure mu] [mu.IsOpenPosMeasure] (T : E → F ≃ₗᵢ[ℝ] F) (hT : ∀ (f : F), Continuous fun (h : E) => (T h) f) (f : F) : A ((normedBumpAverageL phi mu T hT) f) = ∫ (t : E), phi.normed mu t • A ((T (-t)) f) ∂mu

A continuous linear map between complete spaces commutes with a normalized-bump average.

theorem TauCeti.normedBumpAverageL_comm {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace F] [CompleteSpace G] (A : F →L[ℝ] G) (phi : ContDiffBump 0) (mu : MeasureTheory.Measure E) [MeasureTheory.IsLocallyFiniteMeasure mu] [mu.IsOpenPosMeasure] (T : E → F ≃ₗᵢ[ℝ] F) (T' : E → G ≃ₗᵢ[ℝ] G) (hT : ∀ (f : F), Continuous fun (h : E) => (T h) f) (hT' : ∀ (g : G), Continuous fun (h : E) => (T' h) g) (hA : ∀ (h : E) (f : F), A ((T h) f) = (T' h) (A f)) (f : F) : A ((normedBumpAverageL phi mu T hT) f) = (normedBumpAverageL phi mu T' hT') (A f)

A continuous linear map between complete spaces that intertwines two strongly continuous families of linear isometries also intertwines their normalized-bump averages.

theorem TauCeti.norm_normedBumpAverageL_le_one {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (phi : ContDiffBump 0) (mu : MeasureTheory.Measure E) [MeasureTheory.IsLocallyFiniteMeasure mu] [mu.IsOpenPosMeasure] (T : E → F ≃ₗᵢ[ℝ] F) (hT : ∀ (f : F), Continuous fun (h : E) => (T h) f) : ‖normedBumpAverageL phi mu T hT‖ ≤ 1

A normalized-bump average of linear isometries has operator norm at most one.

theorem TauCeti.tendsto_normedBumpAverageL {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {I : Type u_3} {l : Filter I} {phi : I → ContDiffBump 0} (hphi : Filter.Tendsto (fun (i : I) => (phi i).rOut) l (nhds 0)) (mu : MeasureTheory.Measure E) [mu.IsAddHaarMeasure] (T : E → F ≃ₗᵢ[ℝ] F) (hT : ∀ (f : F), Continuous fun (h : E) => (T h) f) (f : F) : Filter.Tendsto (fun (i : I) => (normedBumpAverageL (phi i) mu T hT) f) l (nhds ((T 0) f))

Normalized-bump averages of a strongly continuous family of linear isometries converge to the value of the family at zero as the bump radii tend to zero.