Coarse-graining support: Support.Book.Ch04.Theorems.AnnealedSubadditivity.LawCarrierFullBlock

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

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.integrable_coarseFullBlockMatrixAtCube_of_integrable_diagonalBlockNorms {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (hBInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => coarseBBlockNorm Q a.toFun) P) (hStarInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => coarseSigmaStarInvBlockNorm Q a.toFun) P) : MeasureTheory.Integrable (coarseFullBlockMatrixAtCube Q) P

Integrability of the two diagonal coarse-block norms implies integrability of the full doubled coarse block matrix.

This is the source theorem for the full-block hypotheses used by the public annealed subadditivity and scalarization endpoints. The mixed blocks are controlled by the positive definiteness of the Chapter 2 coarse block matrix, so downstream code should not assemble entrywise integrability by hand.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.integrable_coarseBlockMatrixEntry_of_integrableFullBlock {d : ℕ} {P : RestrictionCoeffLaw d} {Q : TriadicCube d} (hInt : MeasureTheory.Integrable (coarseFullBlockMatrixAtCube Q) P) (α β : BlockCoord d) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => blockMatEntry (coarseBlockMatrix (cubeSet Q) a.toFun) α β) P

Full coarse-block integrability gives entrywise integrability of the corresponding doubled coarse matrix.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.coarseBlockMatrix_lowerRight_posDef_cubeSet_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) : ∀ᵐ (a : RegCoeffField d) ∂P, Matrix.PosDef (coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight

Under a law carrier, the lower-right coarse block is a.e. positive definite on every deterministic triadic cube.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.coarseBlockMatrix_upperLeft_posDef_cubeSet_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) : ∀ᵐ (a : RegCoeffField d) ∂P, Matrix.PosDef (coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft

Under a law carrier, the upper-left coarse block is a.e. positive definite on every deterministic triadic cube.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.Internal.barSigmaStarInverse_pos_of_integrableBlockMatrix {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) {n : ℤ} (hPrim : Internal.AnnealedPrimitiveScalarizationData P n) (hBlock : MeasureTheory.Integrable (coarseFullBlockMatrixAtCube (originCube d n)) P) : 0 < hPrim.barSigmaStarInv

Full coarse-block integrability and primitive scalarization make the inverse-star scalar coefficient strictly positive.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.Internal.barB_pos_of_integrable_coarseFullBlockMatrixAtCube {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) {n : ℤ} (hPrim : Internal.AnnealedPrimitiveScalarizationData P n) (hBlock : MeasureTheory.Integrable (coarseFullBlockMatrixAtCube (originCube d n)) P) : 0 < hPrim.barB

Full coarse-block integrability and primitive scalarization make the upper-left scalar coefficient strictly positive.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.barSigmaAtScale_pos_of_integrable_coarseFullBlockMatrixAtCube {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hStruct : RestrictionStructuralLaw P) {n : ℤ} (hBlock : MeasureTheory.Integrable (coarseFullBlockMatrixAtCube (originCube d n)) P) : 0 < hP.barSigmaAtScale hStruct n

Full coarse-block integrability makes the public scalar \bar\sigma_n strictly positive.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.Internal.one_le_primitiveContrast_of_integrableCoarseBlock {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) {n : ℤ} (hPrim : Internal.AnnealedPrimitiveScalarizationData P n) (hBlock : MeasureTheory.Integrable (coarseFullBlockMatrixAtCube (originCube d n)) P) : 1 ≤ hPrim.contrast

Law-facing primitive lower bound 1 <= Theta_n, stated at the primitive scalarization level.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.Internal.barB_nonneg_of_integrable_coarseFullBlockMatrixAtCube {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) {n : ℤ} (hPrim : Internal.AnnealedPrimitiveScalarizationData P n) (hBlock : MeasureTheory.Integrable (coarseFullBlockMatrixAtCube (originCube d n)) P) : 0 ≤ hPrim.barB

Full coarse-block integrability and primitive scalarization make the upper-left scalar coefficient nonnegative.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.Internal.one_le_scalarContrast_of_integrableCoarseBlock {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) {n : ℤ} (hScal : Internal.AnnealedScalarizationTheory P) (hPrim : Internal.AnnealedPrimitiveScalarizationData P n) (hBlock : MeasureTheory.Integrable (coarseFullBlockMatrixAtCube (originCube d n)) P) : 1 ≤ hScal.contrast n

Law-facing scalar lower bound 1 <= Theta_n, stated for the public scalarization theory.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.blockMatLoewnerLE_annealedBlockMatrixAtScale_of_integrable_coarseFullBlockMatrixAtCube {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) {n m : ℤ} (hn : 0 ≤ n) (hnm : n ≤ m) (hParentInt : MeasureTheory.Integrable (coarseFullBlockMatrixAtCube (originCube d m)) P) (hDescInt : ∀ R ∈ descendantsAtScale (originCube d m) n, MeasureTheory.Integrable (coarseFullBlockMatrixAtCube R) P) : BlockMatLoewnerLE (annealedBlockMatrixAtScale P m) (annealedBlockMatrixAtScale P n)

Law-facing annealed block monotonicity from full coarse-block integrability. This is the Ch5-facing version of RestrictionLawCarrier.blockMatLoewnerLE_annealedBlockMatrixAtScale: downstream callers should not assemble entrywise integrability by hand.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.Internal.primitiveContrast_scaleChain_of_integrableCoarseBlocks {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) {n m : ℤ} (hn_nonneg : 0 ≤ n) (hnm : n ≤ m) (hScal : Internal.AnnealedScalarizationTheory P) (hPrim_m : Internal.AnnealedPrimitiveScalarizationData P m) (hPrim_n : Internal.AnnealedPrimitiveScalarizationData P n) (hParentInt : MeasureTheory.Integrable (coarseFullBlockMatrixAtCube (originCube d m)) P) (hDescInt : ∀ R ∈ descendantsAtScale (originCube d m) n, MeasureTheory.Integrable (coarseFullBlockMatrixAtCube R) P) (hStar_m_pos : 0 < hPrim_m.barSigmaStarInv) (hContrast_m : 1 ≤ hPrim_m.contrast) : hScal.barSigmaStar n ≤ hScal.barSigmaStar m ∧ hScal.barSigmaStar m ≤ hScal.barSigma m ∧ hScal.barSigma m ≤ hScal.barSigma n

Law-facing scalar chain from full coarse-block integrability.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.Internal.primitive_contrast_le_of_integrable_coarseFullBlockMatrixAtCube {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) {n m : ℤ} (hn_nonneg : 0 ≤ n) (hnm : n ≤ m) (hPrim_m : Internal.AnnealedPrimitiveScalarizationData P m) (hPrim_n : Internal.AnnealedPrimitiveScalarizationData P n) (hParentInt : MeasureTheory.Integrable (coarseFullBlockMatrixAtCube (originCube d m)) P) (hDescInt : ∀ R ∈ descendantsAtScale (originCube d m) n, MeasureTheory.Integrable (coarseFullBlockMatrixAtCube R) P) (hStar_m_nonneg : 0 ≤ hPrim_m.barSigmaStarInv) (hB_n_nonneg : 0 ≤ hPrim_n.barB) : hPrim_m.contrast ≤ hPrim_n.contrast

Law-facing primitive contrast monotonicity from full coarse-block integrability.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.Internal.scalarContrast_le_of_integrableCoarseBlocks {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) {n m : ℤ} (hn_nonneg : 0 ≤ n) (hnm : n ≤ m) (hScal : Internal.AnnealedScalarizationTheory P) (hPrim_m : Internal.AnnealedPrimitiveScalarizationData P m) (hPrim_n : Internal.AnnealedPrimitiveScalarizationData P n) (hParentInt : MeasureTheory.Integrable (coarseFullBlockMatrixAtCube (originCube d m)) P) (hDescInt : ∀ R ∈ descendantsAtScale (originCube d m) n, MeasureTheory.Integrable (coarseFullBlockMatrixAtCube R) P) (hStar_m_nonneg : 0 ≤ hPrim_m.barSigmaStarInv) (hB_n_nonneg : 0 ≤ hPrim_n.barB) : hScal.contrast m ≤ hScal.contrast n

Law-facing scalar contrast monotonicity from full coarse-block integrability.