Ycal

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The 𝒢₀ score field 𝒴_n and its Γ_{1/3} tail

ABK26, §4.1, steps l.good.scales.ratio.lambda, the per-annulus atom tail, display (b), and the 𝒴 tail:

max_{z ∈ 3^{k−2}ℤ^d ∩ (□_n∖□_{n−1})} (σ_{k−3}λ_{γ,2}^{-1}(z+□_{k−2};𝐚_{k−2}) − C_cg)_+
  ≤ 𝒪_{Γ_{1/3}} ( C(n−k+1)³ exp(−C^{−1}c⋆²γ^{−1}) ) ,

𝒴_n := γ^{-4} Σ_{k ≤ n} 3^{−¼γ(n−k)} (that maximum)
     ≤ 𝒪_{Γ_{1/3}} ( exp(−C^{−1}c⋆²γ^{−1}) ) .

Both are assembled here from three proved pieces: the per-atom tail (AtomTail.isBigOWith_cgExcess_of_state), the union bound (SeriesTail.isBigOWith_fmax) with the machine-computed lattice count (LatticeCount), and the countable generalized triangle inequality (SeriesTail.isBigOWith_wsum).

Deviations from the printed display

• The normalization γ^{-4} and the weight rate ¼γ are free parameters here: sprime is the rate, and the normalization is deliberately not baked into Ycal, because it is a lane prefactor of the downstream threshold, not a rescaling of the score field. The manuscript's instance is sprime = γ/4 and the normalization γ^{-4} ≍ Σ_j 3^{-¼γ j}(j+3)³, which is the value of the tsum appearing in the tail scale below. Establishing the closed form ≍ γ^{-4} for that sum is arithmetic, not structure, and is not done here.
• The k-series is formed in ℝ≥0∞ (YcalE), hence total, and Ycal is its .toReal. No a.s. finiteness is needed before 𝒴_n may be used, and the tail proved below is a statement about the total object.
• The summand reads the field at the inner scale 𝐚_{k−2}, a per-inner-scale truncation; this is the proved Localize.cgExcess at index k − 2, so the convention is the manuscript's.

References

• ABK26, l.good.scales.ratio.lambda.

1. The per-annulus maximum

