G2RowConversion

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

The 𝒢₂ row: from the manuscript's one-sided ℝ≥0∞ sum to Appendix D's

two-sided real sum

ABK26, §4.1, l.ratio.of.good.scales.for.mathcal.E Step 4 reconciled with Appendix D's row (e.Yk.def.twosided).

This module supplies the conversion, exactly as RowSumFinite does for the 𝒢₀ lane and by the same device:

1. lintegral_XcalE_le — Tonelli over the inner series defining X_j, with the per-annulus two-term displays of G2AtomTail.isTwoTermBigOWith_errorAnnMax at p = 1. The bound xcalMoment is uniform in j: the Step-1 amplitudes depend on j − n, not on j.
2. lintegral_XrowTwoE_le — Tonelli again over the ℤ-row, with the geometric weight sum Σ_{j ∈ ℤ} 3^{−¼s|m−j|} ≤ 12/s.
3. measure_compl_goodRowSetG2 — the two finite expectations make the countable families {X_j = ∞} and {row_m = ∞} null.
4. XrowE_le_XrowTwoE — on the good set the one-sided row sits below the two-sided one (the inequality is in the manuscript's favour: the j > m rows are nonnegative).
5. lt_Yk_of_notMem_eventG2 — the deterministic half of the hreduce slot of the Appendix-D concentration interface, entered through G2Score's exact event characterization.

Everything is a first-moment computation; no Borel--Cantelli is used, and the null set is paid for by RowSumFinite.measure_scaleProp_le_of_null_enlargement.

Scope

Provider material: proved local helpers. hcube is a conditional A obligation, discharged at the caller by G2CubeBound.

References

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

1. Two small ℝ≥0∞ devices

2. Measurability of the 𝒢₂ atom in both readings

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_XcalE {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (j : ℤ) : Measurable (XcalE M s j)

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_XcalE_toReal {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (j : ℤ) : Measurable fun (omega : Section3.Cutoff.CutoffSample d) => (XcalE M s j omega).toReal

3. The first moment of the 𝒢₂ atom

noncomputable def Algsuperdiff.Section4.Provider.Proportion.xcalMoment (d : ℕ) (s A1 A2 : ℝ) : ℝ

The uniform first-moment majorant of the 𝒢₂ atom X_j. The two Step-2 weighted penalty series, weighted by the moment constants of the two Orlicz lanes. It does not depend on j.

Equations

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

theorem Algsuperdiff.Section4.Provider.Proportion.xcalMoment_nonneg (d : ℕ) (s A1 A2 : ℝ) : 0 ≤ xcalMoment d s A1 A2

theorem Algsuperdiff.Section4.Provider.Proportion.lintegral_ofReal_le_of_twoTerm {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {X : Omega → ℝ} {sigma1 sigma2 A1 A2 : ℝ} (hs1 : 0 < sigma1) (hs2 : 0 < sigma2) (hX0 : ∀ (omega : Omega), 0 ≤ X omega) (h : Section3.Probability.IsTwoTermBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma1) (HCPolySupport.IndependentSums.gammaSigma sigma2) X A1 A2) : ∫⁻ (omega : Omega), ENNReal.ofReal (X omega) ∂mu ≤ ENNReal.ofReal (HCPolySupport.IndependentSums.gammaMomentConst sigma1 * A1 + HCPolySupport.IndependentSums.gammaMomentConst sigma2 * A2)

The p = 1 case of the two-term moment engine. A nonnegative random variable with a two-term weak-Orlicz display has first moment at most the sum of the two lanes' one-term moments.

theorem Algsuperdiff.Section4.Provider.Proportion.lintegral_XcalE_le {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {A1 A2 : ℝ} (hcube : ∀ (n : ℤ), Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Support.annularErrorObservable M n s) A1 A2) (j : ℤ) : ∫⁻ (omega : Section3.Cutoff.CutoffSample d), XcalE M s j omega ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (xcalMoment d (↑s) A1 A2)

E[X_j] ≤ xcalMoment, by Tonelli over the inner series. Uniform in j.

4. The two-sided Appendix-D row, formed in ℝ≥0∞

noncomputable def Algsuperdiff.Section4.Provider.Proportion.XrowTwoE {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ENNReal

The Appendix-D row of the 𝒢₂ atoms, formed in ℝ≥0∞. Two-sided, matching ScalesConcentration.Yk at the 𝒢₂ lane rate s' = ¼s, and total. The manuscript's one-sided row XrowE sits below it.

Equations

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

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_XrowTwoE {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (m : ℤ) : Measurable (XrowTwoE M s m)

theorem Algsuperdiff.Section4.Provider.Proportion.lintegral_XrowTwoE_le {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {A1 A2 : ℝ} (hs1 : ↑s ≤ 1) (hcube : ∀ (n : ℤ), Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Support.annularErrorObservable M n s) A1 A2) (m : ℤ) : ∫⁻ (omega : Section3.Cutoff.CutoffSample d), XrowTwoE M s m omega ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (12 / ↑s * xcalMoment d (↑s) A1 A2)

E[Y_m] < ∞, by Tonelli over the ℤ-row.

5. The null set of the enlargement

def Algsuperdiff.Section4.Provider.Proportion.goodRowSetG2 {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) : Set (Section3.Cutoff.CutoffSample d)

The full-measure set on which the 𝒢₂ Appendix-D row is the honest series. Both the inner series defining each X_j and the ℤ-row of the X_j are finite there; off it the real tsum carries no information.

Equations

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

theorem Algsuperdiff.Section4.Provider.Proportion.measure_compl_goodRowSetG2 {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {A1 A2 : ℝ} (hs1 : ↑s ≤ 1) (hcube : ∀ (n : ℤ), Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Support.annularErrorObservable M n s) A1 A2) : ↑(Section3.Cutoff.cutoffSampleLaw M) (goodRowSetG2 M s)ᶜ = 0

The enlargement's null set is null.

6. The row conversion and the Appendix-D reduction

theorem Algsuperdiff.Section4.Provider.Proportion.XrowE_le_XrowTwoE {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (m : ℤ) {omega : Section3.Cutoff.CutoffSample d} (hfin : ∀ (j : ℤ), XcalE M s j omega ≠ ⊤) : XrowE M s m omega ≤ XrowTwoE M s m omega

The ℝ≥0∞ one-sided row is below the real two-sided row, on the set where the atoms are finite. This is the reconciliation of the manuscript's Σ_{j ≤ m} with Appendix D's Σ_{j ∈ ℤ}, the inequality being in the manuscript's favour: the j > m rows are nonnegative.

theorem Algsuperdiff.Section4.Provider.Proportion.lt_Yk_of_notMem_eventG2 {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {ep D : ℝ} (hD : 0 < D) (m : ℤ) {omega : Section3.Cutoff.CutoffSample d} (hgood : omega ∈ goodRowSetG2 M s) (hnot : omega ∉ Support.eventG2 M m s ep) : D⁻¹ * (ep ^ 2 / ↑s) < Probability.ScalesConcentration.Yk (xcalArray M s D) (↑s / 4) m omega

The Appendix-D reduction of 𝒢₂, off the null set. Off 𝒢₂(m;s,ε) — and off the null set of goodRowSetG2 — the Appendix-D row sum of the normalized atoms exceeds D^{-1}ε²s^{-1}. The entry point is G2Score.notMem_eventG2_iff, which is an exact characterization, so nothing is lost here beyond the j > m rows.