Coarse-graining support: Support.Book.Ch04.Theorems.DescendantAveragesAEMeasurable #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
A.e.-measurable descendant-average concentration #
This file mirrors the Gamma descendant-average estimate from
DescendantAverages, replacing global measurability of the summands by
law-a.e. measurability. The locality and unit-range assumptions are unchanged.
theorem
HCPolySupport.Book.Ch04.isBigO_gammaSigma_finiteSum_descendantsScaleColorClass
{d : ℕ}
{Q : TriadicCube d}
{k : ℤ}
{c : ScaleColor d k}
{P : RestrictionCoeffLaw d}
[MeasureTheory.IsProbabilityMeasure P]
{σ K : ℝ}
(hP : RestrictionUnitRangeDependentLaw P)
(hσ₀ : 0 < σ)
(hσ₂ : σ ≤ 2)
(hK : 0 < K)
(X : TriadicCube d → RegCoeffField d → ℝ)
(hX_local : ∀ R ∈ descendantsAtScaleScaleColorClass Q k c, IsRestrictionLocalRandomVariable (cubeSet R) ⋯ (X R))
(hX_aemeas : ∀ R ∈ descendantsAtScaleScaleColorClass Q k c, AEMeasurable (X R) P)
(hX : ∀ R ∈ descendantsAtScaleScaleColorClass Q k c, IsBigO P (gammaSigma σ) (X R) K)
(h_mean : ∀ R ∈ descendantsAtScaleScaleColorClass Q k c, ∫ (a : RegCoeffField d), X R a ∂P = 0)
:
IsBigO P (gammaSigma σ) (fun (a : RegCoeffField d) => ∑ R ∈ descendantsAtScaleScaleColorClass Q k c, X R a)
(gammaSigmaIndependentSumConst σ * √↑(descendantsAtScaleScaleColorClass Q k c).card * K)
theorem
HCPolySupport.Book.Ch04.isBigO_finsetAverage_colorClassSums_gammaSigma_aemeasurable
{Ω : 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))
(hY_aemeas : ∀ (c : κ), AEMeasurable (Y c) μ)
(hSqrt : ∑ c ∈ colors, √(classCount c) ≤ √colorCount * √totalCount)
:
theorem
HCPolySupport.Book.Ch04.isBigO_gammaSigma_restrictionDescendantAverage_of_restrictionUnitRangeDependentLaw_aemeasurable
{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_aemeas : ∀ R ∈ descendantsAtScale Q k, AEMeasurable (X R) P)
(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)