Coarse-graining support: Support.Book.Ch05.Theorems.Section52.ScalarPreliminaries

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

Section 5.2 internals: ScalarPreliminaries

Scalar monotonicity, response identities, and tau nonnegativity.

theorem HCPolySupport.Book.Ch05.Section52.thetaAtScale_mono_of_integrable_diagonalBlockNorms {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {n m : ℤ} (hn_nonneg : 0 ≤ n) (hnm : n ≤ m) (hParentBInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => coarseBBlockNorm (originCube d m) a.toFun) P) (hParentStarInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => coarseSigmaStarInvBlockNorm (originCube d m) a.toFun) P) (hDescBInt : ∀ R ∈ descendantsAtScale (originCube d m) n, MeasureTheory.Integrable (fun (a : RegCoeffField d) => coarseBBlockNorm R a.toFun) P) (hDescStarInt : ∀ R ∈ descendantsAtScale (originCube d m) n, MeasureTheory.Integrable (fun (a : RegCoeffField d) => coarseSigmaStarInvBlockNorm R a.toFun) P) (hChildBlockInt : MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d n)) P) : thetaAtScale hP hStruct m ≤ thetaAtScale hP hStruct n

Scalar contrast monotonicity in Ch5 notation. The only inputs are the note-level integrability facts used to take expectations.

theorem HCPolySupport.Book.Ch05.Section52.thetaAtScale_mono_of_integrable_coarseFullBlockMatrixAtCube {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {n m : ℤ} (hn_nonneg : 0 ≤ n) (hnm : n ≤ m) (hParentBlockInt : MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d m)) P) (hChildBlockInt : MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d n)) P) (hDescBlockInt : ∀ R ∈ descendantsAtScale (originCube d m) n, MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube R) P) : thetaAtScale hP hStruct m ≤ thetaAtScale hP hStruct n

Scalar contrast monotonicity in Ch5 notation, with full coarse-block integrability as the only analytic input.

theorem HCPolySupport.Book.Ch05.Section52.tauAtScale_nonneg_of_integrable_restrictionResponseJObservableCubeSet {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) {k n : ℤ} (hk_nonneg : 0 ≤ k) (hkn : k ≤ n) (p q : Vec d) (hParentInt : MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet (originCube d n) p q) P) (hDescInt : ∀ R ∈ descendantsAtScale (originCube d n) k, MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet R p q) P) : 0 ≤ tauAtScale P n k p q

theorem HCPolySupport.Book.Ch05.Section52.tauAtScale_nonneg_of_integrable_coarseFullBlockMatrixAtCube {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) {k n : ℤ} (hk_nonneg : 0 ≤ k) (hkn : k ≤ n) (p q : Vec d) (hParentBlockInt : MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d n)) P) (hDescBlockInt : ∀ R ∈ descendantsAtScale (originCube d n) k, MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube R) P) : 0 ≤ tauAtScale P n k p q

Nonnegativity of the annealed additivity defect, with response integrability derived from full coarse-block integrability.

theorem HCPolySupport.Book.Ch05.Section52.annealedResponseJAtScale_eq_expectedJScalarFormula {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (n : ℤ) (p q : Vec d) (hBlock : MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d n)) P) : Ch04.annealedResponseJAtScale P n p q = expectedJScalarFormula hP hStruct n p q

Note-facing scalar response formula under the Chapter 4 law and structural assumptions.

theorem HCPolySupport.Book.Ch05.Section52.tauAtScale_eq_tauScalarFormula {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (n k : ℤ) (p q : Vec d) (hBlock_n : MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d n)) P) (hBlock_k : MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d k)) P) : tauAtScale P n k p q = tauScalarFormula hP hStruct n k p q

Note-facing scalar formula for τ_{n,k}.

theorem HCPolySupport.Book.Ch05.Section52.scalarPreliminaries_homogenizationScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (n m k : ℕ) (hnm : n ≤ m) (hkn : k ≤ n) (p q : Vec d) : 1 ≤ thetaAtScale hP hStruct ↑m ∧ thetaAtScale hP hStruct ↑m ≤ thetaAtScale hP hStruct ↑n ∧ thetaAtScale hP hStruct ↑n ≤ widetildeThetaAtScale P (↑n) hP4 ∧ Ch04.annealedResponseJAtScale P (↑n) p q = expectedJScalarFormula hP hStruct (↑n) p q ∧ tauAtScale P (↑n) (↑k) p q = tauScalarFormula hP hStruct (↑n) (↑k) p q ∧ 0 ≤ tauAtScale P (↑n) (↑k) p q

Manuscript Lemma l.scalar.preliminaries.homogenization.scale.

All integrability needed for scalar monotonicity, response identities, and moment-factor comparison is derived internally from the law carrier, structural law, and (P4) hypotheses.