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

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

Proved annealed subadditivity reductions

This file replaces the old abstract Annealed*Theory packages with plain proved theorems. The pointwise deterministic/a.e. subadditivity hypotheses and integrability hypotheses remain explicit; Ch4 owns the expectation, stationarity, matrix-order, and scalarization consequences.

theorem HCPolySupport.Book.Ch04.matLoewnerLE_of_integral_quadratic_mono {d : ℕ} {P : RestrictionCoeffLaw d} {A B : Mat d} {F G : Vec d → RegCoeffField d → ℝ} (hFint : ∀ (x : Vec d), MeasureTheory.Integrable (F x) P) (hGint : ∀ (x : Vec d), MeasureTheory.Integrable (G x) P) (hA : ∀ (x : Vec d), 1 / 2 * vecDot x (matVecMul A x) = ∫ (a : RegCoeffField d), F x a ∂P) (hB : ∀ (x : Vec d), ∫ (a : RegCoeffField d), G x a ∂P = 1 / 2 * vecDot x (matVecMul B x)) (hMono : ∀ (x : Vec d), F x ≤ᵐ[P] G x) : MatLoewnerLE A B

Integrating an a.e. quadratic-form comparison gives a matrix Löwner comparison.

theorem HCPolySupport.Book.Ch04.blockMatLoewnerLE_of_integral_quadratic_mono {d : ℕ} {P : RestrictionCoeffLaw d} {A B : BlockMat d} {F G : BlockVec d → RegCoeffField d → ℝ} (hFint : ∀ (X : BlockVec d), MeasureTheory.Integrable (F X) P) (hGint : ∀ (X : BlockVec d), MeasureTheory.Integrable (G X) P) (hA : ∀ (X : BlockVec d), 1 / 2 * blockVecDot X (blockMatVecMul A X) = ∫ (a : RegCoeffField d), F X a ∂P) (hB : ∀ (X : BlockVec d), ∫ (a : RegCoeffField d), G X a ∂P = 1 / 2 * blockVecDot X (blockMatVecMul B X)) (hMono : ∀ (X : BlockVec d), F X ≤ᵐ[P] G X) : BlockMatLoewnerLE A B

Integrating an a.e. doubled quadratic-form comparison gives a block-matrix Löwner comparison.

theorem HCPolySupport.Book.Ch04.blockMatLoewnerLE_upperLeft_apply {d : ℕ} {A B : BlockMat d} (h : BlockMatLoewnerLE A B) (i : Fin d) : A.upperLeft i i ≤ B.upperLeft i i

A block Löwner comparison controls diagonal entries of the upper-left block.

theorem HCPolySupport.Book.Ch04.blockMatLoewnerLE_lowerRight_apply {d : ℕ} {A B : BlockMat d} (h : BlockMatLoewnerLE A B) (i : Fin d) : A.lowerRight i i ≤ B.lowerRight i i

A block Löwner comparison controls diagonal entries of the lower-right block.

theorem HCPolySupport.Book.Ch04.integrable_blockVecDot_blockMatVecMul_of_integrable_entries {d : ℕ} {P : RestrictionCoeffLaw d} {B : RegCoeffField d → BlockMat d} (hB : ∀ (α β : BlockCoord d), MeasureTheory.Integrable (fun (a : RegCoeffField d) => blockMatEntry (B a) α β) P) (X Y : BlockVec d) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => blockVecDot X (blockMatVecMul (B a) Y)) P

Finite-dimensional block quadratic forms are integrable when all block entries are integrable.

theorem HCPolySupport.Book.Ch04.integral_blockVecDot_blockMatVecMul_eq_of_integrable_entries {d : ℕ} {P : RestrictionCoeffLaw d} {B : RegCoeffField d → BlockMat d} (hB : ∀ (α β : BlockCoord d), MeasureTheory.Integrable (fun (a : RegCoeffField d) => blockMatEntry (B a) α β) P) (X Y : BlockVec d) : ∫ (a : RegCoeffField d), blockVecDot X (blockMatVecMul (B a) Y) ∂P = blockVecDot X (blockMatVecMul { upperLeft := fun (i j : Fin d) => ∫ (a : RegCoeffField d), (B a).upperLeft i j ∂P, upperRight := fun (i j : Fin d) => ∫ (a : RegCoeffField d), (B a).upperRight i j ∂P, lowerLeft := fun (i j : Fin d) => ∫ (a : RegCoeffField d), (B a).lowerLeft i j ∂P, lowerRight := fun (i j : Fin d) => ∫ (a : RegCoeffField d), (B a).lowerRight i j ∂P } Y)

