Pointwise representatives of smooth Lᵖ mollification

This file connects the Lᵖ-valued average in TauCeti.MeasureTheory.Function.Lp.ApproximateIdentity with the usual pointwise convolution formula. The representative theorem applies to every MemLp function: compact support of the smooth kernel makes the convolution meaningful even when the function is not globally integrable. This is the bridge needed to pass between Lᵖ-valued mollification and classical convolution in density and localization arguments.

Attribution

The design follows LeanPool's RellichKondrachov/L2Compactness/Smoothing.lean, especially its smoothFun and smoothL2 constructions, and Tau Ceti's RepresentationTheory/Compact/Convolution.lean, especially convolutionCLM_toLp_apply.

theorem TauCeti.instFiniteDimensionalReal_tauCeti {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace E] : FiniteDimensional ℝ E

theorem TauCeti.normedBumpLp_ae_eq_convolution {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp_ne_top : p ≠ ⊤) (phi : ContDiffBump 0) {f : E → F} (hfLp : MeasureTheory.MemLp f p mu) : ↑↑((normedBumpLp hp_ne_top phi mu) (MeasureTheory.MemLp.toLp f hfLp)) =ᵐ[mu] MeasureTheory.convolution (phi.normed mu) f (ContinuousLinearMap.lsmul ℝ ℝ) mu

The Lᵖ approximate identity is represented almost everywhere by the usual pointwise convolution of any MemLp representative.