High-contrast homogenization: Entry.Analysis.BlockSwapReflection

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The block swap, the skew shear and the Schur factorization

The deterministic block algebra the reference-block comparison of HCPoly/Entry/Analysis/ReferenceComparison.lean runs on; the source argument is Lemma l.bfE.bounds of the companion paper HC, near e.reference.aspect.ratio.

• The swap involution blockSwap d is symmetric and squares to the identity on the full 2d carrier, and conjugation by it is the block reflection. Conjugating the inverse of a positive definite block therefore leaves it positive definite, sends the lower-right corner to (schurSigma E)⁻¹, and inverts the determinant.
• The skew shear blockG h is invertible with inverse blockG (-h); congruence by it carries a symmetric block with positive definite quadratic form to the skew-corrected form in the upper-left corner, preserves positive definiteness, and commutes with the swap conjugation of the inverse up to the shear of the negated skew part.
• The Schur factorization of a symmetric positive definite block along schurSkew E, with the positive definiteness of schurSigma E.

Two order dictionaries are proved with them: toFullBlockMat A ≤ toFullBlockMat B is BlockMatLoewnerLE A B on Hermitian carriers, and A ≤ B is MatLoewnerLE A B on Hermitian matrices. No probability law, quantitative ellipticity constant or annealed premise enters.

theorem HCPolySupport.HighContrast.Analysis.isHermitian_smul {ι : Type u_1} {M : Matrix ι ι ℝ} (hM : M.IsHermitian) (c : ℝ) : (c • M).IsHermitian

A real scalar multiple of a Hermitian matrix is Hermitian.

theorem HCPolySupport.HighContrast.Analysis.posDef_toFullBlockMat_of_blockPosDef {d : ℕ} {E : BlockMat d} (hs : IsSymmetricBlockMat E) (hp : Book.Ch02.BlockPosDef E) : Matrix.PosDef (toFullBlockMat E)

A symmetric block whose block quadratic form is positive definite is positive definite on the full 2d carrier.

theorem HCPolySupport.HighContrast.Analysis.toFullBlockMat_le_iff {d : ℕ} {A B : BlockMat d} (hA : Matrix.IsHermitian (toFullBlockMat A)) (hB : Matrix.IsHermitian (toFullBlockMat B)) : toFullBlockMat A ≤ toFullBlockMat B ↔ BlockMatLoewnerLE A B

On Hermitian full carriers the matrix order is the block Loewner order.

theorem HCPolySupport.HighContrast.Analysis.inv_le_inv_of_posDef_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A B : Matrix ι ι ℝ} (hA : A.PosDef) (hB : B.PosDef) (hle : A ≤ B) : B⁻¹ ≤ A⁻¹

Inversion is antitone on positive definite matrices.

theorem HCPolySupport.HighContrast.Analysis.isSymmetricBlockMat_blockSwap (d : ℕ) : IsSymmetricBlockMat (blockSwap d)

The reflection block is symmetric.

theorem HCPolySupport.HighContrast.Analysis.toFullBlockMat_blockSwap_mul_self (d : ℕ) : toFullBlockMat (blockSwap d) * toFullBlockMat (blockSwap d) = 1

The reflection block is an involution.

theorem HCPolySupport.HighContrast.Analysis.swapConj_eq_blockReflect {d : ℕ} (F : BlockMat d) : ofFullBlockMat (toFullBlockMat (blockSwap d) * toFullBlockMat F * toFullBlockMat (blockSwap d)) = blockReflect F

Literal reflection products agree with the CG block reflection.

theorem HCPolySupport.HighContrast.Analysis.swapConj_inv_eq_blockReflect {d : ℕ} (F : BlockMat d) : ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat F)⁻¹ * toFullBlockMat (blockSwap d)) = blockReflect (ofFullBlockMat (toFullBlockMat F)⁻¹)

The inverse instance of the reflection identity.

theorem HCPolySupport.HighContrast.Analysis.blockSwap_conj_fromBlocks {d : ℕ} (A B C D : Mat d) : toFullBlockMat (blockSwap d) * Matrix.fromBlocks A B C D * toFullBlockMat (blockSwap d) = Matrix.fromBlocks D C B A

Conjugation by the swap exchanges the two diagonal corners of a fromBlocks matrix and the two off-diagonal corners.

theorem HCPolySupport.HighContrast.Analysis.isHermitian_toFullBlockMat_blockSwap (d : ℕ) : Matrix.IsHermitian (toFullBlockMat (blockSwap d))

The swap involution is Hermitian on the full 2d carrier.

