GridDomination #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The gap-0 fold behind hgrid #
Provider/CoarseEllipticity/LowerLeg.lean retains one conditional analytic
input called hgrid --- the domination of the leg's target observable by a
weighted series of per-scale triadic grid maxima, in one of the two shapes
hgrid : forall omega, X omega <= sum_k mass * gridWeight rho k * G k omega (upper leg)
hgrid : forall omega, forall L >= L0, X L omega <= sum_k mass * gridWeight rho k * G k omega
(lower)
The deterministic content behind such a binder --- Lambda_{s,2} and
lambda_{s,2}^{-1} are weighted grid series, gap-0 term included --- is the
subject of Provider/CoarseEllipticity/LambdaGridBridge.lean. This module
supplies the one piece of arithmetic that separates what such a bridge displays
from the shape a consumer accepts: the two index ranges do not match, and the
mismatch is a single extra summand.
The gap-0 fold, and why it is free #
The source series runs over k <= m while gridWeight covers the gaps >= 1
of the proof's own binder n <= m-1. The bridge therefore displays the
gap-0 summand mass * (top-scale maximum) separately, and the consumers'
right-hand side has no slot for it. It is folded into the series here: for any
ctop with 1 <= ctop * sum_k gridWeight rho k,
mass * T + sum_k mass * gridWeight rho k * u k
<= sum_k mass * gridWeight rho k * (ctop * T + u k)
(top_add_gridSum_le_gridSum). At the source's own data the fold is exact,
not lossy: sum_k gridWeight (2s) k = 3^{-2s} (1 - 3^{-2s})^{-1}, so the
canonical ctop = 3^{2s} (one_le_rpow_mul_tsum_gridWeight) reproduces the
gap-0 term with the multiplier mass * ctop * sum_k gridWeight (2s) k = 1 at
mass = c_{s,2} = 1 - 3^{-2s}. Since s <= 1 on the frozen window,
ctop <= 9: the fold costs a dimension-free bounded factor and no pole.
What is proved here #
one_le_rpow_mul_tsum_gridWeight,top_add_gridSum_le_gridSum--- the fold, model-free: neither statement mentions a coefficient field, a cutoff sample or a probability measure, and both areforall-quantified with no almost-everywhere hypothesis used or produced.
Why the fold is stated at an arbitrary majorizing family #
top_add_gridSum_le_gridSum does not name a grid family: it asks only for some
G with ctop * T + u k <= G k at every gap k. That generality is what the
two legs need, and they need it differently.
The upper leg's target is read at a single cutoff index, so there a majorant may be built from the sample alone and no binder survives.
The lower leg's target is the whole family {X L}_{L >= m-1} with an
L-free right-hand side (that is what a single witness for
Probability.IsLowerIntegerFamilyOrlicz means), while any grid family built
from the coefficient cutoff Cutoff.coefficientCutoff M.nu L omega reads the
index L. The L-uniformity is therefore an obligation on the caller, who
must exhibit an L-free family G majorizing the folded grid maxima at every
L >= L0. What that obligation amounts to is the analytic requirement that
the block estimate p.bfA.multiscalebound be uniform in the cutoff index,
which is how the source uses it.
What is not claimed here #
No on-grid domination of an actual observable is proved here, and no block
estimate, no e.maxy.bound lift and no base case is claimed. In particular
hsplit --- the per-scale split of the grid maxima into a deterministic
constant and the Gamma lanes --- is untouched. The two legs themselves are
delivered downstream by the superposed-flux pre-split route, as
superposedFlux_coarse_ellipticity_lower_leg and
superposedFlux_coarse_ellipticity_upper_leg.
References #
- ABK26, coarse-grained ellipticity constants, (the definition and the
normalizer
c_{sq});p.cg.ellipticity.bounds, statement, proof fromp.bfA.multiscalebound(the grid maximum and the summation). Provider/BadEvents/ObservableSwapPayoff.lean(the observables at the translated cutoff samples),Provider/CoarseEllipticity/LambdaGridBridge.lean(the deterministic bridge and theq = 2weight arithmetic),.../GridWeights.lean(gridWeight,gridSupAbs),.../LowerLeg.lean(thehgridconsumer).
1. The gap-0 fold #
The canonical fold constant. ctop = 3^{rho} covers the gap-0 term
against the whole grid series, because the series already contains the gap-1
weight 3^{-rho}.
The gap-0 fold. The source's series carries a gap-0 summand mass * T
outside the gridWeight family (against the proof's binder n <= m-1). Any
family G majorizing ctop * T + u k at every scale absorbs it, provided
ctop covers the gap-0 term against the total weight.
The inequality is proved by comparison inside the series, so the only summability needed is that of the majorizing series itself: the two smaller series are summable by domination.