MollifiedDecorrelation #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: mollification against the stationary Helmholtz splitting, and the #
decorrelation kill
Step 3 of the proof of l.corrector.limit consumes part (ii) of
l.approximation.stationary.by.local: the stationary solenoidal flux 𝐣 = 𝐟 + ∇w must be approximated, inside each cube cu_K, by members of
L²_{sol,0}(cu_K). The manuscript's competitor is the row divergence of a
cutoff antisymmetric stream tensor S with 𝐣_i = Σ_m ∂_m S_{im}, whose
per-realization layer is already available
(Algsuperdiff/Section3/Provider/Corrector/SolenoidalStream.lean).
Part (ii) cannot hold for an arbitrary stationary solenoidal 𝐣: by
Algsuperdiff/Section3/Provider/Corrector/SolenoidalStream.lean
(normSq_le_cubeAverage_normSq_const_sub) a nonzero constant — hence
Koopman-invariant — field is a genuine counterexample to the displayed bound, so
a condition forcing the translation-invariant part of 𝐣 to vanish is necessary
rather than merely convenient.
Motivation, not a claim proved here. The stream constructions that smooth
along the translation action — the resolvent stream
S^λ_{im} = −G_λ(D_m 𝐣_i − D_i 𝐣_m), and the kernel stream
S_{im} = A_{g_m} 𝐣_i − A_{g_i} 𝐣_m built from a smooth compactly supported
vector field g on ℝᵈ — reproduce 𝐣 up to a residual of the shape A_κ 𝐣
with κ a probability density spread over a large scale. Making such a residual
small is therefore the quantitative content of "the invariant part of 𝐣
vanishes".
This file supplies that quantitative content, on the abstract stationary carrier
and with no ergodic theorem, no Liouville argument and no resolvent. Writing
A_κ for the mollification by a probability density κ along the translation
action, the two results are:
norm_toLp_mollify_le_of_helmholtz— if𝐣 = 𝐟 + pwithp ∈ L²_pot(Ω)and𝐣 ∈ L²_sol(Ω)(the Helmholtz characterization of the whole-space corrector∇w = p, ABK26), then‖A_κ 𝐣‖_{L²(Ω)} ≤ ‖A_κ 𝐟‖_{L²(Ω)}: smoothing the flux is controlled by smoothing the forcing. This rests on the fact thatA_κpreserves both halves of the stationary Helmholtz splitting, which in turn is a one-line consequence of the pairing formulaintegral_inner_mollifytogether with the Koopman invariance ofL²_pot(Ω)(koopman_mem_stationaryPotentialSubspace).integral_normSq_mollify_le_of_covariance_support— if the stationary covariancew ↦ E[⟪X(w + ·), X⟫]vanishes for‖w‖ ≥ ρ(which is what a finite range of dependence together with a vanishing mean gives), thenE[|A_κ X|²] ≤ ‖κ‖_∞ · |B_ρ| · E[|X|²].
Composing them (integral_normSq_mollify_le_of_helmholtz_of_covariance_support)
gives E[|A_κ 𝐣|²] ≤ ‖κ‖_∞ |B_ρ| E[|𝐟|²], so A_κ 𝐣 → 0 in L²(Ω) along any
family of probability densities whose sup norms tend to 0, even though the
flux 𝐣 itself has no finite range of dependence. Nothing here uses the mean
ergodic theorem: the whole input is the finite range of the forcing's
covariance.
Disclosure. Nothing in this file realizes any source node. It proves the
Ω-level decorrelation input of part (ii) of
l.approximation.stationary.by.local; it does not prove part (ii) (the stream
construction and the cube cutoff are not done here), and it claims no node
status.
The Koopman action as a group of unitaries #
The Koopman translate of an L² class is represented by the translated
representative.
The Koopman operators compose: U_x ∘ U_y = U_{y+x}.
The Koopman adjoint identity: the translation operators are unitary, so a translation may be moved to the other side of the inner product with the opposite sign.
The Koopman action preserves the stationary Helmholtz splitting #
Coordinate extraction commutes with the Koopman action.
The Koopman action transports strong horizontal gradients.
The stationary potential subspace is Koopman invariant.
The stationary solenoidal subspace is Koopman invariant.
Inner-product bridges between classes and representatives #
The L² inner product of two classes is the integral of the pointwise inner
products of any representatives.
The pairing of a Koopman translate against another class, in integral form.
The pairing formula for a mollification #
Joint integrability of the pairing integrand of a mollification.
The pairing formula for a mollification. Testing a mollified field
against another stationary L² field distributes the kernel over the Koopman
translates.
The pairing formula at the level of L² classes.
Mollification preserves the stationary Helmholtz splitting #
Mollification preserves the stationary solenoidal subspace.
Mollification preserves the stationary potential subspace.
The Helmholtz reduction.
The decorrelation bound #
The decorrelation bound.
The fresh-shell decorrelation kill #
The decorrelation kill for the stationary solenoidal flux.
Let 𝐣 = 𝐟 + p be the stationary Helmholtz splitting of ABK26: p = ∇w lies in
L²_pot(Ω) and the flux 𝐣 lies in L²_sol(Ω). Suppose the forcing 𝐟 has
a covariance supported in the ball of radius ρ — which is exactly what a
finite range of dependence together with a vanishing mean supplies. Then for
every probability density κ bounded by M,
E[|A_κ 𝐣|²] ≤ M · |B_ρ| · E[|𝐟|²].
Along any family of densities whose sup norms tend to 0 the right-hand side
tends to 0, so the translation-invariant part of the flux is annihilated even
though the flux itself has no finite range of dependence. No ergodic theorem,
no Liouville argument and no resolvent is used.
Disclosure. This is the Ω-level decorrelation input of part (ii) of
l.approximation.stationary.by.local, not part (ii) itself, and it claims no
node status.