RowSumFinite

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

a.s. finiteness of the 𝒴 row sum, and the Appendix-D reduction of 𝒢₀

ABK26, §4.1, l.good.scales.ratio.lambda, score domination, and the threshold identification.

ScoreDomination.one_lt_YcalRowE_of_notMem_eventG0 is the deterministic half of the reduction hreduce the 𝒢₀ lane consumes: off 𝒢₀(m) the ℝ≥0∞-formed row sum Σ_{n ≤ m} 3^{−s'(m−n)} 𝒴_n exceeds 1. The Appendix-D row sum Y_m, by contrast, is the real, two-sided series Σ_{j ∈ ℤ} 3^{−s'|m−j|} D^{-1}𝒴_j, which is a tsum in ℝ and therefore only carries information where the family is summable. This module supplies the missing half: the a.s. finiteness that converts the one into the other.

Route

Everything is a first-moment computation; no Borel--Cantelli is used.

1. lintegral_ofReal_le_of_isBigOWith — the p = 1 case of the ambient library's tail-to-moment engine: a Γ_σ upper tail at scale K gives E[Y] ≤ gammaMomentConst σ · K.
2. lintegral_YcalE_le — Tonelli (lintegral_tsum) over the k-series defining 𝒴_n, with the per-annulus tails of Ycal.isBigOWith_annMax: E[𝒴_n] ≤ gammaMomentConst σ · Σ_j 3^{−s'j} a_j < ∞.
3. lintegral_YcalRowTwoE_le — Tonelli again over the ℤ-row, with the 𝒴-tail of Ycal.isBigOWith_Ycal and the geometric weight sum Σ_{j ∈ ℤ} 3^{−s'|m−j|} ≤ 3/s'.
4. measure_compl_goodRowSet — the two finite expectations make the countable family {𝒴_n = ∞} and {row_m = ∞} null; their union N is the null set of the enlargement.
5. lt_Yk_of_notMem_eventG0 — on Nᶜ the ℝ≥0∞ row sum IS the real row sum, the one-sided row is below the two-sided one, and the deterministic half delivers D^{-1} < Y_m.

The final bookkeeping lemma measure_scaleProp_le_of_null_enlargement pays for the enlargement Ev m := 𝒢₀(m) ∪ N with + ℙ[N] = 0, so the tail proved for the enlarged family is a tail for 𝒢₀ itself.

Scope

Provider material: proved local helpers.

References

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

1. Two carrier-neutral devices

theorem Algsuperdiff.Section4.Provider.Proportion.lintegral_ofReal_le_of_isBigOWith {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {Y : Omega → ℝ} {sigma K : ℝ} (hsigma : 0 < sigma) (hK : 0 < K) (hYnn : ∀ (omega : Omega), 0 ≤ Y omega) (hYm : AEMeasurable Y mu) (hY : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) Y K) : ∫⁻ (omega : Omega), ENNReal.ofReal (Y omega) ∂mu ≤ ENNReal.ofReal (HCPolySupport.IndependentSums.gammaMomentConst sigma * K)

The first moment of a Γ_σ upper tail. The p = 1 instance of the ambient library's tail-to-moment engine, in its ∫⁻ reading: a nonnegative random variable with a stretched-exponential upper tail at scale K has E[Y] ≤ gammaMomentConst σ · K.

theorem Algsuperdiff.Section4.Provider.Proportion.measure_scaleProp_le_of_null_enlargement {Omega : Type u_1} [MeasurableSpace Omega] (P : MeasureTheory.Measure Omega) (Ev : ℤ → Set Omega) (N : Set Omega) (hN : P N = 0) {theta : ℝ} (n : ℕ) : P {omega : Omega | theta < Probability.IndicatorDensity.scaleProp (fun (k : ℤ) => (Ev k)ᶜ) n omega} ≤ P {omega : Omega | theta < Probability.IndicatorDensity.scaleProp (fun (k : ℤ) => (Ev k ∪ N)ᶜ) n omega}

Null-set enlargement of an event family. Enlarging every member of an event family by one fixed null set N costs + ℙ[N] = 0 in the bad-density tail: off N the two families have the same indicator sums, so the θ-excess event of the original family is contained in that of the enlarged family together with N.

2. The ℝ≥0∞ score field: measurability and first moment

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

theorem Algsuperdiff.Section4.Provider.Proportion.lintegral_YcalE_le {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 : ℤ) : ∫⁻ (omega : Section3.Cutoff.CutoffSample d), YcalE M Ccg sprime n omega ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (HCPolySupport.IndependentSums.gammaMomentConst sigma * ∑' (j : ℕ), weightThird sprime j * a j)

E[𝒴_n] < ∞, by Tonelli over the k-series. The per-annulus maxima have Γ_σ tails at the penalised atom scales (isBigOWith_annMax), so each has a finite first moment; the weighted series of those moments is the convergent Σ_j 3^{−s'j} a_j of the 𝒴-tail hypothesis. The bound is uniform in n.

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

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

The Appendix-D row sum of the 𝒴-atoms, formed in ℝ≥0∞. Two-sided, matching ScalesConcentration.Yk, and total.

Equations

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

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_YcalRowTwoE {d : ℕ} (M : Section3.ABKModel d) (Ccg sprime : ℝ) (m : ℤ) : Measurable (YcalRowTwoE M Ccg sprime m)

theorem Algsuperdiff.Section4.Provider.Proportion.lintegral_YcalRowTwoE_le {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) {sigma sprime K : ℝ} (hsigma : 0 < sigma) (hK : 0 < K) (hs0 : 0 < sprime) (hs2 : 2 * sprime ≤ 1) (htail : ∀ (n : ℤ), HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sigma) (Ycal M Ccg sprime n) K) (m : ℤ) : ∫⁻ (omega : Section3.Cutoff.CutoffSample d), YcalRowTwoE M Ccg sprime m omega ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (3 / sprime * (HCPolySupport.IndependentSums.gammaMomentConst sigma * K))

E[Y_m] < ∞, by Tonelli over the ℤ-row. The 𝒴-tail gives each atom a finite first moment, and the geometric weights are summable with Σ_{j ∈ ℤ} 3^{−s'|m−j|} ≤ 3/s'.

4. The null set of the enlargement

def Algsuperdiff.Section4.Provider.Proportion.goodRowSet {d : ℕ} (M : Section3.ABKModel d) (Ccg sprime : ℝ) : Set (Section3.Cutoff.CutoffSample d)

The full-measure set on which the Appendix-D row sum is the honest series. Both the k-series defining each 𝒴_n and the ℤ-row of the 𝒴_n are finite there; off it the real tsum defining Y_m carries no information.

Equations

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

theorem Algsuperdiff.Section4.Provider.Proportion.measure_compl_goodRowSet {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) {sigma sprime A K : ℝ} {a : ℕ → ℝ} (hsigma : 0 < sigma) (hA : 0 ≤ A) (hK : 0 < K) (hs0 : 0 < sprime) (hs2 : 2 * sprime ≤ 1) (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) (htail : ∀ (n : ℤ), HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sigma) (Ycal M Ccg sprime n) K) : ↑(Section3.Cutoff.cutoffSampleLaw M) (goodRowSet M Ccg sprime)ᶜ = 0

The enlargement's null set is null. Both defining families are countable and every member is null by the two first-moment bounds.

5. The reduction

theorem Algsuperdiff.Section4.Provider.Proportion.weightThird_eq_wt {sprime : ℝ} {m n : ℤ} (hn : n ≤ m) : weightThird sprime (m - n).toNat = Probability.ScalesConcentration.wt sprime m n

The natural-index row weight agrees with the integer-distance weight.

theorem Algsuperdiff.Section4.Provider.Proportion.YcalRowE_le_YcalRowTwoE {d : ℕ} (M : Section3.ABKModel d) (Ccg sprime : ℝ) (m : ℤ) {omega : Section3.Cutoff.CutoffSample d} (hfin : ∀ (n : ℤ), YcalE M Ccg sprime n omega ≠ ⊤) : YcalRowE M Ccg sprime m omega ≤ YcalRowTwoE M Ccg sprime m omega

The ℝ≥0∞ one-sided row is below the real two-sided row, on the full-measure set where the score fields are finite.

theorem Algsuperdiff.Section4.Provider.Proportion.lt_Yk_of_notMem_eventG0 {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) {D : ℝ} (hD : 0 < D) (m : ℤ) {omega : Section3.Cutoff.CutoffSample d} (hgood : omega ∈ goodRowSet M Ccg (M.gamma / 4)) (hnot : omega ∉ Support.eventG0 M Ccg m) : D⁻¹ < Probability.ScalesConcentration.Yk (ycalArray M Ccg (M.gamma / 4) D) (M.gamma / 4) m omega

The Appendix-D reduction of 𝒢₀, off the null set.

Off 𝒢₀(m) — and off the null set of goodRowSet — the Appendix-D row sum of the normalized atoms D^{-1}𝒴 exceeds D^{-1}. Chaining the deterministic one_lt_YcalRowE_of_notMem_eventG0 with the ℝ≥0∞ → ℝ conversion this module supplies, this is the missing half of hreduce.