noncomputable def Algsuperdiff.Section4.Provider.Proportion.annMax {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (n k : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ℝ

The lattice maximum of the 𝒢₀ bracket over the annulus □_n ∖ □_{n−1}, read at spacing 3^{k−2}. 0-floored, so total.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.Proportion.annMax_nonneg {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (n k : ℤ) (omega : Section3.Cutoff.CutoffSample d) : 0 ≤ annMax M Ccg n k omega

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_cgExcess {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (k : ℤ) (z : HCPolySupport.Vec d) : Measurable fun (omega : Section3.Cutoff.CutoffSample d) => Localize.cgExcess M Ccg (k - 2) z omega

The 𝒢₀ bracket at a fixed centre is measurable.

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_annMax {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (n k : ℤ) : Measurable (annMax M Ccg n k)

theorem Algsuperdiff.Section4.Provider.Proportion.isBigOWith_annMax {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) {A sigma : ℝ} (hsigma : 0 < sigma) (hA : 0 ≤ A) (hatom : ∀ (k : ℤ) (z : HCPolySupport.Vec d), HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sigma) (fun (omega : Section3.Cutoff.CutoffSample d) => Localize.cgExcess M Ccg (k - 2) z omega) A) (n k : ℤ) : HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sigma) (annMax M Ccg n k) (annulusPenalty d sigma (n - (k - 2)).toNat * A)

e.maxy.bound at the 𝒢₀ annulus. The per-atom Γ_σ tail lifts through the lattice maximum at the machine-computed penalty `annulusPenalty d σ (n − k

• 2), which at σ = 1/3is a cubic inn − k: the manuscript's C(n−k+1)³`.

2. The penalty at the manuscript's index σ = 1/3, in closed form

noncomputable def Algsuperdiff.Section4.Provider.Proportion.annulusPenaltyThird (d p : ℕ) : ℝ

The σ = 1/3 lattice penalty as a natural cube — the manuscript's C(n−k+1)³.

Equations

• Algsuperdiff.Section4.Provider.Proportion.annulusPenaltyThird d p = (1 + ↑d * (↑p + 1) * Real.log 3) ^ 3

theorem Algsuperdiff.Section4.Provider.Proportion.annulusPenalty_third (d p : ℕ) : annulusPenalty d (1 / 3) p = annulusPenaltyThird d p

theorem Algsuperdiff.Section4.Provider.Proportion.annulusPenaltyThird_pos (d p : ℕ) : 0 < annulusPenaltyThird d p

3. The geometric weight

noncomputable def Algsuperdiff.Section4.Provider.Proportion.weightThird (sprime : ℝ) (j : ℕ) : ℝ

The manuscript's discount 3^{−s'(n−k)}, written as a geometric power of 3^{−s'} in the offset j = n − k.

Equations

• Algsuperdiff.Section4.Provider.Proportion.weightThird sprime j = (3 ^ (-sprime)) ^ j

theorem Algsuperdiff.Section4.Provider.Proportion.weightThird_pos {sprime : ℝ} (j : ℕ) : 0 < weightThird sprime j

theorem Algsuperdiff.Section4.Provider.Proportion.weightThird_eq (sprime : ℝ) (j : ℕ) : weightThird sprime j = 3 ^ (-(sprime * ↑j))

The weight is the printed 3^{−s'(n−k)} at j = n − k.

4. Summability of the weighted penalties

theorem Algsuperdiff.Section4.Provider.Proportion.annulusPenaltyThird_le (d j : ℕ) : annulusPenaltyThird d (j + 2) ≤ (1 + 3 * ↑d * Real.log 3) ^ 3 * (↑j + 1) ^ 3

The annular penalty at a shifted index is bounded by a cubic polynomial.

theorem Algsuperdiff.Section4.Provider.Proportion.summable_weight_mul_annulusPenaltyThird (d : ℕ) {sprime A : ℝ} (hsprime : 0 < sprime) (hA : 0 ≤ A) : Summable fun (j : ℕ) => weightThird sprime j * (A * annulusPenaltyThird d (j + 2))

The canonical summability: the weighted lattice penalties are summable for every positive rate. This is what makes the 𝒴-series tail available; the manuscript performs the same estimate implicitly when it writes γ^{-4}.

5. The score field 𝒴_n

noncomputable def Algsuperdiff.Section4.Provider.Proportion.YcalE {d : ℕ} (M : Section3.ABKModel d) (Ccg sprime : ℝ) (n : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ENNReal

The 𝒢₀ score field 𝒴_n, formed in ℝ≥0∞. The manuscript's normalization γ^{-4} is deliberately not included; the rate s' is the manuscript's ¼γ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section4.Provider.Proportion.Ycal {d : ℕ} (M : Section3.ABKModel d) (Ccg sprime : ℝ) (n : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ℝ

The real-valued score field.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.Proportion.Ycal_nonneg {d : ℕ} (M : Section3.ABKModel d) (Ccg sprime : ℝ) (n : ℤ) (omega : Section3.Cutoff.CutoffSample d) : 0 ≤ Ycal M Ccg sprime n omega

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_Ycal {d : ℕ} (M : Section3.ABKModel d) (Ccg sprime : ℝ) (n : ℤ) : Measurable (Ycal M Ccg sprime n)

theorem Algsuperdiff.Section4.Provider.Proportion.le_YcalE {d : ℕ} (M : Section3.ABKModel d) (Ccg sprime : ℝ) (n : ℤ) (omega : Section3.Cutoff.CutoffSample d) (j : ℕ) : ENNReal.ofReal (weightThird sprime j * annMax M Ccg n (n - ↑j) omega) ≤ YcalE M Ccg sprime n omega

Every single weighted annulus maximum is below 𝒴_n — unconditionally, in ℝ≥0∞. This is the hatom half of the domination chain, available with no summability hypothesis.

theorem Algsuperdiff.Section4.Provider.Proportion.isBigOWith_Ycal {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) {sigma sprime A : ℝ} {a : ℕ → ℝ} (hsigma : 0 < sigma) (hA : 0 ≤ A) (hatom : ∀ (k : ℤ) (z : HCPolySupport.Vec d), HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sigma) (fun (omega : Section3.Cutoff.CutoffSample d) => Localize.cgExcess M Ccg (k - 2) z omega) A) (hapos : ∀ (j : ℕ), 0 < a j) (hdom : ∀ (j : ℕ), annulusPenalty d sigma (j + 2) * A ≤ a j) (hsum : Summable fun (j : ℕ) => weightThird sprime j * a j) (n : ℤ) : HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sigma) (Ycal M Ccg sprime n) (HCPolySupport.IndependentSums.gammaTriangleConst sigma * ∑' (j : ℕ), weightThird sprime j * a j)

The 𝒴-tail.

𝒴_n ≤ 𝒪_{Γ_σ} ( gammaTriangleConst σ · Σ_j 3^{−s'j} a_j )

from the per-atom tail alone. a is any sequence of positive scales dominating the penalised atom scales annulusPenalty d σ (j+2) · A, with the weighted series summable; the canonical choice a_j = A · annulusPenaltyThird d (j+2) at σ = 1/3 is admissible by annulusPenalty_third and summable_weight_mul_annulusPenaltyThird.

The bound is uniform in n: the manuscript's 𝒴_n ≤ 𝒪_{Γ_{1/3}}(exp(−C^{−1}c⋆²γ^{−1})) is this statement with A = exp(−(C_cg^{−1}E^{−2}γ^{−1})) factored out of the tsum.