Coarse-graining support: Support.CoarseGraining.SharpBlockBounds.DiagonalSandwich

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

Diagonal sandwich (A8 lower) and two-field comparison (A9)

The lower half of the diagonal sandwich A8 and the two-field comparison A9 of Proposition 2.1 of the high-moment paper (Armstrong–Kuusi–Loher, in preparation). These require the block Fenchel duality: bfA is symmetric, positive definite, and its inverse is the block reflection blockReflect bfA. We establish that inverse identity by an explicit block-matrix computation and feed it through a pointwise Young/Fenchel inequality.

Continuation of SharpBlockBounds/Basic.lean.

Block composition and the reflection inverse

theorem HCPolySupport.blockMatVecMul_blockMatMul {d : ℕ} (A B : BlockMat d) (X : BlockVec d) : blockMatVecMul (Book.Ch02.blockMatMul A B) X = blockMatVecMul A (blockMatVecMul B X)

blockMatMul composes with the doubled action.

theorem HCPolySupport.blockMatVecMul_blockIdentity {d : ℕ} (X : BlockVec d) : blockMatVecMul (Book.Ch02.blockIdentity d) X = X

The doubled block identity acts trivially.

theorem HCPolySupport.blockMatMul_blockReflect_blockMatrixOfCoeff_eq_id {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) : Book.Ch02.blockMatMul (blockMatrixOfCoeff A) (blockReflect (blockMatrixOfCoeff A)) = Book.Ch02.blockIdentity d

The block reflection is a right inverse of bfA at the matrix level.

theorem HCPolySupport.blockMatVecMul_blockReflect_inv {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (Y : BlockVec d) : blockMatVecMul (blockMatrixOfCoeff A) (blockMatVecMul (blockReflect (blockMatrixOfCoeff A)) Y) = Y

The reflection is a right inverse of bfA at the level of the doubled action.

Positive semidefiniteness and the block Fenchel inequality

theorem HCPolySupport.blockMatrixOfCoeff_quadratic_nonneg {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (Z : BlockVec d) : 0 ≤ blockVecDot Z (blockMatVecMul (blockMatrixOfCoeff A) Z)

bfA is positive semidefinite.

theorem HCPolySupport.block_fenchel {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (X Y : BlockVec d) : 2 * blockVecDot X Y - blockVecDot Y (blockMatVecMul (blockReflect (blockMatrixOfCoeff A)) Y) ≤ blockVecDot X (blockMatVecMul (blockMatrixOfCoeff A) X)

Block Fenchel/Young inequality. For the symmetric p.s.d. bfA with inverse blockReflect bfA: 2 X·Y − Y·(reflect bfA)Y ≤ X·(bfA)X.

A8 (lower) — diagonal sandwich, lower half

theorem HCPolySupport.blockMatVecMul_blockDiag_smul_one {d : ℕ} (a b : ℝ) (p q : Vec d) : blockMatVecMul (Book.Ch02.blockDiag (a • 1) (b • 1)) (p, q) = (a • p, b • q)

A block-diagonal matrix with scalar-multiple-of-identity blocks acts by scaling each block.

theorem HCPolySupport.blockDiag_blockMatLoewnerLE_blockMatrixOfCoeff_of_isThetaElliptic {d : ℕ} {Θ : ℝ} {A : Mat d} (hA : IsThetaElliptic Θ A) : BlockMatLoewnerLE (Book.Ch02.blockDiag ((1 / 2) • 1) ((2 * Θ)⁻¹ • 1)) (blockMatrixOfCoeff A)

A8 (lower). blockDiag (½ • 1) ((2Θ)⁻¹ • 1) ≤ bfA in the block Loewner order.

A9 — two-field comparison

The verified scalar action on BlockMat d (componentwise), and the comparison bfB ≤ 4Θ • bfA for two matrices in the same (1, Θ) ellipticity class.

@[instance_reducible]

instance HCPolySupport.instSMulRealBlockMat {d : ℕ} : SMul ℝ (BlockMat d)

Componentwise scalar action on doubled block matrices.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.blockSMul_upperLeft {d : ℕ} (c : ℝ) (P : BlockMat d) : (c • P).upperLeft = c • P.upperLeft

@[simp]

theorem HCPolySupport.blockSMul_upperRight {d : ℕ} (c : ℝ) (P : BlockMat d) : (c • P).upperRight = c • P.upperRight

@[simp]

theorem HCPolySupport.blockSMul_lowerLeft {d : ℕ} (c : ℝ) (P : BlockMat d) : (c • P).lowerLeft = c • P.lowerLeft

@[simp]

theorem HCPolySupport.blockSMul_lowerRight {d : ℕ} (c : ℝ) (P : BlockMat d) : (c • P).lowerRight = c • P.lowerRight

theorem HCPolySupport.blockMatVecMul_blockSMul {d : ℕ} (c : ℝ) (P : BlockMat d) (X : BlockVec d) : blockMatVecMul (c • P) X = c • blockMatVecMul P X

The scalar action commutes with the doubled action.

theorem HCPolySupport.blockSMul_blockDiag_smul_one {d : ℕ} (c a b : ℝ) : c • Book.Ch02.blockDiag (a • 1) (b • 1) = Book.Ch02.blockDiag ((c * a) • 1) ((c * b) • 1)

blockSMul on block-diagonal scalar matrices.

theorem HCPolySupport.blockMatLoewnerLE_smul {d : ℕ} {c : ℝ} (hc : 0 ≤ c) {P Q : BlockMat d} (h : BlockMatLoewnerLE P Q) : BlockMatLoewnerLE (c • P) (c • Q)

The block Loewner order is preserved by nonnegative scaling.

theorem HCPolySupport.blockMatrixOfCoeff_blockMatLoewnerLE_smul_of_isThetaElliptic {d : ℕ} {Θ : ℝ} {A B : Mat d} (hA : IsThetaElliptic Θ A) (hB : IsThetaElliptic Θ B) : BlockMatLoewnerLE (blockMatrixOfCoeff B) ((4 * Θ) • blockMatrixOfCoeff A)

A9. For A, B in the same (1, Θ) ellipticity class, bfB ≤ (4Θ) • bfA in the block Loewner order.