SmallWaves #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Step 2 of l.ratio.of.good.scales.for.k: the small-waves lane #
This module realizes the 𝒢₁b half of l.ratio.of.good.scales.for.k: the
genuinely two-index Appendix-D array X_{m,k}, its reduction of the second
𝒢₁ condition, and the resulting proportion tail
e.small.waves.scale.counting.
The array really is two-index, and that is not a problem here #
- the array
arrayG1bis written at the honest two-index shape, which is also the shape of the provedp.concentration.for.scales(its array isX: ℤ → ℤ → Ω → ℝ, andcolArrayis a derived special case), so no new concentration inequality is needed; - the independence hypothesis is discharged by
columnsIndep_of_shellColumn, the genuine two-index producer: columnkreads the single layerj_k, and the row index enters only through deterministic data (the discount and the deterministic centre set), so (J1) gives independence at everyr ≥ 1.
The gap in e.Xmk.pedant.bound, paid explicitly #
The graph records that the lattice-max penalty ≍ C(d)(m-k)^{1/σ} grows with
m - k and is absorbed by nothing displayed except the discount, so the printed
uniform constant implicitly consumes sup_j (1+j)3^{-sj/8} ≍ Cs^{-1} — one power
of s^{-1} beyond the s^{-2} shown. Here that absorption is
SmallWavesArith.rpow_mul_penalty_sq_le, and the resulting uniform amplitude is
smallWaveScale, explicitly 8 s^{-1}(1 + 2d log 3) times the squared atom
amplitude.
References #
- ABK26,
l.ratio.of.good.scales.for.k, Step 2. - ABK26,
d.good.event.for.lambda, (the second𝒢₁condition).
0. A Γ_σ tail for the identically zero observable #
1. The 𝒢₁b score field: the lattice maximum at scale k inside □_m #
The 𝒢₁b score field: 3^{(2-γ)k} max_{z ∈ 3^kℤ^d ∩ □_m} ‖j_k‖_{W^{2,∞}(z+□_k)}, as the 0-floored maximum over the explicit lattice
Finset.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The score field reads exactly one shell — the (J1) input of the independence hypothesis, at the genuinely two-index shape.
e.maxy.bound at the 𝒢₁b lattice cube. The per-centre Γ₂ tail of
atomG1b, lifted through the maximum at the machine-computed union-bound
penalty (1 + d(m-k+1) log 3)^{1/2}.
2. The two-index Appendix-D array #
The 𝒢₁b Appendix-D array, genuinely two-index: X_{m,k} = 3^{-s(m-k)/8}(3^{(2-γ)k}max_{z ∈ 3^kℤ^d ∩ □_m}‖j_k‖_{W^{2,∞}(z+□_k)})² for k ≤ m, and 0 otherwise.
Equations
Instances For
The uniform Γ₁ amplitude of the two-index array: the squared atom
amplitude, times the 8 s^{-1}(1 + 2d log 3) produced by absorbing the growing
lattice-max penalty into the discount.
Equations
Instances For
e.Xmk.pedant.bound, in tail form, with the accounting made explicit.
Every entry of the two-index array has a Γ₁ upper tail at the uniform
amplitude smallWaveScale d s. The three inputs are: the per-centre Γ₂ tail
of atomG1b, the union-bound penalty over the growing lattice cube, and
e.powerofGammasigma (squaring moves σ = 2 to σ = 1).
3. The reduction of the second 𝒢₁ condition #
The inner block of 𝒢₁b at one scale is below the squared score field.
The 𝒢₁b reduction, against the honest two-index array. The left side of
the second 𝒢₁ condition at row m is at most g1bConst s times the
Appendix-D row sum of arrayG1b at rate s/8. Two steps: the interchange (an
identity in ℝ≥0∞) and the geometric partial weight (the manuscript's
4s^{-1}).
Off the lane's good event the ℝ≥0∞ row exceeds the scaled threshold.