Coarse-graining support: Support.Book.Ch04.Theorems.DescendantAverages

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Public descendant-average concentration

This file composes the public color-class concentration estimates with the finite-color aggregation theorem. It is the coefficient-law-facing form of the partition-average fluctuation input: the statements use RestrictionUnitRangeDependentLaw and IsRestrictionLocalRandomVariable, while the old restriction-sigma machinery remains outside the public theorem surface.

theorem HCPolySupport.Book.Ch04.gammaSigmaDescendantsAtScaleConst_pos {d : ℕ} {k : ℤ} {σ : ℝ} (hσ : 0 < σ) : 0 < gammaSigmaDescendantsAtScaleConst d k σ

The explicit descendant-average Gamma_sigma color-count constant is positive.

theorem HCPolySupport.Book.Ch04.psiSigmaDescendantsAtScaleConst_pos {d : ℕ} {k : ℤ} {σ : ℝ} : 0 < psiSigmaDescendantsAtScaleConst d k σ

The explicit descendant-average Psi_sigma color-count constant is positive.

theorem HCPolySupport.Book.Ch04.isBigO_gammaSigma_restrictionDescendantAverage_of_restrictionUnitRangeDependentLaw {d : ℕ} {Q : TriadicCube d} {k : ℤ} {P : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] {σ K : ℝ} (hk : k ≤ Q.scale) (hP : RestrictionUnitRangeDependentLaw P) (hσ₀ : 0 < σ) (hσ₂ : σ ≤ 2) (hK : 0 < K) (X : TriadicCube d → RegCoeffField d → ℝ) (hX_local : ∀ R ∈ descendantsAtScale Q k, IsRestrictionLocalRandomVariable (cubeSet R) ⋯ (X R)) (hX_meas : ∀ R ∈ descendantsAtScale Q k, Measurable (X R)) (hX : ∀ R ∈ descendantsAtScale Q k, IsBigO P (gammaSigma σ) (X R) K) (h_mean : ∀ R ∈ descendantsAtScale Q k, ∫ (a : RegCoeffField d), X R a ∂P = 0) : IsBigO P (gammaSigma σ) (fun (a : RegCoeffField d) => (↑(descendantsAtScale Q k).card)⁻¹ * ∑ R ∈ descendantsAtScale Q k, X R a) (gammaSigmaDescendantsAtScaleConst d k σ * (√↑(descendantsAtScale Q k).card / ↑(descendantsAtScale Q k).card) * K)

Averaging over all descendants at scale k preserves Gamma_sigma concentration for restriction-unit-range-dependent laws.

theorem HCPolySupport.Book.Ch04.isBigO_psiSigma_restrictionDescendantAverage_of_restrictionUnitRangeDependentLaw {d : ℕ} {Q : TriadicCube d} {k : ℤ} {P : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] {σ K : ℝ} (hk : k ≤ Q.scale) (hP : RestrictionUnitRangeDependentLaw P) (hσ : 1 ≤ σ) (hK : 0 < K) (X : TriadicCube d → RegCoeffField d → ℝ) (hX_local : ∀ R ∈ descendantsAtScale Q k, IsRestrictionLocalRandomVariable (cubeSet R) ⋯ (X R)) (hX_meas : ∀ R ∈ descendantsAtScale Q k, Measurable (X R)) (hX_int : ∀ R ∈ descendantsAtScale Q k, MeasureTheory.Integrable (X R) P) (hX : ∀ R ∈ descendantsAtScale Q k, IsBigO P (psiSigma σ) (X R) K) (h_mean : ∀ R ∈ descendantsAtScale Q k, ∫ (a : RegCoeffField d), X R a ∂P = 0) : IsBigO P (psiSigma σ) (fun (a : RegCoeffField d) => (↑(descendantsAtScale Q k).card)⁻¹ * ∑ R ∈ descendantsAtScale Q k, X R a) (psiSigmaDescendantsAtScaleConst d k σ * (√↑(descendantsAtScale Q k).card / ↑(descendantsAtScale Q k).card) * K)

Averaging over all descendants at scale k preserves Psi_sigma concentration for restriction-unit-range-dependent laws.