ShellSumCarrierLaw #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The shell-sum law on the continuous-path carrier #
ABK26, e.def.w and e.perturb.assumption.
Algsuperdiff/Section3/Provider/Corrector/ValuePathTransport.lean puts the
fresh shell on the compact-open carrier C(Vec d, Mat d) -- the only
carrier in this repository that supplies the joint measurability
MeasurableVAdd₂ (Vec d) Ω the Ω-level decorrelation chain needs -- as the
law zeroShellValuePathLaw. The recurrence consumers force not with one shell
but with the finite shell increment k_m - k_n = Σ_{k ∈ (n,m]} j_k
(Cutoff.finiteShellIncrement, Corrector.streamForcing).
This module puts that increment on the same carrier, as
shellSumValuePathLaw M n m, and supplies the three carrier facts the chain
consumes. The point of re-using C(Vec d, Mat d) rather than introducing a new
carrier is that the forcing function does not change: the shell-sum forcing
is literally valuePathForcing e, the same function of a continuous path that
ValuePathTransport uses; only the law on the carrier is new. Every statement
of ValuePathTransport that is about the function therefore transfers
verbatim, and only the measure-dependent statements are reproved here.
What is supplied #
shellSumValuePath-- the increment as a continuous matrix path, withshellSumValuePath_applyidentifying its values withCutoff.finiteShellIncrement.shellSumValuePathLaw-- its law, a probability measure onC(Vec d, Mat d).vaddInvariantMeasure_shellSumValuePathLaw-- stationarity. The input isCutoff.sequenceLaw_stationary, i.e. (J1) stationarity of the zero shell transported to every shell bye.diff.law.shift(ShellLawPrefix.marginal_scaling) and lifted to the whole sequence by the cross-shell independence of ABK26. No new assumption is used.memLp_two_valuePathForcing_shellSum-- theL²layer of the shell-sum forcing, the Minkowski step over the block of the frozen (J2) tail.integral_inner_valuePathForcing_vadd_shellSum_eq_zero-- the covariance kill at the increment's own range√d · 3^m, transported fromShellSumCarrierDecorrelation.lean. This is exactly thehcovbinder ofintegral_normSq_mollify_le_of_helmholtz_of_covariance_support, at the shell-sum carrier.integral_normSq_mollify_le_of_helmholtz_shellSum-- the unconditional decorrelation boundE[|A_κ 𝐣|²] ≤ B · |B_{√d·3^m+1}| · E[|𝐟|²]at this carrier, with no covariance, noL²and no instance obligation left on the caller.
What is not supplied here #
The Helmholtz splitting of the increment flux and the approximate-stream
assembly at this carrier are not proved in this module.
OmegaStreamAssembly's exists_freshShellStream is stated at
zeroShellValuePathLaw and does not apply to shellSumValuePathLaw; its
shell-sum analogue remains open. Nothing below claims any source-node status.
The increment as a continuous matrix path #
The finite shell increment k_m - k_n, read as a continuous matrix path.
This is the same object as Cutoff.finiteShellIncrement (see
shellSumValuePath_apply) on the carrier that supports the joint translation
action.
Equations
- Algsuperdiff.Section3.Provider.Corrector.shellSumValuePath n m omega = ∑ k ∈ Finset.Ioc n m, (omega k).valuePath
Instances For
The law of the finite shell increment on the continuous-path carrier.
The analogue of zeroShellValuePathLaw with the single fresh shell replaced by
the block (n, m].
Equations
Instances For
Equivariance and stationarity #
The increment path is equivariant: translating every shell of the sequence translates the increment path.
The shell-sum law is translation invariant.
The only input is Cutoff.sequenceLaw_stationary: (J1) stationarity of the zero
shell, transported to every shell marginal by e.diff.law.shift
(ShellLawPrefix.marginal_scaling), and lifted to the joint law of the sequence
by the cross-shell independence of ABK26, ShellLawPrefix.independent. No
invariance is assumed on the target law.
The L² layer of the shell-sum forcing #
The shell-sum forcing is square integrable on the continuous-path
carrier. Transported from memLp_two_hilbertForcing_finiteShellIncrement,
whose input is the Minkowski sum over the block of the frozen (J2) tail. No
normalization of e is assumed.
The covariance kill at the increment's own range #
The shell-sum forcing has compactly supported covariance on the continuous-path carrier.
For every translation w with √d · 3^m < ‖w‖, the covariance of the path
forcing against its w-translate vanishes under the shell-sum law. This is
literally the hcov binder of
integral_normSq_mollify_le_of_helmholtz_of_covariance_support at
Ω := C(Vec d, Mat d) and μ := (shellSumValuePathLaw M.P n m).toMeasure; the
(J1) range dependence, e.diff.law.shift and the cross-shell independence
argument is not repeated, it is transported from
integral_vecDot_matVecMul_finiteShellIncrement_eq_zero_of_lt_norm.
The covariance support statement at the concrete admissible radius
√d · 3^m + 1.
The unconditional shell-sum decorrelation bound #
The shell-sum decorrelation bound, with no covariance hypothesis.
Let 𝐣 = 𝐟 + p be a stationary Helmholtz splitting of the shell-sum forcing
𝐟 = valuePathForcing e under the shell-sum law: p lies in the stationary
potential subspace of that carrier and 𝐣 in its stationary solenoidal
subspace. Then for every probability density κ bounded by B,
E[|A_κ 𝐣|²] ≤ B · |B_{√d·3^m+1}| · E[|𝐟|²].
Compared with integral_normSq_mollify_le_of_helmholtz_of_covariance_support,
the covariance support hypothesis hcov is discharged here at the increment's
own range from (J1), e.diff.law.shift and the cross-shell independence, the
L² layer of the forcing is discharged from (J2), and all three carrier
instances are available, so no instance obligation is left on the caller. The
remaining binders are the caller's Helmholtz data.
This is the exact shell-sum analogue of
ValuePathTransport.integral_normSq_mollify_le_of_helmholtz_valuePath, with the
radius √d + 1 of the single fresh shell replaced by the increment's own range
√d · 3^m + 1.