ShellSumCarrierDecorrelation #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The shell-sum forcing has compactly supported covariance, at range √d · 3^m #
ABK26, e.perturb.assumption and its forcing shom_{m-h}^{-1} (k_m - k_{m-h}) e of e.def.w.
Algsuperdiff/Section3/Provider/Corrector/FreshShellDecorrelation.lean proves
the covariance kill for the fresh shell alone, at the range √d hard-wired
in ShellLawJ1.range_dependence. The recurrence consumer
Provider/Diffusivity/ApproximateRecurrence/LocalizationRecurrenceMesh.lean
does not force with one shell but with the finite shell increment
k_m - k_n = Σ_{k ∈ (n,m]} j_k, whose range of dependence is √d · 3^m, not
√d. This file supplies the covariance kill at that range.
Nothing in FreshShellDecorrelation.lean is edited: its √d statements keep
their consumers, and the statements below are the strictly more general forms,
proved from the same two halves of (J1) plus the cross-shell independence of
ABK26.
The two mechanisms #
Write f_Σ(ω)(x) = (Σ_{k ∈ (n,m]} j_k(x)) e for the shell-sum forcing. Its
covariance expands into the double sum Σ_{k,k'} E[ (j_k(w) e) · (j_{k'}(0) e) ]
and every term vanishes, for two different reasons:
- the diagonal terms
k = k'by the spatial range of dependence of shellkat range√d · 3^k ≤ √d · 3^m-- this ise.diff.law.shift(ShellLawPrefix.marginal_scaling) applied to (J1), already packaged asCutoff.indep_shellLocal_of_cutoff_separation; - the off-diagonal terms
k ≠ k'by the cross-shell independence of ABK26,ShellLawPrefix.independent, packaged asCutoff.indepFun_of_measurable_shellIndexSigma_of_disjoint.
In both cases the two factors are independent, so the product is integrable and
its expectation factors; the frozen mean-zero field then kills each factor
(Stream.integral_shell_entry_at_point_eq_zero, itself a marginal_scaling
transport of ShellLawJ1.mean_zero).
The reachable constant #
Exactly as at the fresh shell, ‖w‖ = √d · 3^m is not reachable and every
‖w‖ > √d · 3^m is: the frozen (J1) local σ-algebras are integral
generated, so a point value is local only on a set containing a ball of strictly
positive radius, and the two read sets must be thickened before (J1) applies.
The exported forms are therefore stated with a strict inequality
(..._of_lt_norm).
Main results #
indepFun_shellRowForcing-- any two shell-row observables of the increment, one read atwand one at the origin, are independent once√d · 3^m < ‖w‖.memLp_two_hilbertForcing_finiteShellIncrement-- the shell-sum forcing lies inL²; the Minkowski step over the block of the frozen (J2) tail.integral_vecDot_matVecMul_finiteShellIncrement_eq_zero_of_lt_norm-- the covariance of the shell-sum forcing against itsw-translate vanishes.
Separation of two thickened read sets, at an arbitrary range #
The shell-row observables of the increment forcing #
The i-th component of j_k(x) e, as a real observable of the shell
sequence. The shell-sum forcing pairs into the double sum over shell indices of
products of two such observables, one read at w and one read at 0.
Equations
- Algsuperdiff.Section3.Provider.Corrector.shellRowForcing e x i k omega = ∑ l : Fin d, (↑(omega k)).1 x i l * e l
Instances For
Integrability and mean zero of a shell-row observable #
The shell-row observables are square integrable. This is the frozen (J2)
tail transported to shell k by e.diff.law.shift, through
Stream.memLp_two_shell_entry.
The shell-row observables are centred. This is the frozen (J1)
mean-zero field transported to shell k by e.diff.law.shift, through
Stream.integral_shell_entry_at_point_eq_zero.
Independence of the two read points #
Any two shell-row observables of the increment decouple.
k and k' are two shell indices at or below m, the first observable is read
at w and the second at the origin, and √d · 3^m < ‖w‖. Then the two are
independent. Two disjoint mechanisms cover the two cases: for k = k' the
spatial range of dependence of shell k at range √d · 3^k ≤ √d · 3^m, for
k ≠ k' the cross-shell independence of ABK26.
The expectation of a product of two shell-row observables of the increment,
one read at w and one at the origin, vanishes: they are independent and each
is centred.
The covariance of the shell-sum forcing #
The forcing coordinate of the finite shell increment is the sum over the shell block of the shell-row observables.
The shell-sum forcing splits over the block into the single-shell forcings.
Both matVecMul (· ) e and HilbertVec.ofVec are linear.
The single-shell forcing lies in L²: the frozen (J2) tail read through
Stream.memLp_two_shell_entry.
The shell-sum forcing lies in L².
The Minkowski step of the manuscript's L² bookkeeping: the block forcing is
the sum over the block of the single-shell forcings, and every shell entry is
square integrable by the frozen (J2) tail through
Stream.memLp_two_shell_entry. No normalization of e is assumed.
The shell-sum forcing has compactly supported covariance, at the range
√d · 3^m.
For every translation w with √d · 3^m < ‖w‖, the covariance of the finite
shell-increment forcing (k_m - k_n) e against its w-translate vanishes under
the shell-sequence law. The two halves of (J1), e.diff.law.shift and the
cross-shell independence of are the only inputs; no lower bound on n is needed
and the degenerate block m ≤ n is covered (the increment is then zero).