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

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

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.annealedResponseJAtScale_le {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) {n m : ℤ} (hn : 0 ≤ n) (hnm : n ≤ m) (p q : Vec d) (hParentInt : MeasureTheory.Integrable (restrictionResponseJObservableCubeSet (originCube d m) p q) P) (hDescInt : ∀ R ∈ descendantsAtScale (originCube d m) n, MeasureTheory.Integrable (restrictionResponseJObservableCubeSet R p q) P) : annealedResponseJAtScale P m p q ≤ annealedResponseJAtScale P n p q

Law-facing annealed response subadditivity. Ch4 supplies the deterministic a.e. descendant comparison; callers only provide the integrability and stationarity hypotheses used by the expectation step.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.blockMatLoewnerLE_annealedBlockMatrixAtScale {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) {n m : ℤ} (hn : 0 ≤ n) (hnm : n ≤ m) (hParentInt : ∀ (α β : BlockCoord d), MeasureTheory.Integrable (fun (a : RegCoeffField d) => blockMatEntry (coarseBlockMatrix (cubeSet (originCube d m)) a.toFun) α β) P) (hDescInt : ∀ R ∈ descendantsAtScale (originCube d m) n, ∀ (α β : BlockCoord d), MeasureTheory.Integrable (fun (a : RegCoeffField d) => blockMatEntry (coarseBlockMatrix (cubeSet R) a.toFun) α β) P) : BlockMatLoewnerLE (annealedBlockMatrixAtScale P m) (annealedBlockMatrixAtScale P n)

Law-facing annealed block monotonicity. Ch4 supplies the deterministic a.e. block comparison and the stationarity step; callers provide only the entrywise integrability needed to take expectations.

theorem HCPolySupport.Book.Ch04.blockMatLoewnerLE_annealedStarredBlockMatrixInvAtScale_of_block {d : ℕ} {P : RestrictionCoeffLaw d} {n m : ℤ} (hBlock : BlockMatLoewnerLE (annealedBlockMatrixAtScale P m) (annealedBlockMatrixAtScale P n)) : BlockMatLoewnerLE (annealedStarredBlockMatrixInvAtScale P m) (annealedStarredBlockMatrixInvAtScale P n)

The starred annealed block monotonicity follows from annealed block monotonicity by the built-in block reflection.

theorem HCPolySupport.Book.Ch04.matLoewnerLE_annealedSigmaStarInvAtScale_of_block {d : ℕ} {P : RestrictionCoeffLaw d} {n m : ℤ} (hBlock : BlockMatLoewnerLE (annealedBlockMatrixAtScale P m) (annealedBlockMatrixAtScale P n)) : MatLoewnerLE (annealedSigmaStarInvAtScale P m) (annealedSigmaStarInvAtScale P n)

Matrix monotonicity of σ_*⁻¹ follows from annealed block monotonicity.

theorem HCPolySupport.Book.Ch04.matLoewnerLE_annealedBAtScale_of_block {d : ℕ} {P : RestrictionCoeffLaw d} {n m : ℤ} (hBlock : BlockMatLoewnerLE (annealedBlockMatrixAtScale P m) (annealedBlockMatrixAtScale P n)) : MatLoewnerLE (annealedBAtScale P m) (annealedBAtScale P n)

Matrix monotonicity of b follows from annealed block monotonicity.

theorem HCPolySupport.Book.Ch04.scalar_chain_of_primitive_block_mono {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n m : ℤ} (hScal : Internal.AnnealedScalarizationTheory P) (hm : Internal.AnnealedPrimitiveScalarizationData P m) (hn : Internal.AnnealedPrimitiveScalarizationData P n) (hBlock : BlockMatLoewnerLE (annealedBlockMatrixAtScale P m) (annealedBlockMatrixAtScale P n)) (hStar_m_pos : 0 < hm.barSigmaStarInv) (hContrast_m : 1 ≤ hm.contrast) : hScal.barSigmaStar n ≤ hScal.barSigmaStar m ∧ hScal.barSigmaStar m ≤ hScal.barSigma m ∧ hScal.barSigma m ≤ hScal.barSigma n

The scalar chain \barσ_{*,n} ≤ \barσ_{*,m} ≤ \barσ_m ≤ \barσ_n from primitive scalarization data and annealed block monotonicity.

theorem HCPolySupport.Book.Ch04.primitive_contrast_le_of_block_mono {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n m : ℤ} (hm : Internal.AnnealedPrimitiveScalarizationData P m) (hn : Internal.AnnealedPrimitiveScalarizationData P n) (hBlock : BlockMatLoewnerLE (annealedBlockMatrixAtScale P m) (annealedBlockMatrixAtScale P n)) (hStar_m_nonneg : 0 ≤ hm.barSigmaStarInv) (hB_n_nonneg : 0 ≤ hn.barB) : hm.contrast ≤ hn.contrast

Primitive contrast monotonicity from primitive scalarization data and annealed block monotonicity.

theorem HCPolySupport.Book.Ch04.scalar_contrast_le_of_primitive_block_mono {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n m : ℤ} (hScal : Internal.AnnealedScalarizationTheory P) (hm : Internal.AnnealedPrimitiveScalarizationData P m) (hn : Internal.AnnealedPrimitiveScalarizationData P n) (hBlock : BlockMatLoewnerLE (annealedBlockMatrixAtScale P m) (annealedBlockMatrixAtScale P n)) (hStar_m_nonneg : 0 ≤ hm.barSigmaStarInv) (hB_n_nonneg : 0 ≤ hn.barB) : hScal.contrast m ≤ hScal.contrast n

Scalar contrast monotonicity from primitive scalarization data and annealed block monotonicity, stated for the public scalarization theory.

theorem HCPolySupport.Book.Ch04.abs_blockMatEntry_le_diagonalBlockNorms_of_symm_pos {d : ℕ} {A : BlockMat d} (hSymm : IsSymmetricBlockMat A) (hPos : Ch02.BlockPosDef A) (α β : BlockCoord d) : |blockMatEntry A α β| ≤ matNorm A.upperLeft + matNorm A.lowerRight