Coarse-graining support: Support.Book.Ch04.Theorems.MomentFactorBounds.Helpers

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

Moment factor bounds

This file exposes Chapter 4 scalar factor bounds used to compare the structural contrast Theta_n with the moment-enhanced quantity widetildeTheta_n.

@[reducible, inline]

abbrev HCPolySupport.Book.Ch04.AnnealedPrimitiveScalarizationFamily {d : ℕ} [NeZero d] (P : RestrictionCoeffLaw d) : Prop

Proof-local primitive scalarization data at every nonnegative scale.

Equations

• HCPolySupport.Book.Ch04.AnnealedPrimitiveScalarizationFamily P = ∀ (n : ℕ), HCPolySupport.Book.Ch04.Internal.AnnealedPrimitiveScalarizationData P ↑n

structure HCPolySupport.Book.Ch04.AnnealedPrimitiveMomentFactorBounds {d : ℕ} [NeZero d] (P : RestrictionCoeffLaw d) (sUpper sLower : ℝ) (ξ : ℕ) : Prop

Proof-local scalar factor bounds used to compare Theta_n with widetildeTheta_n internally.

• upper (primitive : AnnealedPrimitiveScalarizationFamily P) (n : ℕ) : Internal.barBAtScaleOfPrimitive ⋯ ≤ LambdaMomentAtScale P (↑n) sUpper ξ
• lower (primitive : AnnealedPrimitiveScalarizationFamily P) (n : ℕ) : Internal.barSigmaStarInvAtScaleOfPrimitive ⋯ ≤ lambdaInvMomentAtScale P (↑n) sLower ξ

theorem HCPolySupport.Book.Ch04.toReal_eLpNorm_eq_integral_norm_pow_rpow_inv {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {f : Ω → ℝ} {p : ℕ} (hp : 1 ≤ p) (hmem : MeasureTheory.MemLp f (↑p) μ) : (MeasureTheory.eLpNorm f (↑p) μ).toReal = (∫ (x : Ω), ‖f x‖ ^ p ∂μ) ^ (1 / ↑p)

theorem HCPolySupport.Book.Ch04.integrable_of_ae_nonneg_pow_integrable {d : ℕ} {P : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] {ξ : ℕ} {X : RegCoeffField d → ℝ} (hξ : 1 ≤ ξ) (hX_meas : AEMeasurable X P) (hX_nonneg : ∀ᵐ (a : RegCoeffField d) ∂P, 0 ≤ X a) (hXpow_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => X a ^ ξ) P) : MeasureTheory.Integrable X P

theorem HCPolySupport.Book.Ch04.integral_le_annealedMomentRoot_of_ae_nonneg {d : ℕ} {P : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] {ξ : ℕ} {X : RegCoeffField d → ℝ} (hξ : 1 ≤ ξ) (hX_meas : AEMeasurable X P) (hX_nonneg : ∀ᵐ (a : RegCoeffField d) ∂P, 0 ≤ X a) (hXpow_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => X a ^ ξ) P) : ∫ (a : RegCoeffField d), X a ∂P ≤ annealedMomentRoot P ξ X

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.finsetSup_abs_restrictionCenteredDescendantAverageOnCube_nonneg {d : ℕ} {n : ℤ} {P : RestrictionCoeffLaw d} {parents : Finset (TriadicCube d)} (hparents : parents.Nonempty) (X : Set (Vec d) → RegCoeffField d → ℝ) (a : RegCoeffField d) : 0 ≤ parents.sup' hparents fun (Q : TriadicCube d) => |restrictionCenteredDescendantAverageOnCube P Q n X a|

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_finsetSup_abs_restrictionCenteredDescendantAverageOnCube {d : ℕ} {n : ℤ} {P : RestrictionCoeffLaw d} {parents : Finset (TriadicCube d)} (hparents : parents.Nonempty) (X : Set (Vec d) → RegCoeffField d → ℝ) (hX_desc_aemeas : ∀ Q ∈ parents, ∀ R ∈ descendantsAtScale Q n, AEMeasurable (X (cubeSet R)) P) : AEMeasurable (fun (a : RegCoeffField d) => parents.sup' hparents fun (Q : TriadicCube d) => |restrictionCenteredDescendantAverageOnCube P Q n X a|) P

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_upperLeft_matrixNorm_positiveExcess_finsetSup {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) {parents : Finset (TriadicCube d)} (hparents : parents.Nonempty) (center : Mat d) : AEMeasurable (fun (a : RegCoeffField d) => parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft - Ch02.matrixNorm center) 0) P

AEMeasurability of the upper-left finite-parent positive excess for the operator norm of coarse blocks.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_lowerRight_matrixNorm_positiveExcess_finsetSup {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) {parents : Finset (TriadicCube d)} (hparents : parents.Nonempty) (center : Mat d) : AEMeasurable (fun (a : RegCoeffField d) => parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight - Ch02.matrixNorm center) 0) P

