Coarse-graining support: Support.Book.Ch04.Theorems.PartitionAverageMoments.Rosenthal #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Restriction-local partition-average moment estimates: Rosenthal bounds #
theorem
HCPolySupport.Book.Ch04.integral_abs_finiteSum_pow_rpow_inv_le_rosenthal_descendantScaleColorClass
{d : ℕ}
{Q : TriadicCube d}
{k : ℤ}
{c : ScaleColor d k}
{P : RestrictionCoeffLaw d}
[MeasureTheory.IsProbabilityMeasure P]
{p : ℕ}
{K : ℝ}
(hP : RestrictionUnitRangeDependentLaw P)
(hp : 2 ≤ p)
(hK_nonneg : 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)
(hLp_int :
∀ R ∈ descendantsAtScaleScaleColorClass Q k c, MeasureTheory.Integrable (fun (a : RegCoeffField d) => |X R a| ^ p) P)
(h_mean : ∀ R ∈ descendantsAtScaleScaleColorClass Q k c, ∫ (a : RegCoeffField d), X R a ∂P = 0)
(hK : ∀ R ∈ descendantsAtScaleScaleColorClass Q k c, (∫ (a : RegCoeffField d), |X R a| ^ p ∂P) ^ (1 / ↑p) ≤ K)
:
Rosenthal's L^p bound on a single scale-color class of descendants under
the restriction-unit-range and restriction-local-random-variable assumptions.
theorem
HCPolySupport.Book.Ch04.integral_abs_finiteSum_pow_rpow_inv_le_rosenthal_uniform_descendants
{d : ℕ}
{Q : TriadicCube d}
{k : ℤ}
{P : RestrictionCoeffLaw d}
[MeasureTheory.IsProbabilityMeasure P]
{p : ℕ}
{K : ℝ}
(hP : RestrictionUnitRangeDependentLaw P)
(hp : 2 ≤ p)
(hK_nonneg : 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)
(hLp_int : ∀ R ∈ descendantsAtScale Q k, MeasureTheory.Integrable (fun (a : RegCoeffField d) => |X R a| ^ p) P)
(h_mean : ∀ R ∈ descendantsAtScale Q k, ∫ (a : RegCoeffField d), X R a ∂P = 0)
(hK : ∀ R ∈ descendantsAtScale Q k, (∫ (a : RegCoeffField d), |X R a| ^ p ∂P) ^ (1 / ↑p) ≤ K)
:
(∫ (a : RegCoeffField d), |∑ R ∈ descendantsAtScale Q k, X R a| ^ p ∂P) ^ (1 / ↑p) ≤ rosenthalDescendantsAtScaleLpConst d k p * ↑(descendantsAtScale Q k).card ^ (1 / ↑p) * K + rosenthalDescendantsAtScaleSqrtConst d k p * √↑(descendantsAtScale Q k).card * K
Rosenthal's L^p bound for sums over all descendants at a fixed scale,
using the restriction-local and restriction-unit-range interfaces.