High-contrast homogenization: Provider.Transport.BridgeAlgebra

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

The algebra of the bridge congruence

p.two.grid.transport compares the terminal annealed block of the old grid with the terminal annealed block of the new one through the near isometry (1 - η_x)H ≤ F ≤ (1 + η_x)H, and reads that comparison through the congruence S = H^{1/2}F^{-1/2}. Two displays record what the comparison says about S: the normalization bounds e.two.grid.inverse.comparison and the determinant bounds e.two.grid.determinant.

Both are proved here, in the generality in which the transport proof uses them: H and F are arbitrary positive definite doubled blocks. The first step is the identity S^tS = F^{-1/2}HF^{-1/2}, which says that the Gram matrix of the bridge is the normalization of the old terminal block by the new one; after that, the first display is the comparison conjugated by F^{-1/2}, and the second is the comparison with determinants taken.

The determinant display carries the only arithmetic in the paragraph. The matrices have size 2d while the determinant root uses the d-th root, so a scalar dilation by c multiplies the determinant by c^{2d} and the root by c^2; that is where the squares in (1 - η_x)^2 and (1 + η_x)^2 come from.

The Gram matrix of the bridge is a normalization

theorem HCPolySupport.HighContrast.Transport.toFullBlockMat_bridgeGram {d : ℕ} {H F : BlockMat d} (hH : Matrix.PosSemidef (toFullBlockMat H)) (hF : Matrix.PosDef (toFullBlockMat F)) : toFullBlockMat (bridgeGram H F) = matSqrt (toFullBlockMat F)⁻¹ * toFullBlockMat H * matSqrt (toFullBlockMat F)⁻¹

The flattened Gram matrix of the bridge congruence is the literal congruence F^{-1/2}HF^{-1/2}: the two inner square roots of H multiply to H, and both square roots are symmetric.

theorem HCPolySupport.HighContrast.Transport.posDef_toFullBlockMat_bridgeGram {d : ℕ} {H F : BlockMat d} (hH : Matrix.PosDef (toFullBlockMat H)) (hF : Matrix.PosDef (toFullBlockMat F)) : Matrix.PosDef (toFullBlockMat (bridgeGram H F))

The Gram matrix of a bridge between positive definite blocks is positive definite.

theorem HCPolySupport.HighContrast.Transport.isSymmetricBlockMat_bridgeGram {d : ℕ} {H F : BlockMat d} (hH : Matrix.PosDef (toFullBlockMat H)) (hF : Matrix.PosDef (toFullBlockMat F)) : IsSymmetricBlockMat (bridgeGram H F)

The Gram matrix of a bridge between positive definite blocks is symmetric.

The normalization display

theorem HCPolySupport.HighContrast.Transport.bridge_normalization {d : ℕ} {H F : BlockMat d} (hH : Matrix.PosDef (toFullBlockMat H)) (hF : Matrix.PosDef (toFullBlockMat F)) {etaX : ℝ} (hetaX : 0 ≤ etaX) (hetaX4 : etaX ≤ 1 / 4) (hlo : BlockMatLoewnerLE (blockScale (1 - etaX) H) F) (hhi : BlockMatLoewnerLE F (blockScale (1 + etaX) H)) : BlockMatLoewnerLE (blockScale (1 + etaX)⁻¹ (Book.Ch02.blockIdentity d)) (bridgeGram H F) ∧ BlockMatLoewnerLE (bridgeGram H F) (blockScale (1 - etaX)⁻¹ (Book.Ch02.blockIdentity d)) ∧ BlockMatLoewnerLE (blockScale (1 - etaX / (1 - etaX)) (Book.Ch02.blockIdentity d)) (bridgeGram H F) ∧ BlockMatLoewnerLE (bridgeGram H F) (blockScale (1 + etaX / (1 - etaX)) (Book.Ch02.blockIdentity d))

The bridge normalization display (e.two.grid.inverse.comparison). For a near isometry (1 - η_x)H ≤ F ≤ (1 + η_x)H with 0 ≤ η_x ≤ 1/4, the Gram matrix of the bridge congruence S = H^{1/2}F^{-1/2} satisfies both printed pairs of bounds: the first pair is the comparison conjugated by F^{-1/2}, and the second follows from it, the upper bound being an identity of scalars and the lower one the inequality 2η_x^2 ≥ 0.

The determinant display

theorem HCPolySupport.HighContrast.Transport.bridge_determinant {d : ℕ} {H F : BlockMat d} (hd : d ≠ 0) (hH : Matrix.PosDef (toFullBlockMat H)) (hF : Matrix.PosDef (toFullBlockMat F)) {etaX : ℝ} (hetaX : 0 ≤ etaX) (hetaX4 : etaX ≤ 1 / 4) (hlo : BlockMatLoewnerLE (blockScale (1 - etaX) H) F) (hhi : BlockMatLoewnerLE F (blockScale (1 + etaX) H)) : (1 - etaX) ^ 2 * detRoot d H ≤ detRoot d F ∧ detRoot d F ≤ (1 + etaX) ^ 2 * detRoot d H

The bridge determinant display (e.two.grid.determinant). Taking determinants in the near isometry (1 - η_x)H ≤ F ≤ (1 + η_x)H and recalling that the blocks have size 2d while the determinant root uses the d-th root gives the two printed bounds, with the bridge error squared.