AEMeasurability of the lower-right finite-parent positive excess for the operator norm of coarse blocks.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.momentRoot_excess_le_card_mul_entryRootBound {d : ℕ} {P : RestrictionCoeffLaw d} {ξ : ℕ} {C : ℝ} (hξ : 1 ≤ ξ) (excess : RegCoeffField d → ℝ) (entry : Fin d → Fin d → RegCoeffField d → ℝ) (hexcess_nonneg : ∀ (a : RegCoeffField d), 0 ≤ excess a) (hexcess_aemeas : AEMeasurable excess P) (hentry_nonneg : ∀ (i j : Fin d) (a : RegCoeffField d), 0 ≤ entry i j a) (hentry_aemeas : ∀ (i j : Fin d), AEMeasurable (entry i j) P) (hentry_int : ∀ (i j : Fin d), MeasureTheory.Integrable (fun (a : RegCoeffField d) => |entry i j a| ^ ξ) P) (hentry_root : ∀ (i j : Fin d), (∫ (a : RegCoeffField d), |entry i j a| ^ ξ ∂P) ^ (1 / ↑ξ) ≤ C) (hpoint : excess ≤ᵐ[P] fun (a : RegCoeffField d) => ∑ i : Fin d, ∑ j : Fin d, entry i j a) : annealedMomentRoot P ξ excess ≤ ↑(Fintype.card (Fin d)) * ↑(Fintype.card (Fin d)) * C

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.upperLeftPositiveMatrixNormExcess_integrable {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) {parents : Finset (TriadicCube d)} (hparents : parents.Nonempty) {n : ℤ} {ξ : ℕ} (hn : 0 ≤ n) (hparent_scale : ∀ Q ∈ parents, n ≤ Q.scale) (hPstat : RestrictionStationaryLaw P) (center : Mat d) (hcenter : ∀ (i j : Fin d), center i j = ∫ (b : RegCoeffField d), (coarseBlockMatrix (cubeSet (originCube d n)) b.toFun).upperLeft i j ∂P) (hξ : 2 ≤ ξ) (hOriginLp_int : ∀ (i j : Fin d), MeasureTheory.Integrable (fun (a : RegCoeffField d) => |restrictionCenteredOriginObservable P n (fun (U : Set (Vec d)) (a : RegCoeffField d) => (coarseBlockMatrix U a.toFun).upperLeft i j) a| ^ ξ) P) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => ‖parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft - Ch02.matrixNorm center) 0‖ ^ ξ) P

Integrability of the upper-left finite-parent operator-norm positive excess. This is the integrability half of upperLeft_matrixNorm_positiveExcess_finsetSup_momentRoot_le_of_restrictionUnitRangeDependentLaw.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.upperLeftNorm_positiveExcess_momentRoot_le_of_unitRangeLaw {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) {parents : Finset (TriadicCube d)} (hparents : parents.Nonempty) {n : ℤ} {ξ : ℕ} {K B : ℝ} (hn : 0 ≤ n) (hparent_scale : ∀ Q ∈ parents, n ≤ Q.scale) (hPstat : RestrictionStationaryLaw P) (hPdep : RestrictionUnitRangeDependentLaw P) (center : Mat d) (hcenter : ∀ (i j : Fin d), center i j = ∫ (b : RegCoeffField d), (coarseBlockMatrix (cubeSet (originCube d n)) b.toFun).upperLeft i j ∂P) (hξ : 2 ≤ ξ) (hK_nonneg : 0 ≤ K) (hB_nonneg : 0 ≤ B) (hOriginLp_int : ∀ (i j : Fin d), MeasureTheory.Integrable (fun (a : RegCoeffField d) => |restrictionCenteredOriginObservable P n (fun (U : Set (Vec d)) (a : RegCoeffField d) => (coarseBlockMatrix U a.toFun).upperLeft i j) a| ^ ξ) P) (hOriginLp : ∀ (i j : Fin d), (∫ (a : RegCoeffField d), |restrictionCenteredOriginObservable P n (fun (U : Set (Vec d)) (a : RegCoeffField d) => (coarseBlockMatrix U a.toFun).upperLeft i j) a| ^ ξ ∂P) ^ (1 / ↑ξ) ≤ K) (hBudget : ∀ Q ∈ parents, (↑(descendantsAtScale Q n).card)⁻¹ * (rosenthalDescendantsAtScaleLpConst d n ξ * ↑(descendantsAtScale Q n).card ^ (1 / ↑ξ) * K + rosenthalDescendantsAtScaleSqrtConst d n ξ * √↑(descendantsAtScale Q n).card * K) ≤ B) : (annealedMomentRoot P ξ fun (a : RegCoeffField d) => parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft - Ch02.matrixNorm center) 0) ≤ ↑(Fintype.card (Fin d)) * ↑(Fintype.card (Fin d)) * (↑parents.card ^ (1 / ↑ξ) * B)

Upper-left finite-parent coarse-block fluctuation bound, stated directly against the law-facing Ch4 surface. The proof owns all locality, measurability, covariance, and deterministic positive-excess domination.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.lowerRightPositiveMatrixNormExcess_integrable {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) {parents : Finset (TriadicCube d)} (hparents : parents.Nonempty) {n : ℤ} {ξ : ℕ} (hn : 0 ≤ n) (hparent_scale : ∀ Q ∈ parents, n ≤ Q.scale) (hPstat : RestrictionStationaryLaw P) (center : Mat d) (hcenter : ∀ (i j : Fin d), center i j = ∫ (b : RegCoeffField d), (coarseBlockMatrix (cubeSet (originCube d n)) b.toFun).lowerRight i j ∂P) (hξ : 2 ≤ ξ) (hOriginLp_int : ∀ (i j : Fin d), MeasureTheory.Integrable (fun (a : RegCoeffField d) => |restrictionCenteredOriginObservable P n (fun (U : Set (Vec d)) (a : RegCoeffField d) => (coarseBlockMatrix U a.toFun).lowerRight i j) a| ^ ξ) P) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => ‖parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight - Ch02.matrixNorm center) 0‖ ^ ξ) P

Integrability of the lower-right finite-parent operator-norm positive excess. This is the integrability half of lowerRight_matrixNorm_positiveExcess_finsetSup_momentRoot_le_of_restrictionUnitRangeDependentLaw.