Coarse-graining support: Support.Book.Ch04.Theorems.PartitionAverages #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Public partition-average concentration tools #
This file contains proved, coefficient-free probability tools for the
finite-coloring step in Proposition
p.local.partition.average.fluctuations.stationary.random.fields. The
locality and stationarity bridges remain separate; the aggregation of
independent color-class estimates is already a theorem.
theorem
HCPolySupport.Book.Ch04.isBigO_finsetAverage_colorClassSums_gammaSigma
{Ω : Type u_1}
{κ : Type u_2}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
(colors : Finset κ)
{Y : κ → Ω → ℝ}
{classCount : κ → ℝ}
{colorCount totalCount C K σ : ℝ}
(hσ : 0 < σ)
(hcolors : colors.Nonempty)
(hClassCount : ∀ c ∈ colors, 0 < classCount c)
(hTotal : 0 < totalCount)
(hC : 0 < C)
(hK : 0 < K)
(hY : ∀ c ∈ colors, IsBigO μ (gammaSigma σ) (Y c) (C * √(classCount c) * K))
(hYmeas : ∀ c ∈ colors, Measurable (Y c))
(hSqrt : ∑ c ∈ colors, √(classCount c) ≤ √colorCount * √totalCount)
:
Aggregating Gamma_sigma color-class sum estimates and then dividing by
the total cardinality gives the partition-average square-root scale.
theorem
HCPolySupport.Book.Ch04.isBigO_finsetAverage_colorClassSums_psiSigma
{Ω : Type u_1}
{κ : Type u_2}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
(colors : Finset κ)
{Y : κ → Ω → ℝ}
{classCount : κ → ℝ}
{colorCount totalCount C K σ : ℝ}
(hσ : 1 ≤ σ)
(hcolors : colors.Nonempty)
(hClassCount : ∀ c ∈ colors, 0 < classCount c)
(hTotal : 0 < totalCount)
(hC : 0 < C)
(hK : 0 < K)
(hY : ∀ c ∈ colors, IsBigO μ (psiSigma σ) (Y c) (C * √(classCount c) * K))
(hYmeas : ∀ c ∈ colors, Measurable (Y c))
(hSqrt : ∑ c ∈ colors, √(classCount c) ≤ √colorCount * √totalCount)
:
Aggregating Psi_sigma color-class sum estimates and then dividing by the
total cardinality gives the partition-average square-root scale.