Coarse-graining support: Support.Book.Ch04.Theorems.PartitionAverageMoments.CenteredAverage

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

Restriction-carrier partition-average moment estimates: centered descendant averages

theorem HCPolySupport.Book.Ch04.centeredDescendantAverageMomentRoot_le_of_unitRangeLaw {d : ℕ} {n m : ℤ} {P : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] {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_aemeas : AEMeasurable (X (cubeSet (originCube d n))) P) (hX_desc_aemeas : ∀ R ∈ descendantsAtScale (originCube d m) 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), |restrictionCenteredDescendantAverage P n m X a| ^ p ∂P) ^ (1 / ↑p) ≤ (↑(descendantsAtScale (originCube d m) n).card)⁻¹ * (rosenthalDescendantsAtScaleLpConst d n p * ↑(descendantsAtScale (originCube d m) n).card ^ (1 / ↑p) * K + rosenthalDescendantsAtScaleSqrtConst d n p * √↑(descendantsAtScale (originCube d m) n).card * K)

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