G1Engine

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

The single-shell array engine behind both 𝒢₁ lanes

This module is the common engine: it takes such an array, together with a uniform Γ_σ tail for its entries and a deterministic reduction of the lane's bad event, and returns the lane's proportion tail in the consumer's shape. Both Appendix-D hypotheses are discharged inside:

• hmomL from the entries' Γ_σ tails and the normalizer (proved lintegral_rpow_le_one_of_array, stated at the two-index shape);
• hindep from (J1) alone (columnsIndep_of_shellColumn) — no separation geometry, no dimension restriction, and valid for every r ≥ 1.

What remains a caller obligation is the deterministic domination of the lane's bad event by the Appendix-D row sum. Because ScalesConcentration.Yk is a real tsum (which reads 0 off summability), that domination is supplied here in ℝ≥0∞ and converted on a full-measure set, exactly as the 𝒢₀ lane does: the two first moments are finite, so the rows are a.s. finite, and the enlargement Ev m ∪ N costs nothing (measure_scaleProp_le_of_null_enlargement).

References

• ABK26, l.ratio.of.good.scales.for.k.
• ABK26, p.concentration.for.scales and Appendix D.

1. The two-sided geometric row weight

theorem Algsuperdiff.Section4.Provider.Proportion.summable_wtRow {sprime : ℝ} (hs0 : 0 < sprime) (hs2 : 2 * sprime ≤ 1) (m : ℤ) : Summable fun (j : ℤ) => Probability.ScalesConcentration.wt sprime m j

theorem Algsuperdiff.Section4.Provider.Proportion.tsum_wtRow_le {sprime : ℝ} (hs0 : 0 < sprime) (hs2 : 2 * sprime ≤ 1) (m : ℤ) : ∑' (j : ℤ), Probability.ScalesConcentration.wt sprime m j ≤ 3 / sprime

2. The Appendix-D row of a two-index array, formed in ℝ≥0∞

noncomputable def Algsuperdiff.Section4.Provider.Proportion.rowGE {d : ℕ} (G : ℤ → ℤ → Section3.Cutoff.CutoffSample d → ℝ) (sprime : ℝ) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ENNReal

The two-sided Appendix-D row sum of a two-index array, formed in ℝ≥0∞ (total, no summability side condition).

Equations

• Algsuperdiff.Section4.Provider.Proportion.rowGE G sprime m omega = ∑' (j : ℤ), ENNReal.ofReal (Algsuperdiff.Section4.Probability.ScalesConcentration.wt sprime m j * G m j omega)

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_rowGE {d : ℕ} {G : ℤ → ℤ → Section3.Cutoff.CutoffSample d → ℝ} (hGm : ∀ (m j : ℤ), Measurable (G m j)) (sprime : ℝ) (m : ℤ) : Measurable (rowGE G sprime m)

theorem Algsuperdiff.Section4.Provider.Proportion.lintegral_rowGE_le {d : ℕ} (M : Section3.ABKModel d) {G : ℤ → ℤ → Section3.Cutoff.CutoffSample d → ℝ} {sigma sprime K : ℝ} (hsigma : 0 < sigma) (hK : 0 < K) (hs0 : 0 < sprime) (hs2 : 2 * sprime ≤ 1) (hGnn : ∀ (m j : ℤ) (omega : Section3.Cutoff.CutoffSample d), 0 ≤ G m j omega) (hGm : ∀ (m j : ℤ), Measurable (G m j)) (hGtail : ∀ (m j : ℤ), HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sigma) (G m j) K) (m : ℤ) : ∫⁻ (omega : Section3.Cutoff.CutoffSample d), rowGE G sprime m omega ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (3 / sprime * (HCPolySupport.IndependentSums.gammaMomentConst sigma * K))

The row has a finite first moment. Tonelli over the ℤ-row against the uniform Γ_σ tail of the entries and the summable geometric weights.

3. The null set on which the real row sum is the honest series

def Algsuperdiff.Section4.Provider.Proportion.goodRowG {d : ℕ} (G : ℤ → ℤ → Section3.Cutoff.CutoffSample d → ℝ) (sprime : ℝ) : Set (Section3.Cutoff.CutoffSample d)

The full-measure set on which every Appendix-D row of the array is finite.

Equations

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

theorem Algsuperdiff.Section4.Provider.Proportion.measure_compl_goodRowG {d : ℕ} (M : Section3.ABKModel d) {G : ℤ → ℤ → Section3.Cutoff.CutoffSample d → ℝ} {sigma sprime K : ℝ} (hsigma : 0 < sigma) (hK : 0 < K) (hs0 : 0 < sprime) (hs2 : 2 * sprime ≤ 1) (hGnn : ∀ (m j : ℤ) (omega : Section3.Cutoff.CutoffSample d), 0 ≤ G m j omega) (hGm : ∀ (m j : ℤ), Measurable (G m j)) (hGtail : ∀ (m j : ℤ), HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sigma) (G m j) K) : ↑(Section3.Cutoff.cutoffSampleLaw M) (goodRowG G sprime)ᶜ = 0

The enlargement's null set is null, by first moments alone: countably many rows, each with a finite expectation.

4. From the ℝ≥0∞ row to ScalesConcentration.Yk

theorem Algsuperdiff.Section4.Provider.Proportion.lt_Yk_of_lt_rowGE {d : ℕ} {G : ℤ → ℤ → Section3.Cutoff.CutoffSample d → ℝ} {sprime D lam : ℝ} (hD : 0 < D) (hlam : 0 ≤ lam) (m : ℤ) {omega : Section3.Cutoff.CutoffSample d} (hnn : ∀ (j : ℤ), 0 ≤ G m j omega) (hfin : rowGE G sprime m omega ≠ ⊤) (hlt : ENNReal.ofReal (D * lam) < rowGE G sprime m omega) : lam < Probability.ScalesConcentration.Yk (fun (m j : ℤ) (omega : Section3.Cutoff.CutoffSample d) => D⁻¹ * G m j omega) sprime m omega

The ℝ≥0∞-to-ℝ conversion of the Appendix-D row. On the finiteness set, a strict lower bound for the ℝ≥0∞ row is a strict lower bound for the real normalized row Yk.