Documentation

LeanPool.Superdiffusion.Algsuperdiff.Probability.ColoredAverage

ColoredAverage #

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

Abstract coloured (finite-range) Γ_σ concentration #

ABK26, the grid corollary stated immediately after Proposition p.concentration: for centered O_{Γ_σ}(1) variables indexed by a 3ⁿ-grid inside □_m, independent whenever the corresponding subcubes do not touch (finite range of dependence), the averaged sum obeys ∑_{z} X_z ≤ O_{Γ_σ}(C(σ)·3^{d(m−n)/2}), i.e. the average gains 3^{−d(m−n)/2}.

What this module adds #

CoarseGraining proves the concrete triadic instance of the corollary (Ch04.isBigO_gammaSigma_descendantAverage_of_unitRangeDependentLaw), tied to the specific triadic geometry and the unit range r = 1, and it exposes the recombination step Ch04.isBigO_finsetAverage_colorClassSums_gammaSigma. What is missing everywhere — in CoarseGraining and in this repository, whose only colourings are hard-wired to spatial sites Fin d → ℤ — is the abstract, index-set and palette generic colouring wrapper: for an arbitrary finite index set s and an arbitrary colouring c : ι → κ whose colour classes are internally mutually independent, centered O_{Γ_σ}(K) summands give the averaged √card / card gain.

That wrapper is isBigO_gammaSigma_average_colored below. It is the reusable core of the grid corollary at any range r: the caller supplies one iIndepFun per used colour, which is exactly what a finite-range-r colouring with C(r,d) colours delivers. Instantiating κ, c at the triadic residue colouring recovers CoarseGraining's concrete theorem; instantiating them at ZMod (r+1) on a window of ℤ gives the r-dependent Cesàro engine.

The combinatorial hSqrt input is supplied here in the generality any finite palette provides (sum_sqrt_class_card_le).

Main results #

References #

source
theorem Algsuperdiff.Probability.gammaSigmaIndependentSumConst_pos {σ : ℝ} (hσ : 0 < σ) :
0 < HCPolySupport.Book.Ch04.gammaSigmaIndependentSumConst σ

Positivity of CoarseGraining's public constant for the centered independent-sum Γ_σ concentration inequality. CoarseGraining keeps this fact private, so it is reproved here from CoarseGraining's public constants.

source
theorem Algsuperdiff.Probability.sum_sqrt_class_card_le {ι : Type u_1} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (s : Finset ι) (c : ι → κ) :
∑ b ∈ Finset.image c s, √↑{j ∈ s | c j = b}.card ≤ √↑(Fintype.card κ) * √↑s.card

Cauchy--Schwarz over the colour classes. For any colouring c : ι → κ of a finite set s by a finite palette κ, the sum of the square roots of the colour-class cardinalities is at most √(#κ) · √(#s).

This is the hSqrt hypothesis of isBigO_gammaSigma_average_colored, in the form in which a residue colouring by a Fintype palette supplies it.

source
theorem Algsuperdiff.Probability.isBigO_gammaSigma_average_colored {Ω : Type u_1} {ι : Type u_2} {κ : Type u_3} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] [DecidableEq κ] (s : Finset ι) (c : ι → κ) {X : ι → Ω → ℝ} {σ K colorCount : ℝ} (hσ₀ : 0 < σ) (hσ₂ : σ ≤ 2) (hK : 0 < K) (h_indep : ∀ b ∈ Finset.image c s, ProbabilityTheory.iIndepFun (fun (i : ↥({j ∈ s | c j = b})) => X ↑i) P) (h_meas : ∀ i ∈ s, Measurable (X i)) (hX : ∀ i ∈ s, HCPolySupport.IndependentSums.IsBigO P (HCPolySupport.IndependentSums.gammaSigma σ) (X i) K) (h_mean : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂P = 0) (hSqrt : ∑ b ∈ Finset.image c s, √↑{j ∈ s | c j = b}.card ≤ √colorCount * √↑s.card) :
HCPolySupport.IndependentSums.IsBigO P (HCPolySupport.IndependentSums.gammaSigma σ) (fun (ω : Ω) => (↑s.card)⁻¹ * ∑ i ∈ s, X i ω) (HCPolySupport.IndependentSums.gammaTriangleConst σ * HCPolySupport.Book.Ch04.gammaSigmaIndependentSumConst σ * (√colorCount * (√↑s.card / ↑s.card)) * K)

Coloured (finite-range) concentration. Let s be a finite index set and c : ι → κ a colouring whose colour classes {i ∈ s | c i = b} are internally mutually independent (hypothesis h_indep, one iIndepFun per used colour — this is precisely the finite-range-of-dependence colouring with C(r,d) colours). If each summand is centered with X i ≤ O_{Γ_σ}(K), and the colour-class square roots obey the combinatorial bound hSqrt (with colorCount ≥ #colours), then the average obeys

(1/#s)∑_{i∈s} X_i ≤ O_{Γ_σ}(gammaTriangleConst σ · gammaSigmaIndependentSumConst σ · (√colorCount · √#s / #s) · K).

Instantiating s at a triadic descendant set, c at the residue colouring and colorCount at the residue-period power recovers the paper's 3^{−d(m−n)/2} grid corollary.