CesaroWindow

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

The Cesàro window average, its arithmetic, and Γ_σ centering

ABK26, §4.2 writes avsum_{k=n}^m f k for the window average (m − n + 1)⁻¹ ∑_{k ∈ [n,m]} f k. This module supplies

• the average itself (cesaroAvg) and the elementary window arithmetic (natCast_card_Icc_int, one_le_window, window_pos) used to normalise the √N / N = N^{-1/2} bookkeeping;
• the rpow identities sqrt_div_self_eq_rpow_neg_half and inv_le_rpow_neg_half that convert those prefactors into the paper's (m − n + 1)^{-1/2} envelope;
• the moment and centering layer for the stretched-exponential class: a Γ_σ tail gives integrability and a first-moment bound (e.moments.OGamma2), and recentring a Γ_σ variable costs only the explicit constant cesaroCenterConst σ = (1 + log 2)^{1/σ}(1 + gammaMomentConst σ); and
• the deterministic split cesaroAvg_le_add_cesaroAvg_sub, which peels a uniform mean bound off a window average.

Everything here is generic over the sample space: no carrier, no coefficient field, no scale index enters. The centering step deliberately routes through the measurability-free two-term triangle inequality of Algsuperdiff/Probability/GammaSigmaFiniteTriangle.lean, because the objects recentred downstream are existential witnesses with no available measurability.

Main results

• Algsuperdiff.Probability.cesaroAvg
• Algsuperdiff.Probability.integrable_of_isBigO_gammaSigma
• Algsuperdiff.Probability.centered_isBigO_gammaSigma_moment
• Algsuperdiff.Probability.cesaroAvg_le_add_cesaroAvg_sub

References

• ABK26, l.minimal.scale.sep for the window average.
• ABK26, e.moments.OGamma2 for the moment bound.
• ABK26, l.Gamma.sigma.triangle for the centering cost.

The window average

noncomputable def Algsuperdiff.Probability.cesaroAvg (f : ℤ → ℝ) (n m : ℤ) : ℝ

The Cesàro (window) average avsum_{k=n}^m f k = (m − n + 1)⁻¹ ∑_{k=n}^m f k.

Equations

• Algsuperdiff.Probability.cesaroAvg f n m = 1 / ↑(m - n + 1) * ∑ k ∈ Finset.Icc n m, f k

Window arithmetic

theorem Algsuperdiff.Probability.natCast_card_Icc_int {n m : ℤ} (hnm : n ≤ m) : ↑(Finset.Icc n m).card = ↑(m - n + 1)

The window cardinality, as a real number.

theorem Algsuperdiff.Probability.one_le_window {n m : ℤ} (hnm : n ≤ m) : 1 ≤ ↑(m - n + 1)

theorem Algsuperdiff.Probability.window_pos {n m : ℤ} (hnm : n ≤ m) : 0 < ↑(m - n + 1)

rpow bookkeeping

theorem Algsuperdiff.Probability.sqrt_div_self_eq_rpow_neg_half {c : ℝ} (hc : 0 < c) : √c / c = c ^ (-1 / 2)

√c / c = c^{-1/2} for c > 0.

theorem Algsuperdiff.Probability.inv_le_rpow_neg_half {c : ℝ} (hc : 1 ≤ c) : 1 / c ≤ c ^ (-1 / 2)

c⁻¹ ≤ c^{-1/2} for c ≥ 1.

The centering constant

theorem Algsuperdiff.Probability.one_add_log_two_pos : 0 < 1 + Real.log 2

noncomputable def Algsuperdiff.Probability.cesaroCenterConst (σ : ℝ) : ℝ

The centering cost for a Γ_σ variable: X − ≤ O_{Γ_σ}(cesaroCenterConst σ · K) whenever X ≤ O_{Γ_σ}(K). Built from the measurability-free two-term triangle constant (1 + log 2)^{1/σ} and the first-moment constant gammaMomentConst σ (e.moments.OGamma2).

Equations

• Algsuperdiff.Probability.cesaroCenterConst σ = (1 + Real.log 2) ^ σ⁻¹ * (1 + HCPolySupport.IndependentSums.gammaMomentConst σ)

theorem Algsuperdiff.Probability.cesaroCenterConst_pos {σ : ℝ} (hσ : 0 < σ) : 0 < cesaroCenterConst σ

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

theorem Algsuperdiff.Probability.integral_abs_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.moments.OGamma2 (p = 1): a Γ_σ tail gives ∫ |X| ≤ C_mom(σ) K.

theorem Algsuperdiff.Probability.integrable_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) : MeasureTheory.Integrable X P

A Γ_σ tail bound makes X integrable.

theorem Algsuperdiff.Probability.abs_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

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

Centering

theorem Algsuperdiff.Probability.centered_isBigO_gammaSigma {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : Ω → ℝ} {σ K c : ℝ} (hσ : 0 < σ) (hK : 0 ≤ K) (hc0 : 0 ≤ c) (hc : |∫ (ω : Ω), X ω ∂P| ≤ c) (hX : HCPolySupport.IndependentSums.IsBigO P (HCPolySupport.IndependentSums.gammaSigma σ) X K) : HCPolySupport.IndependentSums.IsBigO P (HCPolySupport.IndependentSums.gammaSigma σ) (fun (ω : Ω) => X ω - ∫ (ω' : Ω), X ω' ∂P) ((1 + Real.log 2) ^ σ⁻¹ * (K + c))

Centering a Γ_σ variable. If X ≤ O_{Γ_σ}(K) and || ≤ c then X − ≤ O_{Γ_σ}((1 + log 2)^{1/σ}(K + c)). Measurability-free: it uses the two-term triangle inequality of GammaSigmaFiniteTriangle.lean.

theorem Algsuperdiff.Probability.centered_isBigO_gammaSigma_moment {Ω : 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) : HCPolySupport.IndependentSums.IsBigO P (HCPolySupport.IndependentSums.gammaSigma σ) (fun (ω : Ω) => X ω - ∫ (ω' : Ω), X ω' ∂P) (cesaroCenterConst σ * K)

Centering with the moment bound already inserted: the scale is cesaroCenterConst σ · K.

The deterministic Cesàro rearrangement

theorem Algsuperdiff.Probability.cesaroAvg_le_add_cesaroAvg_sub {f g : ℤ → ℝ} {mu0 : ℝ} {n m : ℤ} (hnm : n ≤ m) (hg : ∀ (j : ℤ), g j ≤ mu0) : cesaroAvg f n m ≤ mu0 + cesaroAvg (fun (j : ℤ) => f j - g j) n m

Splitting a Cesàro average into a mean part and a centered part: if g j ≤ μ₀ for all j then avsum f ≤ μ₀ + avsum (f − g).