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

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

Restriction-local Gamma partition fluctuations

This is the a.e.-restriction-local counterpart of the Gamma partition fluctuation estimate. It is designed for totalized Ch4 observables which are only a.e.-equal to local representatives on each descendant cube.

theorem HCPolySupport.Book.Ch04.isBigO_gammaSigma_centeredDescendantMean_of_unitRangeLaw {d : ℕ} {Q : TriadicCube d} {n : ℤ} {P : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] {σ K : ℝ} (hP : RestrictionLawCarrier P) (hn : 0 ≤ n) (hnQ : n ≤ Q.scale) (hPstat : RestrictionStationaryLaw P) (hPdep : RestrictionUnitRangeDependentLaw P) (X : Set (Vec d) → RegCoeffField d → ℝ) (hX_localRep : ∀ R ∈ descendantsAtScale Q n, ∃ (Y : RegCoeffField d → ℝ), IsRestrictionLocalRandomVariable (cubeSet R) ⋯ Y ∧ X (cubeSet R) =ᵐ[P] Y) (hX_cov : IsRestrictionTranslationCovariant X) (hX0_aemeas : AEMeasurable (X (cubeSet (originCube d n))) P) (hX_desc_aemeas : ∀ R ∈ descendantsAtScale Q n, AEMeasurable (X (cubeSet R)) P) (hσ₀ : 0 < σ) (hσ₂ : σ ≤ 2) (hK : 0 < K) (hX0 : IsBigO P (gammaSigma σ) (restrictionCenteredOriginObservable P n X) K) : IsBigO P (gammaSigma σ) (restrictionCenteredDescendantAverageOnCube P Q n X) (gammaSigmaDescendantsAtScaleConst d n σ * (√↑(descendantsAtScale Q n).card / ↑(descendantsAtScale Q n).card) * K)