G2Concentration

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

The 𝒢₂ lane: r-dependence of the atoms X_j

ABK26, §4.1, l.ratio.of.good.scales.for.mathcal.E: the Appendix-D independence hypothesis of the lane's atoms.

r-dependence

columnsIndep_Xcal is the 𝒢₂ twin of Concentration.columnsIndep_Ycal, and it runs on exactly the same geometry: the atom X_j reads only truncation levels ≤ j − 2 and only on annulusRegion d j (G2Locality.measurable_Xcal_annulusRegion_local, a statement with no hypotheses), so the varying-level producer Probability.iIndepFun_of_local_cutoffSample applies at the separation supplied by Probability.separatedBy_annulusRegion_of_gap at the truncation offset c = 2.

Scope

Provider material: proved local helpers.

References

• ABK26, l.ratio.of.good.scales.for.mathcal.E.

1. r-dependence of the 𝒢₂ atoms

theorem Algsuperdiff.Section4.Provider.Proportion.columnsIndep_Xcal {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (D : ℝ) {r : ℕ} (hr1 : 1 ≤ r) (hr : 3 + 2 * 3 ^ (1 - 2) * √↑d ≤ 3 ^ r) : Probability.ScalesConcentration.ColumnsIndep (↑(Section3.Cutoff.cutoffSampleLaw M)) (xcalArray M s D) r

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

The atoms X_j 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 statement is at the general r, so no dimension restriction enters this file.

Unlike the 𝒢₀ lane, the locality input needs no premise at all: the 𝒢₂ locality endpoint measurable_Xcal_annulusRegion_local is unconditional.