StepThreeRearrange #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The Step-3 window rearrangement #
ABK26, §4.2, l.minimal.scale.sep, Step 3. The manuscript's D₃(k) inner
object is the doubly indexed sum
Σ_{l ≤ k} 3^{−α(k−l)} Σ_{i = l−1}^{k} 3^{(2−γ)i} max_{z ∈ 3^iℤ^d ∩ □_k} ‖j_i‖_{W^{2,∞}(z+□_i)}
with α = s/4, and Step 3 rearranges it into the two channels of
StepThreeDThree:
Σ_{k=n}^m (inner) ≤ K₀ ( Σ_{i=n}^m V_i + Σ_{r≥0} 3^{−α(k−n+r+1)}-weighted H_r ) ,
K₀ = 3^α(1−3^{−α})⁻¹ .
The reordering is an inequality, and it is here #
The manuscript performs the (l,i) reordering as an identity. At the ℝ≥0∞
carrier the reordering is available as a genuine Tonelli identity, but the
collapse of the inner l-sum into the coefficient K₀·3^{−α(k−i)} is an
inequality (the honest coefficient is Σ_{p ≥ q−1} 3^{−αp}, which is at most
3^α(1−3^{−α})⁻¹3^{−αq}, with equality only for q ≥ 1).
Why ℝ≥0∞ #
Every sum here is formed in ℝ≥0∞, exactly as the anchor
annular_decomposition forms the D₃ term. In ℝ≥0∞ the depth swap needs no
summability hypothesis at all: ENNReal.tsum_comm and
ENNReal.tsum_le_of_sum_range_le are unconditional. Only the very last step —
reading the bound in ℝ — needs the
majorant to be finite, and that holds almost surely by the per-layer first
moments (ae_wsumE_ne_top), which is proved rather than assumed.
References #
- ABK26,
l.minimal.scale.sepStep 3.
1. The D₃(k) inner object #
The outer scales l ≤ k, enumerated by the depth k − l ∈ ℕ.
Equations
Instances For
The inner object of D₃(k), formed in ℝ≥0∞ at the ℓ¹ reading of the
anchor's D₃ term.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The real-valued inner object; at the divergent samples this is 0, which only
strengthens every upper-tail statement about it.
Equations
- Algsuperdiff.Section4.Provider.MinimalScale.hessInner M alpha k omega = (Algsuperdiff.Section4.Provider.MinimalScale.hessInnerE M alpha k omega).toReal
Instances For
The lattice maximum at the layer k − q, enumerated downwards from the outer
cube k.
Equations
- Algsuperdiff.Section4.Provider.MinimalScale.hessDown M k q omega = Algsuperdiff.Section4.Provider.Proportion.scoreG1b M k (k - ↑q) omega
Instances For
The layer block at depth p: the finite inner sum of the manuscript's
display, enumerated downwards from k.
Equations
- Algsuperdiff.Section4.Provider.MinimalScale.hessBlock M k p omega = ∑ q ∈ Finset.range (p + 2), Algsuperdiff.Section4.Provider.MinimalScale.hessDown M k q omega
Instances For
The inner object as a SeriesTail weighted series over the depth.
2. The depth-collapse coefficient #
3. The depth swap #
The depth swap. The manuscript's inner double sum is at most
K₀ = 3^α(1−3^{−α})⁻¹ times the single geometrically weighted sum of the lattice
maxima, at every sample point, unconditionally.
4. The window split #
Over the window [n,m] the manuscript's D₃ inner objects are bounded, in
ℝ≥0∞ and at every sample point, by K₀ = 3^α(1−3^{−α})⁻¹ times the sum of
the two channels of StepThreeDThree.
5. Almost sure finiteness of the below-window channel #
The below-window channel converges almost surely, at every window. Proved
from its per-depth first moments, which come from the per-depth Γ₂ tails.
The real form of the rearrangement: almost surely, the window sum of the
manuscript's D₃ inner objects is below K₀ times the two channels.
6. The D₃ bound: e.D3k.kicked at the manuscript's own D₃ #
e.D3k.kicked, at an arbitrary nonnegative prefactor and at the
manuscript's own D₃ inner object. At pref = c⋆^{−1/2}s^{−1}γ^{1/2} and α = s/4 the two output scales are, by stepThree_det_closed and
stepThree_fluc_closed,
deterministic : C c⋆^{−1/2}s^{−7/2}γ^{1/2} (the printed level)
fluctuation : C c⋆^{−1/2}s^{−9/2}γ^{1/2}(m−n)^{−1/2} (the E5 finding)
i.e. the printed display with the fluctuation exponent corrected from s^{−7/2}
to s^{−9/2}.