High-contrast homogenization: Entry.Multiscale.Global.GeoMeanBlocks

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

Block plumbing and the projective-distance sandwich

Block-matrix plumbing for the Loewner order (matLE_iff, le_of_blockMatLoewnerLE, toFullBlockMat_blockScale, the lowerRight transfer lemmas), the projective-distance sandwich projectiveDistance_le_of_sandwich, and the identification of the canonical metric with a matrix geometric mean. These are the helpers the public toolkit HCPoly.Entry.Multiscale.Initial.GeometricMean (namespace GeometricMean) does not itself carry; the square-root order and geometric-mean facts are taken from there. They supply the block-order and matrix-geometric-mean part of the canonical-metric comparison in the finite run of p.global.selection, bounding the projective distance between two canonical metrics by half the logarithm of the Loewner sandwich ratio.

Part 2. Block plumbing

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

theorem HCPolySupport.HighContrast.Multiscale.BlockGeometricMean.symm_blockScale {d : ℕ} {c : ℝ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) : IsSymmetricBlockMat (blockScale c E)

theorem HCPolySupport.HighContrast.Multiscale.BlockGeometricMean.lowerRight_ofFull {d : ℕ} (M : FullBlockMat d) : (ofFullBlockMat M).lowerRight = Matrix.submatrix M Sum.inr Sum.inr

theorem HCPolySupport.HighContrast.Multiscale.BlockGeometricMean.lowerRightMono {d : ℕ} {M N : FullBlockMat d} (h : M ≤ N) : (ofFullBlockMat M).lowerRight ≤ (ofFullBlockMat N).lowerRight

theorem HCPolySupport.HighContrast.Multiscale.BlockGeometricMean.lowerRight_smul {d : ℕ} (a : ℝ) (M : FullBlockMat d) : (ofFullBlockMat (a • M)).lowerRight = a • (ofFullBlockMat M).lowerRight

Part 3. The projective-distance sandwich

theorem HCPolySupport.HighContrast.Multiscale.BlockGeometricMean.projectiveDistance_le_of_sandwich {d : ℕ} [NeZero d] {m₀ m₁ : Mat d} (h₀ : Matrix.PosDef m₀) (h₁ : Matrix.PosDef m₁) {a b : ℝ} (ha : 0 < a) (hlo : MatLoewnerLE (a • m₀) m₁) (hhi : MatLoewnerLE m₁ (b • m₀)) : projectiveDistance m₀ m₁ ≤ 1 / 2 * Real.log (b / a)

Part 4. The canonical metric as a geometric mean

theorem HCPolySupport.HighContrast.Multiscale.BlockGeometricMean.explicitCanonicalMetric_eq_geoMean {d : ℕ} (F : BlockMat d) : explicitCanonicalMetric F = (ofFullBlockMat (GeometricMean.geoMean (toFullBlockMat F) (toFullBlockMat (blockSwap d) * (toFullBlockMat F)⁻¹ * toFullBlockMat (blockSwap d)))).lowerRight⁻¹

theorem HCPolySupport.HighContrast.Multiscale.BlockGeometricMean.lowerRightPosDef {d : ℕ} {M : FullBlockMat d} (hM : Matrix.PosDef M) : Matrix.PosDef (ofFullBlockMat M).lowerRight

theorem HCPolySupport.HighContrast.Multiscale.BlockGeometricMean.swapFullHerm (d : ℕ) : Matrix.conjTranspose (toFullBlockMat (blockSwap d)) = toFullBlockMat (blockSwap d)

theorem HCPolySupport.HighContrast.Multiscale.BlockGeometricMean.sandwich {d : ℕ} [NeZero d] (F G : BlockMat d) (hF : IsSymmetricBlockMat F) (hFpos : Book.Ch02.BlockPosDef F) (hG : IsSymmetricBlockMat G) (hGpos : Book.Ch02.BlockPosDef G) (c κ : ℝ) (hc : 0 < c) (hκ : 1 ≤ κ) (hlo : BlockMatLoewnerLE (blockScale c G) F) (hhi : BlockMatLoewnerLE F (blockScale (κ * c) G)) : projectiveDistance (explicitCanonicalMetric F) (explicitCanonicalMetric G) ≤ 1 / 2 * Real.log κ

theorem HCPolySupport.HighContrast.Multiscale.BlockGeometricMean.explicitCanonicalMetric_projectiveDistance_le_logDet_aux_scale_one_le {d : ℕ} (G F : BlockMat d) (hGs : IsSymmetricBlockMat G) (hG : Book.Ch02.BlockPosDef G) (hFs : IsSymmetricBlockMat F) (hF : Book.Ch02.BlockPosDef F) (hGF : BlockMatLoewnerLE G F) : BlockMatLoewnerLE (blockScale 1 G) F

Block-plumbing step for explicitCanonicalMetric_projectiveDistance_le_logDet: unit scaling of a symmetric positive block preserves a Loewner bound above another such block.

theorem HCPolySupport.HighContrast.Multiscale.BlockGeometricMean.explicitCanonicalMetric_projectiveDistance_le_logDet_aux_upper {d : ℕ} (F G : BlockMat d) (hFs : IsSymmetricBlockMat F) (hF : Book.Ch02.BlockPosDef F) (hGs : IsSymmetricBlockMat G) (hG : Book.Ch02.BlockPosDef G) (hGF : BlockMatLoewnerLE G F) : BlockMatLoewnerLE F (blockScale (Real.exp (blockLogDet F - blockLogDet G)) G) ∧ 0 ≤ blockLogDet F - blockLogDet G

Projective-distance-sandwich step for explicitCanonicalMetric_projectiveDistance_le_logDet: for symmetric positive blocks G ≤ F, F is Loewner-below exp(logDet F − logDet G) • G, and the exponent is nonnegative.