StepTwoDTwo #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Step 2 of the kicking lemma: the D₂ half of e.kick.Dees.Dees #
ABK26, §4.2, l.minimal.scale.sep, Step 2. The manuscript's D₂ is
D₂(k) = c⋆^{−1/2} s^{−1} γ^{1/2} Σ_{l ≥ k} 3^{(2−γ)k} ‖∇j_l‖_{W^{1,∞}(□_k)}
and Step 2 proves the display e.D2k.kicked
avsum_{k=n}^m D₂(k) ≤ C c⋆^{−1/2}s^{−1}γ^{1/2}
+ 𝒪_{Γ₂}( C c⋆^{−1/2}s^{−1}γ^{1/2}(m−n)^{−1/2} ) .
The three ingredients #
- the window rearrangement —
cesaro_gradInner_le; - the layer gradient tail — proved in
LayerBrackets; - the Step-2 conclusion —
exists_stepTwo_kickedand its prefactor formexists_D2k_kicked.
The rearrangement, and the two corrections it respects #
The manuscript rearranges Σ_{k=n}^m Σ_{l≥k} into Σ_{l≥n} Σ_{k=n}^{m∧l} and
then majorizes the inner k-sum. Two corrections are built into the route:
- the printed majorant
3^{(2−γ)(m∧l)}‖∇j_l‖_{W^{1,∞}(□_l)}enlarges the cube, and the volume-normalized gauge is not monotone in the cube, so that step is false as printed forl > m. Here the comparison is always□_kversus□_lat the same centre with both3^{(2−γ)·}weights attached (LayerBrackets.gradCross_le), which is the honest form; the printed majorant is never formed. - the shell weight that survives the comparison is
1 − γ, not2 − γ. Sinceγ ≤ 1/4(frozenShellLawPrefix.gamma_le_quarter), the rate is at least3/4and the geometric closuregeomTailConstis bounded by an absolute numeral; noγ-dependence enters the output constant.
The window arithmetic itself is the carrier-free
Algsuperdiff.Probability.window_geom_tail_rearrange_le, applied at
α = 1 − γ.
Why the endpoint is almost sure #
The manuscript's inner sum is an infinite series over the field index l; the
anchor forms it in ℝ≥0∞. The real reading .toReal is dominated by the
majorant series only where that series converges, and convergence holds almost
surely — proved, not assumed, from the per-layer first moments
(LayerBrackets.ae_wsumE_ne_top). The anchor's clause (i) is itself an almost
sure statement, so nothing is lost.
Independence #
Step 2 applies p.concentration to the layer family {3^{(2−γ)l}‖∇j_l‖},
which is genuinely independent: each layer is a functional of its own shell and
the single-shell sigma-fields are mutually independent
(LayerBrackets.iIndepFun_gradLayer). The manuscript's own justification ("by
the independence of the sequence {j_n}") is exactly this.
References #
- ABK26,
l.minimal.scale.sepStep 2.
1. The (1−γ) rate #
On the frozen window γ ≤ 1/4 the Step-2 rate is at least 3/4.
The geometric closure constant is antitone in the rate.
The absolute bound on the Step-2 geometric closure: it is at most the
numeral geomTailConst (3/4), with no γ left in it.
2. The anchor-shaped inner sum of D₂(k) #
The field indices l ≥ k, enumerated by the offset l − k ∈ ℕ.
Equations
Instances For
The inner sum of D₂(k), formed in ℝ≥0∞ exactly as the anchor
annular_decomposition forms it: Σ_{l ≥ k} 3^{(2−γ)k}‖∇j_l‖_{W^{1,∞}(□_k)}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The real-valued inner sum; at the samples where the ℝ≥0∞ sum diverges this
is 0, which only strengthens every upper-tail statement about it.
Equations
Instances For
The inner sum as a SeriesTail weighted series: the weight is constant in
the offset and the atom is the cross-scale gauge.
3. The majorant layer series #
The geometric gradient weight at one minimal-scale depth.
Instances For
The Step-2 majorant series at scale k: the geometrically weighted sum
of the layer brackets at their own scales, from k upwards. This is the
right-hand side of the manuscript's rearranged display.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The majorant series in the real tsum spelling consumed by the window
arithmetic of Algsuperdiff.Probability.WindowRearrange.
The pointwise majorization, in ℝ≥0∞, unconditional. This is the
manuscript's cube comparison summed over the field indices.
The real form of the majorization, at the samples where the majorant series converges.
4. Almost sure convergence of the majorant series #
The per-layer first moment of the Step-2 layer bracket.
The majorant series converges almost surely, at every scale. Proved from the per-layer first moments; the manuscript never states the convergence and never needs to, because it is automatic.
5. The Step-2 window rearrangement #
The Step-2 window rearrangement. At every sample point where the majorant series converges,
Σ_{k=n}^m (inner sum of D₂(k)) ≤ Cgeo ( Σ_{l=n}^m Y_l + Σ_{p≥0} 3^{−(1−γ)p} Y_{m+1+p} )
with Cgeo = geomTailConst (1−γ) = (1 − 3^{−(1−γ)})⁻¹ and Y_l the layer
bracket at its own scale.
6. The Γ₂ tail of the off-window series #
The off-window layer series has a Γ₂ tail at a constant amplitude:
Σ_{l≥m} 3^{(2−γ)(m−l)}Y_l ≤ 𝒪_{Γ₂}(C). This is the e.Gamma.sigma.triangle
step of Step 2, at the proved geometric-weight closure
Algsuperdiff.Probability.weightedTsum_isBigOWith (L4); no pointwise
summability of the layer series is assumed.
7. The Step-2 conclusion #
The fluctuation constant of Step 2, in units of the D₂ prefactor. Both
constants are absolute numerals: no γ, no s, no dimension.
Equations
- One or more equations did not get rendered due to their size.
Instances For
For a window n < m, the Cesàro average of the inner sums of D₂ splits into
a deterministic level and a Γ₂ fluctuation of scale stepTwoConst · (m−n)^{−1/2}.
e.D2k.kicked, at an arbitrary nonnegative prefactor. At pref = c⋆^{−1/2}s^{−1}γ^{1/2} — the prefactor the annular decomposition puts in front
of the inner sum — this is the printed display
avsum_{k=n}^m D₂(k) ≤ C c⋆^{−1/2}s^{−1}γ^{1/2}
+ 𝒪_{Γ₂}( C c⋆^{−1/2}s^{−1}γ^{1/2}(m−n)^{−1/2} )
with C = max(stepTwoDetConst, stepTwoConst), both absolute numerals. The
prefactor is kept abstract so that the final stitch may supply it in whatever
spelling the D-decomposition delivers.