ColoredCesaro

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

The r-dependent Cesàro Γ_σ concentration engine

ABK26, proof of l.minimal.scale.sep, Step 1. Step 1 does not end with a fully independent family: it ends with

"Since the sequence {X_j} is r(d)-dependent, we may apply Proposition p.concentration to obtain (m−n)^{-1/2} ∑_{j=n}^m (X_j − E[X_j]) ≤ O_{Γ₂}(C c⋆^{-1} s^{-5/2} γ^{1/2})."

p.concentration as printed is stated for independent sequences, so the object Step 1 actually consumes is not a theorem of the manuscript. This module supplies it: the exact analogue of the independent Cesàro engine with full independence weakened to the r-dependence of Algsuperdiff/Probability/RDependent.lean. The free r reaches the conclusion only through the constant rDepEngineConst r (a √(r+1) colour count), so no dimensional restriction rides on the engine.

The route

Split the window [n, m] ⊆ ℤ into the r+1 residue classes mod r+1. Two distinct indices in one class differ by a nonzero multiple of r+1, hence are ≥ r-separated, hence the class is mutually independent (le_abs_sub_of_intCast_zmod_eq); the r+1 per-class sums are recombined by the Γ_σ triangle inequality. Both halves are packaged in the palette-generic isBigO_gammaSigma_average_colored, whose combinatorial input at this colouring is sum_sqrt_class_card_le together with card_zmod_succ.

Main results

• rDepEngineConst — the explicit colour-count constant.
• isBigO_cesaroAvg_of_rDependent_centered — colouring plus concentration for a centred family.
• cesaroAvg_isBigO_of_rDependent — the corresponding engine before centring.

References

• ABK26, Proposition p.concentration.
• ABK26, l.minimal.scale.sep, Step 1.

Explicit constants

noncomputable def Algsuperdiff.Probability.rDepEngineConst (r : ℕ) : ℝ

The r-dependent Cesàro engine constant: CoarseGraining's centered independent-sum constant for σ = 2, times the centering cost, inflated by the Γ₂ triangle constant (recombining the r+1 colour classes) and by √(r+1) (the colour count).

Equations

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

theorem Algsuperdiff.Probability.rDepEngineConst_pos (r : ℕ) : 0 < rDepEngineConst r

The coloured concentration bound for a centred r-dependent family

theorem Algsuperdiff.Probability.isBigO_cesaroAvg_of_rDependent_centered {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (Y : ℤ → Ω → ℝ) {Kc : ℝ} {r : ℕ} (hKc : 0 < Kc) (hdep : RDependent P Y r) (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.IndependentSums.gammaTriangleConst 2 * HCPolySupport.Book.Ch04.gammaSigmaIndependentSumConst 2 * √(↑r + 1) * Kc * ↑(m - n + 1) ^ (-1 / 2))

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

The engine

theorem Algsuperdiff.Probability.cesaroAvg_isBigO_of_rDependent {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (X : ℤ → Ω → ℝ) {K mu0 : ℝ} {r : ℕ} (hK : 0 < K) (hdep : RDependent P X r) (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 (rDepEngineConst r * K * ↑(m - n + 1) ^ (-1 / 2))

The r-dependent Cesàro concentration engine. For an r-dependent 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 rDepEngineConst r · K · (m − n + 1)^{-1/2}.

This is the form Step 1 of ABK26 l.minimal.scale.sep needs: the same conclusion as the fully independent engine, with independence weakened to r-dependence.