Coarse-graining support: Support.Book.Ch04.Theorems.PartitionAverageMoments.OnCube #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Restriction-carrier partition-average moment estimates: parent-cube and response averages #
theorem
HCPolySupport.Book.Ch04.integral_abs_centeredDescendantMean_pow_rpow_inv_le_of_unitRangeLaw
{d : ℕ}
{Q : TriadicCube d}
{n : ℤ}
{P : RestrictionCoeffLaw d}
[MeasureTheory.IsProbabilityMeasure P]
{p : ℕ}
{K : ℝ}
(hn : 0 ≤ n)
(hnQ : n ≤ Q.scale)
(hPstat : RestrictionStationaryLaw P)
(hPdep : RestrictionUnitRangeDependentLaw P)
(X : Set (Vec d) → RegCoeffField d → ℝ)
(hX_local : ∀ R ∈ descendantsAtScale Q n, IsRestrictionLocalRandomVariable (cubeSet R) ⋯ (X (cubeSet R)))
(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)
(hp : 2 ≤ p)
(hK_nonneg : 0 ≤ K)
(hX0Lp_int :
MeasureTheory.Integrable (fun (a : RegCoeffField d) => |restrictionCenteredOriginObservable P n X a| ^ p) P)
(hX0Lp : (∫ (a : RegCoeffField d), |restrictionCenteredOriginObservable P n X a| ^ p ∂P) ^ (1 / ↑p) ≤ K)
:
(∫ (a : RegCoeffField d), |restrictionCenteredDescendantAverageOnCube P Q n X a| ^ p ∂P) ^ (1 / ↑p) ≤ (↑(descendantsAtScale Q n).card)⁻¹ * (rosenthalDescendantsAtScaleLpConst d n p * ↑(descendantsAtScale Q n).card ^ (1 / ↑p) * K + rosenthalDescendantsAtScaleSqrtConst d n p * √↑(descendantsAtScale Q n).card * K)
Centered polynomial-moment fluctuation bound for restriction-centered descendant averages over an arbitrary parent cube.
theorem
HCPolySupport.Book.Ch04.integral_abs_centeredDescendantMean_pow_rpow_inv_le_of_of_unitRangeLaw
{d : ℕ}
{Q : TriadicCube d}
{n : ℤ}
{P : RestrictionCoeffLaw d}
[MeasureTheory.IsProbabilityMeasure P]
{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)
(hp : 2 ≤ p)
(hK_nonneg : 0 ≤ K)
(hX0Lp_int :
MeasureTheory.Integrable (fun (a : RegCoeffField d) => |restrictionCenteredOriginObservable P n X a| ^ p) P)
(hX0Lp : (∫ (a : RegCoeffField d), |restrictionCenteredOriginObservable P n X a| ^ p ∂P) ^ (1 / ↑p) ≤ K)
:
(∫ (a : RegCoeffField d), |restrictionCenteredDescendantAverageOnCube P Q n X a| ^ p ∂P) ^ (1 / ↑p) ≤ (↑(descendantsAtScale Q n).card)⁻¹ * (rosenthalDescendantsAtScaleLpConst d n p * ↑(descendantsAtScale Q n).card ^ (1 / ↑p) * K + rosenthalDescendantsAtScaleSqrtConst d n p * √↑(descendantsAtScale Q n).card * K)
Completed-local version of
integral_abs_centeredDescendantMean_pow_rpow_inv_le_of_unitRangeLaw.
The raw observable is allowed to be only a.e.-equal, under the law, to local representatives on the finitely many descendant cubes. This is the honest surface for totalized Ch4 observables such as coarse-block entries: stationarity and moment transfer use the raw translation-covariant observable, while unit-range independence is applied to the local representatives internally.