CesaroEngine

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

The independent-family Cesàro concentration engine

ABK26, proof of l.minimal.scale.sep.

Each of the paper's three Steps ends, after a deterministic rearrangement, with a Cesàro average over the window [n, m] of the shape (m − n + 1)⁻¹ ( a · Σ_{k = n}^{m} X_k(ω) + T(ω) ),

where {X_k} is an independent family with X_k ≤ O_{Γ₂}(K) and E[X_k] ≤ μ₀, and T is a boundary/tail term with T ≤ O_{Γ₂}(b). The Step's conclusion is ≤ a·μ₀ + O_{Γ₂}( C (a K + b) (m − n + 1)^{-1/2} ).

This module proves that implication for genuinely independent families. Its r-dependent counterpart — the form Step 1 actually needs, where independence is weakened to finite-range dependence — is Algsuperdiff/Probability/ColoredCesaro.lean; the two are deliberately parallel, and this one is the cheaper route whenever full independence is available.

The route is the paper's own:

1. integral_le_of_isBigO_gammaSigma — e.moments.OGamma2: a Γ_σ tail gives integrability and the first-moment bound ∫ X ≤ C_mom(σ) K (the modulus version and the integrability are in CesaroWindow.lean).
2. centered_isBigO_gammaSigma_moment (CesaroWindow.lean) — centering X ↦ X − E X costs only a constant factor in the Γ_σ scale.
3. isBigO_cesaroAvg_of_iIndepFun_centered — CoarseGraining's averaged p.concentration transported to the cesaroAvg/Finset.Icc n m bookkeeping, with the √N / N = N^{-1/2} rewrite done once and for all.
4. cesaroAvg_isBigO_of_iIndepFun — the headline engine.
5. cesaroAvg_isBigO_of_iIndepFun_with_tail — the engine with the boundary term, absorbed by (m − n + 1)⁻¹ ≤ (m − n + 1)^{-1/2}.

Everything is generic over the sample space: no carrier, no coefficient field and no scale geometry enters.

Main results

• Algsuperdiff.Probability.cesaroEngineConst
• Algsuperdiff.Probability.isBigO_cesaroAvg_of_iIndepFun_centered
• Algsuperdiff.Probability.cesaroAvg_isBigO_of_iIndepFun
• Algsuperdiff.Probability.cesaroAvg_isBigO_of_iIndepFun_with_tail

References

• ABK26, Proposition p.concentration.
• ABK26, e.moments.OGamma2.

Explicit constants

noncomputable def Algsuperdiff.Probability.cesaroEngineConst : ℝ

The Cesàro engine constant: CoarseGraining's centered independent-sum constant for σ = 2 times the centering cost.

Equations

• Algsuperdiff.Probability.cesaroEngineConst = HCPolySupport.Book.Ch04.gammaSigmaIndependentSumConst 2 * Algsuperdiff.Probability.cesaroCenterConst 2

noncomputable def Algsuperdiff.Probability.cesaroTailEngineConst : ℝ

The Cesàro engine constant in the presence of an additive boundary/tail term.

Equations

• Algsuperdiff.Probability.cesaroTailEngineConst = (1 + Real.log 2) ^ 2⁻¹ * (Algsuperdiff.Probability.cesaroEngineConst + 1)

theorem Algsuperdiff.Probability.cesaroEngineConst_pos : 0 < cesaroEngineConst

theorem Algsuperdiff.Probability.cesaroTailEngineConst_pos : 0 < cesaroTailEngineConst

rpow bookkeeping

theorem Algsuperdiff.Probability.rpow_neg_half_le_rpow_neg_half {x y : ℝ} (hx : 0 < x) (hxy : x ≤ y) : y ^ (-1 / 2) ≤ x ^ (-1 / 2)

(x + 1)^{-1/2} ≤ x^{-1/2} for x > 0 — the little monotonicity fact that converts the engine's natural (m − n + 1)^{-1/2} envelope into the paper's (m − n)^{-1/2} envelope.

Moments from Γ_σ tails (e.moments.OGamma2)

theorem Algsuperdiff.Probability.integral_le_of_isBigO_gammaSigma {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : Ω → ℝ} {σ K : ℝ} (hσ : 0 < σ) (hK : 0 < K) (hXm : AEMeasurable X P) (hX : HCPolySupport.IndependentSums.IsBigO P (HCPolySupport.IndependentSums.gammaSigma σ) X K) : ∫ (ω : Ω), X ω ∂P ≤ HCPolySupport.IndependentSums.gammaMomentConst σ * K

E X ≤ C_mom(σ) K under a Γ_σ tail bound.

The averaged concentration bound for a centered family

