Global Contraction Estimate for Mollification
ProvedFunctionalInequalities.Analysis.Mollification.lintegral_enorm_convolution_sq_le_readableThis is the global squared extended-norm contraction estimate for a normalized mollifier.
Let be a finite-dimensional real inner-product space, let be an additive Haar measure, let be a normed real vector space, and let be a smooth bump centered at . If is almost everywhere strongly measurable, then
Both integrals are lower integrals with values in (ENNReal). This is the measure-theoretic contraction property used in mollification arguments.
Original Lean declaration header
Within namespace FunctionalInequalities.Analysis.Mollification. Shown in its original module context. Proof omitted.
theorem lintegral_enorm_convolution_sq_le {f : V → E} (hf : AEStronglyMeasurable f m) :
∫⁻ x, ‖(φ.normed m ⋆[ContinuousLinearMap.lsmul ℝ ℝ, m] f) x‖ₑ ^ 2 ∂m ≤
∫⁻ x, ‖f x‖ₑ ^ 2 ∂m
Module navigation
Module: Analysis/Mollification/Basic.
Supporting theorems: enorm_convolution_sq_le.
Previous: enorm_convolution_sq_le · Next: tendsto_eLpNorm_convolution_sub_of_continuous.
Source excerpt, lines 97–99 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Mollification_Basic
open MeasureTheory Filter Topology Metric InnerProductSpace
open scoped Convolution ContDiff ENNReal RealInnerProductSpace
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
[MeasurableSpace V] [BorelSpace V] {m : MeasureTheory.Measure V} [m.IsAddHaarMeasure]
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
variable (φ : ContDiffBump (0 : V))
theorem FunctionalInequalities.Analysis.Mollification.lintegral_enorm_convolution_sq_le_readable {f : V → E} (hf : AEStronglyMeasurable f m) :
∫⁻ x, ‖(φ.normed m ⋆[ContinuousLinearMap.lsmul ℝ ℝ, m] f) x‖ₑ ^ 2 ∂m ≤
∫⁻ x, ‖f x‖ₑ ^ 2 ∂m := by sorry