GradientIdentification #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the mollified gradient is the mollification of the gradient #
Algsuperdiff/Section3/Provider/Corrector/MollifiedPrimitive.lean produces, for
every stationary L² scalar φ and every smooth compactly supported kernel
κ, a member mollify κ φ of the dense class of part (i) of
l.approximation.stationary.by.local together with its spatial gradient
mollifyGrad κ φ (whose ith component is the mollification of φ by ∂ᵢκ).
mollifyGrad κ φ = mollify κ F almost surely,
whenever F is the strong horizontal gradient of φ in L²(Ω)
(Algsuperdiff.Probability.Stationary.HasHorizontalGradient).
The proof uses no integration by parts. The difference quotients of the
mollified field along the ith coordinate orbit converge
- pointwise, for almost every sample, to
mollify (∂ᵢκ) φ, because the spatial realization ofmollify κ φis smooth with derivative(∂ᵢκ) ⋆ realize φ(fderiv_realize_mollify), and - in
L²(Ω)tomollify κ Fᵢ, because the difference quotients ofφitself converge toFᵢinL²(Ω)and mollification is anL²contraction (integral_normSq_mollify_le).
Fatou's lemma then forces the two limits to agree. Combining this with the
approximate-identity estimate of
Algsuperdiff/Section3/Provider/Corrector/MollifierConvergence.lean shows that
the mollified gradients are L²-dense in the stationary potential subspace.
The Koopman action at the origin #
The Koopman operator of the zero translation is the identity.
An L²-versus-pointwise uniqueness lemma #
If a sequence converges pointwise almost everywhere to B and its squared
L² distance to C tends to zero, then B = C almost everywhere. This is
Fatou's lemma; it replaces the usual "convergence in measure plus subsequence"
argument.
Difference quotients of the mollified orbit #
The mollified field is differentiable along every coordinate orbit, with derivative the mollification by the corresponding partial derivative of the kernel. This is the pointwise half of the gradient identification.
Difference quotients along a coordinate orbit #
The difference quotient of a stationary field along the ith coordinate
orbit at scale t.
Equations
- Algsuperdiff.Section3.Provider.Corrector.diffQuot i t φ ω = t⁻¹ • (φ (t • HCPolySupport.basisVec i +ᵥ ω) - φ ω)
Instances For
The gradient identification #
The sequence of scales along which the difference quotients are taken.
Equations
Instances For
Componentwise gradient identification. If the coordinate orbit of φ
has strong L² derivative G at the origin, then mollifying φ by the ith
partial derivative of the kernel is the same as mollifying G by the kernel.
The vector form of the gradient identification #
The ith coordinate of a Euclidean-vector-valued stationary field.
Equations
- Algsuperdiff.Section3.Provider.Corrector.coordField F i ω = (F ω).toVec i
Instances For
Mollification commutes with taking a coordinate.
The L² coordinate projection is computed by the coordinate field.
The gradient identification. The mollified gradient of a stationary
L² scalar is the mollification of its strong horizontal gradient.
Density of the mollified gradients in the stationary potential subspace #
The L² energy of the difference of two square-integrable fields is the
squared distance of their classes.
Density of the mollified gradients. Every element of the stationary
potential subspace L²_pot(Ω) is approximated in L²(Ω), to any prescribed
accuracy, by the mollified gradient of a stationary square-integrable scalar.
This is what removes the smooth-primitive hypothesis from the cutoff core of
part (i) of l.approximation.stationary.by.local.