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

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

Restriction-carrier partition-average moment estimates

This file exposes the finite-moment partition-average estimate against the clean Chapter 4 observable surface. The hypotheses are direct: locality on the descendant cubes, translation covariance, measurability, and the origin-cube moment input.

theorem HCPolySupport.Book.Ch04.integral_finsetSup_abs_pow_rpow_inv_le_card_rpow_mul {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {s : Finset ι} (hs : s.Nonempty) {p : ℕ} {K : ℝ} (hp : 1 ≤ p) (hK_nonneg : 0 ≤ K) (X : ι → Ω → ℝ) (hX_aemeas : ∀ i ∈ s, AEMeasurable (X i) μ) (hX_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => |X i ω| ^ p) μ) (hX_root : ∀ i ∈ s, (∫ (ω : Ω), |X i ω| ^ p ∂μ) ^ (1 / ↑p) ≤ K) : (∫ (ω : Ω), (s.sup' hs fun (i : ι) => |X i ω|) ^ p ∂μ) ^ (1 / ↑p) ≤ ↑s.card ^ (1 / ↑p) * K

A finite supremum costs only card ^ (1 / p) in an L^p root when each observable has L^p root bounded by the same constant.

theorem HCPolySupport.Book.Ch04.integral_finiteSupAbs_centeredDescendantMean_pow_rpow_inv_le {d : ℕ} {n : ℤ} {P : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] {parents : Finset (TriadicCube d)} (hparents : parents.Nonempty) {p : ℕ} {K B : ℝ} (hn : 0 ≤ n) (hparent_scale : ∀ Q ∈ parents, n ≤ Q.scale) (hPstat : RestrictionStationaryLaw P) (hPdep : RestrictionUnitRangeDependentLaw P) (X : Set (Vec d) → RegCoeffField d → ℝ) (hX_local : ∀ Q ∈ parents, ∀ 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 : ∀ Q ∈ parents, ∀ R ∈ descendantsAtScale Q n, AEMeasurable (X (cubeSet R)) P) (hp : 2 ≤ p) (hK_nonneg : 0 ≤ K) (hB_nonneg : 0 ≤ B) (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) (hB : ∀ Q ∈ parents, (↑(descendantsAtScale Q n).card)⁻¹ * (rosenthalDescendantsAtScaleLpConst d n p * ↑(descendantsAtScale Q n).card ^ (1 / ↑p) * K + rosenthalDescendantsAtScaleSqrtConst d n p * √↑(descendantsAtScale Q n).card * K) ≤ B) : (∫ (a : RegCoeffField d), (parents.sup' hparents fun (Q : TriadicCube d) => |restrictionCenteredDescendantAverageOnCube P Q n X a|) ^ p ∂P) ^ (1 / ↑p) ≤ ↑parents.card ^ (1 / ↑p) * B

Finite-parent maximum of restriction-centered descendant averages, using the restriction-unit-range partition-average moment theorem on each parent cube.

This is the Ch4 probabilistic block behind the one-scale fluctuation estimate in the Section 5.2 multiscale ellipticity moment lemma: the finite maximum over parents costs only parents.card ^ (1 / p) after the per-parent Rosenthal bound has been proved.

theorem HCPolySupport.Book.Ch04.integral_finiteSupAbs_centeredDescendantMean_pow_rpow_inv_le_of_unitRangeLaw {d : ℕ} {n : ℤ} {P : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] {parents : Finset (TriadicCube d)} (hparents : parents.Nonempty) {p : ℕ} {K B : ℝ} (hP : RestrictionLawCarrier P) (hn : 0 ≤ n) (hparent_scale : ∀ Q ∈ parents, n ≤ Q.scale) (hPstat : RestrictionStationaryLaw P) (hPdep : RestrictionUnitRangeDependentLaw P) (X : Set (Vec d) → RegCoeffField d → ℝ) (hX_localRep : ∀ Q ∈ parents, ∀ 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 : ∀ Q ∈ parents, ∀ R ∈ descendantsAtScale Q n, AEMeasurable (X (cubeSet R)) P) (hp : 2 ≤ p) (hK_nonneg : 0 ≤ K) (hB_nonneg : 0 ≤ B) (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) (hB : ∀ Q ∈ parents, (↑(descendantsAtScale Q n).card)⁻¹ * (rosenthalDescendantsAtScaleLpConst d n p * ↑(descendantsAtScale Q n).card ^ (1 / ↑p) * K + rosenthalDescendantsAtScaleSqrtConst d n p * √↑(descendantsAtScale Q n).card * K) ≤ B) : (∫ (a : RegCoeffField d), (parents.sup' hparents fun (Q : TriadicCube d) => |restrictionCenteredDescendantAverageOnCube P Q n X a|) ^ p ∂P) ^ (1 / ↑p) ≤ ↑parents.card ^ (1 / ↑p) * B

Completed-local finite-parent version of integral_finiteSupAbs_centeredDescendantMean_pow_rpow_inv_le.

The caller supplies raw translation-covariant observables and Ch4 supplies local representatives on each descendant cube. This is the form used by law-facing coarse-block fluctuation estimates, where the raw totalized observable is a.e.-equal to a local-test representative but is not itself definitionally local.

theorem HCPolySupport.Book.Ch04.integral_abs_restrictionCenteredDescendantAverage_le_of_restrictionUnitRangeDependentLaw {d : ℕ} {n m : ℤ} {P : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure 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) (hξ : 2 ≤ ξ) (hK_nonneg : 0 ≤ K) (hX0ξ_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |restrictionCenteredOriginObservable P n X a| ^ ξ) P) (hX0ξ : (∫ (a : RegCoeffField d), |restrictionCenteredOriginObservable P n X a| ^ ξ ∂P) ^ (1 / ↑ξ) ≤ K) : ∫ (a : RegCoeffField d), |restrictionCenteredDescendantAverage P n m X a| ∂P ≤ (↑(descendantsAtScale (originCube d m) n).card)⁻¹ * (rosenthalDescendantsAtScaleLpConst d n 2 * √↑(descendantsAtScale (originCube d m) n).card * K + rosenthalDescendantsAtScaleSqrtConst d n 2 * √↑(descendantsAtScale (originCube d m) n).card * K)

Low-moment finite partition-average fluctuation estimate with explicit Rosenthal constants.