MollifierConvergence #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: mollification converges in L²(Ω) as the radius shrinks #
Algsuperdiff/Section3/Provider/Corrector/Mollification.lean builds the
smoothing operator mollify ρ X ω = ∫ ρ(y) • X((-y) +ᵥ ω) along the stationary
translation action and shows that it stays inside the stationary L² layer.
This file supplies the quantitative half needed by part (i) of
l.approximation.stationary.by.local: mollification is an approximate identity
on L²(Ω),
‖mollify ρ X − X‖²_{L²(Ω)} ≤ sup_{|y| < radius ρ} ‖X((−y) + ·) − X‖²_{L²(Ω)},
and the right-hand side tends to 0 with the radius because the Koopman orbit
y ↦ X((−y) + ·) is L²-continuous
(Algsuperdiff.Probability.Stationary.continuous_koopman_orbit).
Along the way the file records the elementary algebra of mollify (linearity
and equivariance under the translation action) and the identity
‖f‖²_{L²} = ∫ ‖f‖², both of which are also consumed by the gradient
identification of
Algsuperdiff/Section3/Provider/Corrector/GradientIdentification.lean.
The squared L² norm as an integral #
The squared norm of an L² class is the integral of the squared pointwise
norms of any of its representatives.
The L² energy of a square-integrable function is the squared norm of its
class.
Elementary algebra of the mollification #
Mollification commutes with the translation action: this is the pointwise form of the fact that the Koopman operators commute with the smoothing.
Mollification is additive, given the integrability of the two pieces.
Mollification is homogeneous.
Integrability of the mollification kernel #
The integrand of the mollification is integrable for almost every sample.
Joint integrability of the weighted squared increment of a stationary L²
field.
The weighted increment integrability facts used by the approximate-identity estimate, for almost every sample.
The approximate-identity estimate #
The pointwise Jensen bound behind the approximate-identity estimate.
The approximate-identity estimate. If the L² increment of the field
under every translation of size below the radius of the mollifier is at most
ε, then the mollification differs from the field by at most ε in squared
L² norm.
L² continuity of the translation action #
The Koopman translate of an L² class is represented by the translated
representative.
The L² increment of a stationary field under a translation is the squared
distance travelled by the Koopman orbit.
The L² modulus of continuity of the translation action is continuous.
This is the only place where the ContinuousAction-style carrier hypotheses of
Algsuperdiff/Probability/StationaryProjection.lean are used.
Mollification is an approximate identity on L²(Ω). For every
tolerance there is a radius at which the mollification of a stationary L²
field differs from it by at most that tolerance in squared L² norm.