ShellSlotBounds #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The two gauge slots, resolved into a head block and an L-carrying tail #
Nothing here imports that file, and nothing here claims the anchor.
The shell-sum route #
MajorantSlots.lean isolates the whole L-dependence of Step 3's display in
the two gauges of the recentered shell h = k_L − k_{j−2} − (k_L − k_m)_{□_m}.
This module resolves both gauges into
(an L-FREE head block over the layers k ∈ (j−2, m]) + (a tail over k ∈ (m, L]) ,
using only proved material:
- the gradient slot --
Annular.gradientW1Infinity_centeredShellUnitCube_le(the cube-scale normalization: the centering constant is invisible to a gradient gauge) followed bySupport.shellW1InfGradNorm_translate_shellIncrement_split(the manuscript's∇(k_L − k_{j−2}) = Σ ∇j_kplus the triangle inequality, split atm); - the value slot --
Annular.valueL2_centeredShellUnitCube_le(the manuscript's own split: theL^∞content ofk_m − k_{j−2}on3^j v + □_jplus the mean-value bound fork_L − k_m − (k_L − k_m)_{□_m}on□_m) followed by the same layer expansion at the origin cube of scalem.
Both tails are values of ONE functional of the shell stream, the
(m, L]-layer gauge sum
tailLayerSum k v ω L = Σ_{i ∈ (m, L]} ‖∇ j_i‖_{W^{1,∞}(3^k v + □_k)} ,
which is nondecreasing in L. An L-free bound for it is therefore the ONLY
L-uniformity input the whole majorant needs; it is a parameter here
(hT), disclosed below.
The disclosed obligation hT, and why it is not discharged here #
hT asks for a real T k v ω dominating the tail sums for every L ≥ m, i.e.
for the convergence of the upper shell series with an explicit bound. This is a
genuine mathematical input about the stream, not a source premise and not a
proof step in disguise:
- it holds almost surely (each layer gauge is
O_{Γ₂}(3^{(γ−1)k})byStream.isBigOWith_gammaSigma_shellDerivGauge_cube, andγ < 1), but - it hold for every
ωin the carrier:Cutoff.CutoffSampleconstrains only the lower tails (Cutoff.LowerTailGood), so the upper shell series diverges on a (null, nonempty) set of sequences.
References #
- ABK26,
l.bounds.mathcal.E.aL, (Step 3); (e.ugly.estimate.for.J.pre, the gradient slot); (the layer expansion); (e.jk.O,e.nabla.jk.O).
The layer gauge sums #
The head block of the layer expansion at the cube 3^k v + □_k: the layers
i ∈ (k−2, m], which is the block the Step-3 display resums. L-free.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The tail block of the layer expansion at the cube 3^k v + □_k: the layers
i ∈ (m, L], i.e. the k > m block. This is the ONLY carrier of L in the
whole majorant.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The layer gauge extended by zero below the recentering scale: the canonical
ℤ-indexed summand of the upper shell series.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical tail gauge: the value of the upper shell series.
Equations
- Algsuperdiff.Section4.Provider.BoundsEaL.tailSeriesGauge m k v omega = ∑' (i : ℤ), Algsuperdiff.Section4.Provider.BoundsEaL.tailLayerTerm m k v omega i
Instances For
The obligation hT, reduced to summability.
If the upper shell series converges at ω, its value is an L-uniform bound for
every tail block. This is the exact bridge from a probabilistic
summability statement to the L-freeness input used below: no other property of
the stream is needed.
The gradient slot #
The gradient gauge of the recentered shell, split at m.
The cube-scale normalization of Annular.GradNormalization followed by the
layer expansion of Support.shellW1InfGradNorm_translate_shellIncrement_split.
The head block is L-free; the tail block is the k > m layer sum.
The L-free gradient slot, at a caller-supplied tail gauge T.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The gradient slot bound, L-free. Every L ≥ m obeys the same bound
once the tail gauge is L-uniform.
The value slot #
The mean-value tail of the value slot, expanded into layers.
3^{2m} ‖∇(k_L − k_m)‖_{W^{1,∞}(□_m)} is at most the (m, L] layer sum at the
origin cube of scale m, by the same triangle inequality.
The L² gauge of the recentered shell, split at m.
Annular.valueL2_centeredShellUnitCube_le at the manuscript's own centering
constant (k_L − k_m)_{□_m}, with the mean-value tail expanded into layers.
The first summand is L-free.
The L-free value slot, at a caller-supplied tail gauge T.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The value slot bound, L-free.