Finite-dimensional block quadratic forms commute with entrywise expectation under entrywise integrability.

theorem HCPolySupport.Book.Ch04.blockMatLoewnerLE_blockReflect {d : ℕ} {A B : BlockMat d} (h : BlockMatLoewnerLE A B) : BlockMatLoewnerLE (blockReflect A) (blockReflect B)

Reflection of doubled variables preserves block Löwner comparisons.

theorem HCPolySupport.Book.Ch04.matLoewnerLE_lowerRight_of_blockMatLoewnerLE {d : ℕ} {A B : BlockMat d} (h : BlockMatLoewnerLE A B) : MatLoewnerLE A.lowerRight B.lowerRight

The lower-right block of a block Löwner comparison is a matrix Löwner comparison.

theorem HCPolySupport.Book.Ch04.matLoewnerLE_upperLeft_of_blockMatLoewnerLE {d : ℕ} {A B : BlockMat d} (h : BlockMatLoewnerLE A B) : MatLoewnerLE A.upperLeft B.upperLeft

The upper-left block of a block Löwner comparison is a matrix Löwner comparison.

theorem HCPolySupport.Book.Ch04.restrictionResponseJ_le_descendantAverage {d : ℕ} [NeZero d] {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) {n m : ℤ} (hnm : n ≤ m) (p q : Vec d) : restrictionResponseJObservableCubeSet (originCube d m) p q a ≤ descendantsAverage (originCube d m) (m - n).toNat fun (R : TriadicCube d) => restrictionResponseJObservableCubeSet R p q a

Pointwise response subadditivity for the Ch4 scalar response observable, with the a.e. coefficient representative handled by the Chapter 2 coefficient family.

theorem HCPolySupport.Book.Ch04.responseJObservableSet_le_descendantMean_cube_of_locallyEllipticField {d : ℕ} [NeZero d] {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (p q : Vec d) : restrictionResponseJObservableCubeSet Q p q a ≤ descendantsAverage Q (Q.scale - k).toNat fun (R : TriadicCube d) => restrictionResponseJObservableCubeSet R p q a

Pointwise response subadditivity on an arbitrary triadic cube for the Ch4 scalar response observable, with the a.e. coefficient representative handled by the Chapter 2 coefficient family.

theorem HCPolySupport.Book.Ch04.coarseBlockMatrix_le_descendantAverage {d : ℕ} [NeZero d] {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) : BlockMatLoewnerLE (coarseBlockMatrix (cubeSet Q) a.toFun) (descendantsAverageBlockMat Q (Q.scale - k).toNat fun (R : TriadicCube d) => coarseBlockMatrix (cubeSet R) a.toFun)

Pointwise block coarse-matrix subadditivity on an arbitrary triadic cube for a locally a.e.-elliptic coefficient field, with the a.e. representative handled by the Chapter 2 coefficient family.

theorem HCPolySupport.Book.Ch04.coarseBlockMatrix_le_descendantsAverageBlockMat_of_aelocallyUniformlyEllipticField {d : ℕ} [NeZero d] {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) {n m : ℤ} (hnm : n ≤ m) : BlockMatLoewnerLE (coarseBlockMatrix (cubeSet (originCube d m)) a.toFun) (descendantsAverageBlockMat (originCube d m) (m - n).toNat fun (R : TriadicCube d) => coarseBlockMatrix (cubeSet R) a.toFun)

Pointwise block coarse-matrix subadditivity for a locally a.e.-elliptic coefficient field, with the a.e. representative handled by the Chapter 2 coefficient family.