LayerBrackets #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The Step-2 and Step-3 layer brackets of the kicking lemma #
ABK26, §4.2, l.minimal.scale.sep, Steps 2 and 3. Steps 2 and 3 both run on
layer variables: the 3^{(2−γ)·}-weighted volume-normalized shell gauges
Y_l := 3^{(2−γ)l} ‖∇j_l‖_{W^{1,∞}(□_l)} (Step 2)
G_i^k := 3^{(2−γ)i} max_{z ∈ 3^iℤ^d ∩ □_k} ‖j_i‖_{W^{2,∞}(z+□_i)} (Step 3)
(Step 2's display is ABK26, Step 3's is.)
together with the per-layer Γ₂ tails Y_l ≤ 𝒪_{Γ₂}(C),
3^{(2−γ)i}‖j_i‖_{W^{2,∞}(z+□_i)} ≤ 𝒪_{Γ₂}(C) and the lattice maximum G_i^k ≤ 𝒪_{Γ₂}(C(k+1−i)^{1/2}) (e.maxy.bound).
The layer variables are the §4.1 atoms, not new objects #
The §4.1 proportion lane already renders both brackets at exactly this repository's carrier, and both per-layer tails are proved there:
Proportion.atomG1a M l = 3^{(2−γ)l}‖∇j_l‖_{W^{1,∞}(□_l)}withProportion.isBigOWith_atomG1aat amplitude1;Proportion.atomG1b M i z = 3^{(2−γ)i}‖j_i‖_{W^{2,∞}(z+□_i)}withProportion.isBigOWith_atomG1bat the amplitudeatomG1bScale, uniformly in the base pointz;Proportion.scoreG1b M k i = fmaxofatomG1b M i (3^i v)overv ∈ latticeCubeFinset d i k, withProportion.isBigOWith_scoreG1bat the machine-computed union-bound penaltyannulusPenalty d 2 (k−i).toNat.
No layer variable is therefore defined here.
The same tail at every translate, not weakened #
e.maxy.bound needs one common amplitude at every lattice centre.
The ℝ≥0∞ reconciliation #
The manuscript's D₂(k) and D₃(k) are sums over infinitely many layers. {n // n ≤ m}), which is total; the real-valued reading is .toReal, which is 0
at the divergent samples and hence only strengthens every upper-tail statement.
Two services are needed downstream and proved here:
wsum_eq_tsum— for nonnegative layers theℝ≥0∞-formed weighted seriesProportion.wsumequals the realtsumat every sample point (both are the junk value0exactly when the family is not summable). This is what lets the carrier-free window arithmetic ofAlgsuperdiff.Probability.WindowRearrange(stated for realtsums) act on the anchor-shaped objects.ae_wsumE_ne_top— a weighted layer series with summable weighted first moments is almost surely finite. This is the honest discharge of the convergence side condition that the manuscript never mentions: it is proved from the per-layer tails, never assumed.
References #
- ABK26,
l.minimal.scale.sep, Step 2 and Step 3. - ABK26,
e.maxy.bound,e.Gamma.sigma.triangle.
1. The layer gradient tail #
This is Proportion.score_le_wt_mul_atomG1a at sprime = 1 − γ, with the row
weight wt unfolded. It never enlarges the cube: the comparison is between
□_k and □_l at the same centre with both 3^{(2−γ)·} prefactors
attached, and the printed majorant 3^{(2−γ)(m∧l)}‖∇j_l‖_{W^{1,∞}(□_l)} is
never formed.
2. The layer Hessian tail #
3. The Step-3 lattice maximum (e.maxy.bound) #
The dimension-dependent amplitude for the lattice maximum estimate.
Equations
Instances For
e.maxy.bound at the Step-3 lattice cube:
max_{z ∈ 3^iℤ^d ∩ □_k} 3^{(2−γ)i}‖j_i‖_{W^{2,∞}(z+□_i)} ≤ 𝒪_{Γ₂}(C(k+1−i)^{1/2})
at C = latticeMaxAmp d, for every i ≤ k. The maximum is
Proportion.scoreG1b M k i, the 0-floored maximum over the explicit lattice
Finset; the tail is the proved Proportion.isBigOWith_scoreG1b with its
union-bound penalty put into the manuscript's √-shape. The amplitude is
exactly the summand shape consumed by
Algsuperdiff.Probability.sum_windowAmp_le and
Algsuperdiff.Probability.sum_headAmp_le.
4. Layer independence across shells #
The Step-2 layer family is independent ("by the independence of the
sequence {j_n}"). Every layer bracket is a functional of its own shell, and
the single-shell sigma-fields are mutually independent under the cutoff sample
law (Proportion.iIndep_shellSigma, the proved form of the frozen
ShellLawPrefix.independent).
The Step-3 in-window layer family is independent. A weighted finite sum
of lattice maxima at the fixed inner scale i over outer cubes k is a
functional of the shell j_i alone, so the family is independent across i.
The weights and the outer window are arbitrary: they enter only deterministically.
5. First moments from the per-layer tails #
A nonnegative variable with a Γ_σ upper tail has a first moment bounded by
gammaMomentConst σ times its scale. This is e.moments.OGamma2 in the form
Steps 2 and 3 consume; the two-sided IsBigO needed by the moment lemma is the
one-sided tail, because the variable is nonnegative.
A nonnegative variable with a Γ_σ upper tail is integrable.
6. The ℝ≥0∞ / ℝ reconciliation of an infinite layer sum #
The ℝ≥0∞-formed weighted layer series is the real tsum. For
nonnegative layers and nonnegative weights the two readings agree at every
sample point: where the family is summable both are the sum, and where it is not
both are the junk value 0 (ℝ≥0∞ sum ⊤, hence .toReal = 0).
This is the bridge that lets the carrier-free real window arithmetic of
Algsuperdiff.Probability.WindowRearrange act on the anchor-shaped ℝ≥0∞
objects.
A weighted layer series with summable weighted first moments is almost
surely finite. This is the honest discharge of the convergence side condition
that the manuscript never states: ∫⁻ ∑'_j c_j T_j = ∑'_j c_j ∫ T_j by Tonelli,
which is finite, so the ℝ≥0∞ series is finite almost everywhere. Only the
per-layer first moments enter, and those come from the per-layer Γ₂ tails.