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

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

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.lowerRightNorm_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).lowerRight 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).lowerRight 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).lowerRight 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).lowerRight - Ch02.matrixNorm center) 0) ≤ ↑(Fintype.card (Fin d)) * ↑(Fintype.card (Fin d)) * (↑parents.card ^ (1 / ↑ξ) * B)

Lower-right 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.upperLeft_entry_le_LambdaSqCoeffField_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) : (fun (a : RegCoeffField d) => (coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft 0 0) ≤ᵐ[P] fun (a : RegCoeffField d) => LambdaSqCoeffField Q s (Ch02.MultiscaleExponent.finite 1) a

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.lowerRight_entry_le_lambdaSqCoeffField_inv_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) : (fun (a : RegCoeffField d) => (coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight 0 0) ≤ᵐ[P] fun (a : RegCoeffField d) => (lambdaSqCoeffField Q s (Ch02.MultiscaleExponent.finite 1) a)⁻¹

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.upperLeft_abs_entry_le_LambdaSqCoeffField_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (i j : Fin d) : (fun (a : RegCoeffField d) => |(coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft i j|) ≤ᵐ[P] fun (a : RegCoeffField d) => LambdaSqCoeffField Q s (Ch02.MultiscaleExponent.finite 1) a

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.lowerRight_abs_entry_le_lambdaSqCoeffField_inv_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (i j : Fin d) : (fun (a : RegCoeffField d) => |(coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight i j|) ≤ᵐ[P] fun (a : RegCoeffField d) => (lambdaSqCoeffField Q s (Ch02.MultiscaleExponent.finite 1) a)⁻¹

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.integrable_abs_pow_of_ae_abs_le_nonneg {d : ℕ} {P : RestrictionCoeffLaw d} {ξ : ℕ} {X Y : RegCoeffField d → ℝ} (hX_meas : AEMeasurable X P) (hY_nonneg : ∀ᵐ (a : RegCoeffField d) ∂P, 0 ≤ Y a) (hXY : (fun (a : RegCoeffField d) => |X a|) ≤ᵐ[P] Y) (hY_pow_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Y a ^ ξ) P) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |X a| ^ ξ) P

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.restrictionOriginUpperLeftMomentRoot_le_twoLambdaMoment {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) {s : ℝ} {ξ : ℕ} (hs : 0 < s) (hξ : 1 ≤ ξ) (hUpperPowInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => LambdaSqCoeffField (originCube d 0) s (Ch02.MultiscaleExponent.finite 1) a ^ ξ) P) (i j : Fin d) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |restrictionCenteredOriginObservable P 0 (fun (U : Set (Vec d)) (a : RegCoeffField d) => (coarseBlockMatrix U a.toFun).upperLeft i j) a| ^ ξ) P ∧ (∫ (a : RegCoeffField d), |restrictionCenteredOriginObservable P 0 (fun (U : Set (Vec d)) (a : RegCoeffField d) => (coarseBlockMatrix U a.toFun).upperLeft i j) a| ^ ξ ∂P) ^ (1 / ↑ξ) ≤ 2 * LambdaMomentAtScale P 0 s ξ

Unit-scale centered upper-left entries have their L^ξ roots controlled by the unit upper multiscale ellipticity moment.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.centeredOriginLowerRightEntry_momentRoot_le_twoLambdaInvMoment {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) {s : ℝ} {ξ : ℕ} (hs : 0 < s) (hξ : 1 ≤ ξ) (hLowerPowInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => (lambdaSqCoeffField (originCube d 0) s (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ ξ) P) (i j : Fin d) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |restrictionCenteredOriginObservable P 0 (fun (U : Set (Vec d)) (a : RegCoeffField d) => (coarseBlockMatrix U a.toFun).lowerRight i j) a| ^ ξ) P ∧ (∫ (a : RegCoeffField d), |restrictionCenteredOriginObservable P 0 (fun (U : Set (Vec d)) (a : RegCoeffField d) => (coarseBlockMatrix U a.toFun).lowerRight i j) a| ^ ξ ∂P) ^ (1 / ↑ξ) ≤ 2 * lambdaInvMomentAtScale P 0 s ξ

Unit-scale centered lower-right entries have their L^ξ roots controlled by the unit lower inverse multiscale ellipticity moment.