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

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

Restriction-carrier partition-average moment estimates: integrability

theorem HCPolySupport.Book.Ch04.integrable_abs_pow_restrictionCenteredDescendantAverage_of_stationary_of_isTranslationCovariant {d : ℕ} {n m : ℤ} {P : RestrictionCoeffLaw d} {p : ℕ} (hn : 0 ≤ n) (hnm : n ≤ m) (hPstat : RestrictionStationaryLaw P) (X : Set (Vec d) → RegCoeffField d → ℝ) (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 : 1 ≤ p) (hX0Lp_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |restrictionCenteredOriginObservable P n X a| ^ p) P) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |restrictionCenteredDescendantAverage P n m X a| ^ p) P

Integrability of the centered descendant average follows from the corresponding centered origin-cube moment by stationarity and translation covariance.

theorem HCPolySupport.Book.Ch04.integrable_abs_pow_restrictionCenteredDescendantAverage_of_stationary {d : ℕ} {n m : ℤ} {P : RestrictionCoeffLaw d} {p : ℕ} (hn : 0 ≤ n) (hnm : n ≤ m) (hPstat : RestrictionStationaryLaw P) (X : Set (Vec d) → RegCoeffField d → ℝ) (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 : 1 ≤ p) (hX0Lp_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |restrictionCenteredOriginObservable P n X a| ^ p) P) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |restrictionCenteredDescendantAverage P n m X a| ^ p) P

Integrability of the centered descendant average follows from the corresponding centered origin-cube moment by stationarity.

theorem HCPolySupport.Book.Ch04.integrable_abs_pow_centeredDescendantMean_of_stationary {d : ℕ} {Q : TriadicCube d} {n : ℤ} {P : RestrictionCoeffLaw d} {p : ℕ} (hn : 0 ≤ n) (hnQ : n ≤ Q.scale) (hPstat : RestrictionStationaryLaw P) (X : Set (Vec d) → RegCoeffField d → ℝ) (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 : 1 ≤ p) (hX0Lp_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |restrictionCenteredOriginObservable P n X a| ^ p) P) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |restrictionCenteredDescendantAverageOnCube P Q n X a| ^ p) P

Integrability of the centered descendant average over an arbitrary parent cube follows from the corresponding centered origin-cube moment by stationarity and translation covariance.

theorem HCPolySupport.Book.Ch04.integrable_abs_pow_restrictionCenteredDescendantAverageOnCube_of_stationary {d : ℕ} {Q : TriadicCube d} {n : ℤ} {P : RestrictionCoeffLaw d} {p : ℕ} (hn : 0 ≤ n) (hnQ : n ≤ Q.scale) (hPstat : RestrictionStationaryLaw P) (X : Set (Vec d) → RegCoeffField d → ℝ) (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 : 1 ≤ p) (hX0Lp_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |restrictionCenteredOriginObservable P n X a| ^ p) P) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |restrictionCenteredDescendantAverageOnCube P Q n X a| ^ p) P

Integrability of the centered descendant average over an arbitrary parent cube follows from the corresponding centered origin-cube moment by stationarity.

theorem HCPolySupport.Book.Ch04.integrable_finsetSup_abs_restrictionCenteredDescendantAverageOnCube_pow_of_stationary {d : ℕ} {n : ℤ} {P : RestrictionCoeffLaw d} {parents : Finset (TriadicCube d)} (hparents : parents.Nonempty) {p : ℕ} (hn : 0 ≤ n) (hparent_scale : ∀ Q ∈ parents, n ≤ Q.scale) (hPstat : RestrictionStationaryLaw P) (X : Set (Vec d) → RegCoeffField d → ℝ) (hX_cov : IsRestrictionTranslationCovariant X) (hX0_aemeas : AEMeasurable (X (cubeSet (originCube d n))) P) (hX_desc_aemeas : ∀ Q ∈ parents, ∀ R ∈ descendantsAtScale Q n, AEMeasurable (X (cubeSet R)) P) (hp : 1 ≤ p) (hX0Lp_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |restrictionCenteredOriginObservable P n X a| ^ p) P) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => (parents.sup' hparents fun (Q : TriadicCube d) => |restrictionCenteredDescendantAverageOnCube P Q n X a|) ^ p) P

Integrability of the finite parent maximum of centered descendant averages.

This is the integrability half of the public finite-parent moment estimate; it is useful when a downstream theorem first compares another observable to this finite maximum and then applies the Ch4 moment bound.