MollifierGradient #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: mollified fields have strong horizontal gradients #
Algsuperdiff/Section3/Provider/Corrector/GradientIdentification.lean proves the
reverse identification mollifyGrad_ae_eq_mollify: if a stationary scalar
φ already possesses a strong horizontal gradient F, then
mollifyGrad κ φ = mollify κ F almost surely. That statement presupposes the
existence of the gradient, so it cannot produce new members of the stationary
potential subspace.
This file proves the forward direction, which needs no such hypothesis:
hasHorizontalGradient_toLp_mollify — for every φ ∈ L²(Ω) and every smooth
compactly supported kernel κ, the mollification A_κ φ lies in the domain of
the horizontal gradient and its gradient is mollifyGrad κ φ.
Smoothing therefore creates differentiability along the translation action, so
every mollified stationary scalar contributes a member of
horizontalGradientRange, hence of stationaryPotentialSubspace.
The proof is elementary; no ergodic theorem, no resolvent and no semigroup theory is used. Two ingredients:
the kernel translation identity
mollify_kernelShift:A_κ X (z +ᵥ ω) = A_{κ(· + z)} X (ω). It is the change of variablesy ↦ y + zunder the translation-invariant Lebesgue measure ofVec d, and it holds for every sample with no integrability hypothesis;the
L¹-contractionnorm_toLp_mollify_le:‖A_ν X‖_{L²(Ω)} ≤ ‖ν‖_{L¹} ‖X‖_{L²(Ω)}, which isintegral_normSq_mollify_leafter taking square roots.
Combining them, the increment of the Koopman orbit of A_κ φ minus its candidate
derivative is the mollification of φ by the second-order Taylor remainder
ν_t = κ(· + t e_i) − κ − t ∂_iκ of the kernel, whose L¹ norm is O(t²)
(exists_integral_abs_kernel_taylor_le, proved by two applications of the mean
value inequality, using that ∂_i∂_iκ is bounded and that everything in sight is
supported in one fixed ball). Hence the difference quotient converges in
L²(Ω), which is exactly HasHorizontalGradient.
Disclosure. Nothing in this file realizes any source node. It supplies the forward gradient identification for mollified stationary scalars and claims no node status.
An elementary comparison #
Translated kernels #
The kernel translated by z, namely κ(· + z).
Equations
- Algsuperdiff.Section3.Provider.Corrector.kernelShift κ z y = κ (y + z)
Instances For
Translating the sample is translating the kernel. This is the change of
variables y ↦ y + z under the translation-invariant Lebesgue measure; it holds
for every sample, with no integrability hypothesis.
Smoothness and support of the kernel derivative #
The partial derivative of a smooth kernel is smooth. (The same statement for
coordDeriv is contDiff_coordDeriv of
Algsuperdiff/Section3/Provider/Corrector/SolenoidalStream.lean; the two
functions agree, but that file is not in this import closure.)
A partial derivative does not enlarge the closed support.
The second-order Taylor bound for the kernel #
The coordinate line s ↦ y + s • e_i has derivative e_i.
The derivative of a smooth kernel along the i-th coordinate line is ∂_iκ.
The mean value bound for the first partial derivative along its own axis.
The second-order Taylor bound along a coordinate axis.
The Taylor remainder of a smooth kernel is continuous.
The Taylor remainder of a smooth compactly supported kernel is integrable.
The L¹ Taylor bound for the kernel. There is a constant C with
∫ |κ(· + t e_i) − κ − t ∂_iκ| ≤ C t² for every |t| ≤ 1. This is what makes
the Koopman difference quotient of a mollification converge in L²(Ω).
The L¹-contraction bound in L²(Ω) #
The L¹-contraction bound. Mollification by a kernel of total mass
‖κ‖₁ has operator norm at most ‖κ‖₁ on L²(Ω). This is
integral_normSq_mollify_le after taking square roots.
The forward horizontal gradient of a mollification #
The Taylor remainder of a mollification. The Koopman translate of
A_κ φ minus A_κ φ minus t times A_{κ₁} φ is exactly the mollification of
φ by the kernel remainder κ(· + t e_i) − κ − t κ₁.
The quantitative form of koopman_toLp_mollify_sub_sub_smul: the increment of
the Koopman orbit minus the candidate derivative is controlled by the L¹ norm
of the kernel remainder.
The forward gradient identification, with the kernel data as parameters.
The two hypotheses hκcont and hκint are consequences of hκ and hκc
(ContDiff.continuous and Continuous.integrable_of_hasCompactSupport); they
appear as parameters only so that the MemLp proof terms occurring in the
statement stay opaque during the proof. The consequence with those proofs
supplied is hasHorizontalGradient_toLp_mollify below.
The forward gradient identification. For every stationary
square-integrable scalar φ and every smooth compactly supported kernel κ, the
mollification A_κ φ has a strong horizontal gradient, namely mollifyGrad κ φ.
No hypothesis on φ beyond membership in L²(Ω) is used: smoothing creates
differentiability along the translation action.
This is the converse direction of mollifyGrad_ae_eq_mollify
(Algsuperdiff/Section3/Provider/Corrector/GradientIdentification.lean), which
assumes the gradient of φ to exist.
Mollified gradients lie in the stationary potential subspace. An
immediate consequence: the mollified gradient of any stationary L² scalar is a
member of horizontalGradientRange, hence of stationaryPotentialSubspace.