theorem HCPolySupport.HighContrast.Analysis.swapConj_posDef {d : ℕ} {F : BlockMat d} (hp : Matrix.PosDef (toFullBlockMat F)) : Matrix.PosDef (toFullBlockMat (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat F)⁻¹ * toFullBlockMat (blockSwap d))))

The adjoint reference block is positive definite in the full matrix carrier.

theorem HCPolySupport.HighContrast.Analysis.isUnit_toFullBlockMat_blockG {d : ℕ} (h : Mat d) : IsUnit (toFullBlockMat (Book.Ch02.blockG h))

The skew shear is invertible on the full 2d carrier.

theorem HCPolySupport.HighContrast.Analysis.blockG_conj_swapConj_eq {d : ℕ} (E : BlockMat d) (h : Mat d) (hh : IsSkewMat h) : Matrix.conjTranspose (toFullBlockMat (Book.Ch02.blockG h)) * (toFullBlockMat (blockSwap d) * (toFullBlockMat E)⁻¹ * toFullBlockMat (blockSwap d)) * toFullBlockMat (Book.Ch02.blockG h) = toFullBlockMat (blockSwap d) * (Matrix.conjTranspose (toFullBlockMat (Book.Ch02.blockG h)) * toFullBlockMat E * toFullBlockMat (Book.Ch02.blockG h))⁻¹ * toFullBlockMat (blockSwap d)

The skew shear commutes with the swap conjugation of the inverse, up to the shear of the negated skew part.

theorem HCPolySupport.HighContrast.Analysis.blockG_conj_eq_fromBlocks {d : ℕ} {E : BlockMat d} (hs : IsSymmetricBlockMat E) (hp : Book.Ch02.BlockPosDef E) (h : Mat d) : Matrix.conjTranspose (toFullBlockMat (Book.Ch02.blockG h)) * toFullBlockMat E * toFullBlockMat (Book.Ch02.blockG h) = Matrix.fromBlocks (skewCorrectedForm E h) (E.upperRight + Matrix.conjTranspose h * E.lowerRight) (E.lowerLeft + E.lowerRight * h) E.lowerRight

Congruence by the skew shear blockG h puts the skew-corrected form in the upper-left corner.

theorem HCPolySupport.HighContrast.Analysis.posDef_blockG_conj {d : ℕ} {E : BlockMat d} (hs : IsSymmetricBlockMat E) (hp : Book.Ch02.BlockPosDef E) (h : Mat d) : (Matrix.conjTranspose (toFullBlockMat (Book.Ch02.blockG h)) * toFullBlockMat E * toFullBlockMat (Book.Ch02.blockG h)).PosDef

Congruence by the skew shear preserves positive definiteness.

theorem HCPolySupport.HighContrast.Analysis.matrix_le_iff_matLoewnerLE {d : ℕ} {A B : Mat d} (hA : Matrix.IsHermitian A) (hB : Matrix.IsHermitian B) : A ≤ B ↔ MatLoewnerLE A B

On Hermitian matrices the matrix order is the Loewner order read on quadratic forms.

theorem HCPolySupport.HighContrast.Analysis.posDef_skewCorrectedForm {d : ℕ} {E : BlockMat d} (hs : IsSymmetricBlockMat E) (hp : Book.Ch02.BlockPosDef E) (h : Mat d) : Matrix.PosDef (skewCorrectedForm E h)

The skew-corrected form of a symmetric positive definite block is positive definite.

theorem HCPolySupport.HighContrast.Analysis.posDef_schurSigma {d : ℕ} {E : BlockMat d} (hs : IsSymmetricBlockMat E) (hp : Book.Ch02.BlockPosDef E) : Matrix.PosDef (schurSigma E)

The Schur complement schurSigma E of a symmetric positive definite block is positive definite.

theorem HCPolySupport.HighContrast.Analysis.swapConj_lowerRight {d : ℕ} {E : BlockMat d} (hs : IsSymmetricBlockMat E) (hp : Book.Ch02.BlockPosDef E) : (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat E)⁻¹ * toFullBlockMat (blockSwap d))).lowerRight = (schurSigma E)⁻¹

The lower-right block of the swap-conjugated inverse is the inverse Schur complement (schurSigma E)⁻¹. This is the Schur factorization read off the reflected inverse.

theorem HCPolySupport.HighContrast.Analysis.det_swapConj {d : ℕ} (E : BlockMat d) : Matrix.det (toFullBlockMat (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat E)⁻¹ * toFullBlockMat (blockSwap d)))) = (Matrix.det (toFullBlockMat E))⁻¹

Reflection preserves the inverse determinant; no normalized determinant convention is used.