theorem Algsuperdiff.Probability.isBigO_cesaroAvg_of_iIndepFun_centered {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (Y : ℤ → Ω → ℝ) {Kc : ℝ} (hKc : 0 < Kc) (hindep : ProbabilityTheory.iIndepFun Y P) (hmeas : ∀ (j : ℤ), Measurable (Y j)) (hY : ∀ (j : ℤ), HCPolySupport.IndependentSums.IsBigO P (HCPolySupport.IndependentSums.gammaSigma 2) (Y j) Kc) (hmean : ∀ (j : ℤ), ∫ (ω : Ω), Y j ω ∂P = 0) {n m : ℤ} (hnm : n ≤ m) : HCPolySupport.IndependentSums.IsBigO P (HCPolySupport.IndependentSums.gammaSigma 2) (fun (ω : Ω) => cesaroAvg (fun (j : ℤ) => Y j ω) n m) (HCPolySupport.Book.Ch04.gammaSigmaIndependentSumConst 2 * Kc * ↑(m - n + 1) ^ (-1 / 2))

Averaged p.concentration in cesaroAvg form. For a centered, independent, Γ₂-controlled family {Y_j}, the Cesàro average over [n, m] obeys O_{Γ₂}( C · K · (m − n + 1)^{-1/2} ).

The engine

theorem Algsuperdiff.Probability.cesaroAvg_isBigO_of_iIndepFun {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (X : ℤ → Ω → ℝ) {K mu0 : ℝ} (hK : 0 < K) (hindep : ProbabilityTheory.iIndepFun X P) (hmeas : ∀ (j : ℤ), Measurable (X j)) (hX : ∀ (j : ℤ), HCPolySupport.IndependentSums.IsBigO P (HCPolySupport.IndependentSums.gammaSigma 2) (X j) K) (hmean : ∀ (j : ℤ), ∫ (ω : Ω), X j ω ∂P ≤ mu0) (n m : ℤ) (hnm : n ≤ m) : ∃ (Xfluc : Ω → ℝ), (∀ (ω : Ω), cesaroAvg (fun (j : ℤ) => X j ω) n m ≤ mu0 + Xfluc ω) ∧ HCPolySupport.IndependentSums.IsBigO P (HCPolySupport.IndependentSums.gammaSigma 2) Xfluc (cesaroEngineConst * K * ↑(m - n + 1) ^ (-1 / 2))

The Cesàro concentration engine. For an independent family {X_j} with X_j ≤ O_{Γ₂}(K) and E X_j ≤ μ₀, the Cesàro average over a window [n, m] splits as μ₀ plus a fluctuation of scale cesaroEngineConst · K · (m − n + 1)^{-1/2}.

This is the shared probabilistic core of Steps 1--3 in the proof of ABK26 l.minimal.scale.sep, in the fully independent regime.

theorem Algsuperdiff.Probability.cesaroAvg_isBigO_of_iIndepFun_with_tail {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (X : ℤ → Ω → ℝ) (T Dbar : Ω → ℝ) {K mu0 a b : ℝ} (hK : 0 < K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hindep : ProbabilityTheory.iIndepFun X P) (hmeas : ∀ (j : ℤ), Measurable (X j)) (hX : ∀ (j : ℤ), HCPolySupport.IndependentSums.IsBigO P (HCPolySupport.IndependentSums.gammaSigma 2) (X j) K) (hmean : ∀ (j : ℤ), ∫ (ω : Ω), X j ω ∂P ≤ mu0) (hT : HCPolySupport.IndependentSums.IsBigO P (HCPolySupport.IndependentSums.gammaSigma 2) T b) (n m : ℤ) (hnm : n ≤ m) (hdom : ∀ (ω : Ω), Dbar ω ≤ a * cesaroAvg (fun (j : ℤ) => X j ω) n m + 1 / ↑(m - n + 1) * T ω) : ∃ (Xdet : Ω → ℝ) (Xfluc : Ω → ℝ), (∀ (ω : Ω), Dbar ω ≤ Xdet ω + Xfluc ω) ∧ (∀ (ω : Ω), Xdet ω ≤ a * mu0) ∧ HCPolySupport.IndependentSums.IsBigO P (HCPolySupport.IndependentSums.gammaSigma 2) Xfluc (cesaroTailEngineConst * (a * K + b) * ↑(m - n + 1) ^ (-1 / 2))

The Cesàro engine with an additive boundary/tail term. This is the exact shape produced by each of the paper's Steps 1--3 after the deterministic rearrangement: D ≤ a · avsum X + (m − n + 1)⁻¹ · T with T ≤ O_{Γ₂}(b) gives D ≤ a μ₀ + O_{Γ₂}( C (aK + b)(m − n + 1)^{-1/2} ).