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

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

Restriction-local partition-average fluctuation theorems

This file connects the restriction-local descendant-average concentration estimates to the centered origin-cube formulation used in the notes. The proof uses the existing stationarity lemmas internally, but the theorem statements are phrased only in terms of the explicit restriction law and restriction-local-random-variable notions.

theorem HCPolySupport.Book.Ch04.integral_restrictionDescendantAverage_eq_integral_originCube_of_stationary {d : ℕ} {n m : ℤ} {P : RestrictionCoeffLaw d} (hn : 0 ≤ n) (hnm : n ≤ m) (hPstat : RestrictionStationaryLaw P) (X : Set (Vec d) → RegCoeffField d → ℝ) (hX0_meas : Measurable (X (cubeSet (originCube d n)))) (hX_desc_int : ∀ R ∈ descendantsAtScale (originCube d m) n, MeasureTheory.Integrable (X (cubeSet R)) P) (hX_cov : IsRestrictionTranslationCovariant X) : ∫ (a : RegCoeffField d), restrictionDescendantAverage n m X a ∂P = ∫ (a : RegCoeffField d), X (cubeSet (originCube d n)) a ∂P

Stationarity identifies the expectation of the uncentered descendant partition average with the expectation on the origin cube at the descendant scale.

theorem HCPolySupport.Book.Ch04.integral_restrictionCenteredDescendantAverage_eq_zero_of_stationary {d : ℕ} {n m : ℤ} {P : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] (hn : 0 ≤ n) (hnm : n ≤ m) (hPstat : RestrictionStationaryLaw P) (X : Set (Vec d) → RegCoeffField d → ℝ) (hX0_meas : Measurable (X (cubeSet (originCube d n)))) (hX_desc_int : ∀ R ∈ descendantsAtScale (originCube d m) n, MeasureTheory.Integrable (X (cubeSet R)) P) (hX_cov : IsRestrictionTranslationCovariant X) : ∫ (a : RegCoeffField d), restrictionCenteredDescendantAverage P n m X a ∂P = 0

The centered descendant partition average has mean zero under stationarity.

theorem HCPolySupport.Book.Ch04.isBigO_gammaSigma_restrictionCenteredDescendantAverage_of_restrictionUnitRangeDependentLaw {d : ℕ} {n m : ℤ} {P : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] {σ K : ℝ} (hn : 0 ≤ n) (hnm : n ≤ m) (hPstat : RestrictionStationaryLaw P) (hPdep : RestrictionUnitRangeDependentLaw P) (X : Set (Vec d) → RegCoeffField d → ℝ) (hX_local : ∀ R ∈ descendantsAtScale (originCube d m) n, IsRestrictionLocalRandomVariable (cubeSet R) ⋯ (X (cubeSet R))) (hX_cov : IsRestrictionTranslationCovariant X) (hX0_meas : Measurable (X (cubeSet (originCube d n)))) (hX_desc_meas : ∀ R ∈ descendantsAtScale (originCube d m) n, Measurable (X (cubeSet R))) (hσ₀ : 0 < σ) (hσ₂ : σ ≤ 2) (hK : 0 < K) (hX0 : IsBigO P (gammaSigma σ) (restrictionCenteredOriginObservable P n X) K) : IsBigO P (gammaSigma σ) (restrictionCenteredDescendantAverage P n m X) (gammaSigmaDescendantsAtScaleConst d n σ * partitionCardinalityScale n m * K)

Centered Gamma_sigma fluctuation bound for restriction-centered descendant averages of a translation-covariant cube observable.

theorem HCPolySupport.Book.Ch04.isBigO_psiSigma_restrictionCenteredDescendantAverage_of_restrictionUnitRangeDependentLaw {d : ℕ} {n m : ℤ} {P : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] {σ K : ℝ} (hn : 0 ≤ n) (hnm : n ≤ m) (hPstat : RestrictionStationaryLaw P) (hPdep : RestrictionUnitRangeDependentLaw P) (X : Set (Vec d) → RegCoeffField d → ℝ) (hX_local : ∀ R ∈ descendantsAtScale (originCube d m) n, IsRestrictionLocalRandomVariable (cubeSet R) ⋯ (X (cubeSet R))) (hX_cov : IsRestrictionTranslationCovariant X) (hX0_meas : Measurable (X (cubeSet (originCube d n)))) (hX0_int : MeasureTheory.Integrable (X (cubeSet (originCube d n))) P) (hX_desc_meas : ∀ R ∈ descendantsAtScale (originCube d m) n, Measurable (X (cubeSet R))) (hX_desc_int : ∀ R ∈ descendantsAtScale (originCube d m) n, MeasureTheory.Integrable (X (cubeSet R)) P) (hσ : 1 ≤ σ) (hK : 0 < K) (hX0 : IsBigO P (psiSigma σ) (restrictionCenteredOriginObservable P n X) K) : IsBigO P (psiSigma σ) (restrictionCenteredDescendantAverage P n m X) (psiSigmaDescendantsAtScaleConst d n σ * partitionCardinalityScale n m * K)

Centered Psi_sigma fluctuation bound for restriction-centered descendant averages of a translation-covariant cube observable.