Concentration

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

The 𝒢₀ lane: unit moments and r-dependence

ABK26, §4.1, l.good.scales.ratio.lambda, the moment and p choice, the two-dependence step and the display e.no.bad.scales.applied.for.lambdas.

What is assembled

1. lintegral_rpow_le_one_Ycal — the Appendix-D moment hypothesis E[(D^{-1}𝒴_n)^p] ≤ 1 from the 𝒴-tail, via the proved IndicatorArray discharger. This is's "by taking p := exp(K^{-1}c⋆²γ^{-1}) with K(d) large enough, we obtain E[𝒴_n^p] ≤ 1"; the numerical step of that sentence is the hypothesis hnorm (gammaMomentConst σ · p^{1/σ} · K ≤ D), which is exactly the manuscript's own "for K(d) large enough".

2. columnsIndep_Ycal — the 2-dependence assertion, at the honest r(d). The theorem below is stated at the general r, so no dimension restriction enters this file; d ≤ 81 gives r = 2, and larger d is covered by separatedBy_annulusRegion_of_gap at the larger r(d). The cost of r > 2 is absorbed in the rate.

Scope

Provider material: proved local helpers.

References

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

noncomputable def Algsuperdiff.Section4.Provider.Proportion.ycalArray {d : ℕ} (M : Section3.ABKModel d) (Ccg sprime D : ℝ) : ℤ → ℤ → Section3.Cutoff.CutoffSample d → ℝ

The Appendix-D array of the 𝒢₀ lane, X_{k,n} = D^{-1}𝒴_n. The normalizer D carries the manuscript's γ^{-4}.

Equations

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

@[simp]

theorem Algsuperdiff.Section4.Provider.Proportion.ycalArray_apply {d : ℕ} (M : Section3.ABKModel d) (Ccg sprime D : ℝ) (k j : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ycalArray M Ccg sprime D k j omega = D⁻¹ * Ycal M Ccg sprime j omega

1. The Appendix-D unit moments

theorem Algsuperdiff.Section4.Provider.Proportion.lintegral_rpow_le_one_Ycal {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) {sigma sprime p D K : ℝ} (hsigma : 0 < sigma) (hK : 0 < K) (hp : 1 ≤ p) (hD : 0 < D) (htail : ∀ (n : ℤ), HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sigma) (Ycal M Ccg sprime n) K) (hnorm : HCPolySupport.IndependentSums.gammaMomentConst sigma * p ^ sigma⁻¹ * K ≤ D) (k j : ℤ) : ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (ycalArray M Ccg sprime D k j omega ^ p) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ 1

E[(D^{-1}𝒴_n)^p] ≤ 1. The Appendix-D moment hypothesis e.Xk.p.moment.twosided, in its honest ∫⁻ reading, for the column array of the 𝒴-atoms.

hnorm is the manuscript's own numerical step: at σ = 1/3 the moment growth is gammaMomentConst σ · p³ · K makes it ≤ 1 "by taking p:= exp(K^{-1}c⋆²γ^{-1}) with K(d) large enough" — i.e. by the smallness of the tail scale K against p³.

3. r-dependence of the 𝒴_n

theorem Algsuperdiff.Section4.Provider.Proportion.columnsIndep_Ycal {d : ℕ} (M : Section3.ABKModel d) (Ccg sprime D : ℝ) {r : ℕ} (hr1 : 1 ≤ r) (hr : 3 + 2 * 3 ^ (1 - 2) * √↑d ≤ 3 ^ r) (hloc : ∀ (n : ℤ), Measurable (Ycal M Ccg sprime n)) : Probability.ScalesConcentration.ColumnsIndep (↑(Section3.Cutoff.cutoffSampleLaw M)) (ycalArray M Ccg sprime D) r

The Appendix-D independence hypothesis e.independent.columns.twosided for the 𝒢₀ lane.

The atoms 𝒴_n are r-dependent for every r ≥ 1 with 3 + 2·3^{1−2}√d ≤ 3^r, i.e. 3 + (2/3)√d ≤ 3^r: the annuli at index gap ≥ r are separated at the shared-shell threshold √d·3^{min(n−2, n'−2)}, which is exactly what the varying-level producer consumes. No dimension restriction is imposed here — r is a parameter, and d ≤ 81 gives the manuscript's r = 2.