High-contrast homogenization: Entry.Geometry.CanonicalMetricBounds

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

Positivity of the canonical metric

This proves positive definiteness of the closed printed definition of explicitCanonicalMetric; it does not introduce a geometric-mean characterization or the metric-loss estimate, which belong to the global selection. The positivity of the canonical metric, and its specialization to the rounded adapted means, underlies the projective-distance geometry serving p.global.selection and p.scale.selection.

theorem HCPolySupport.HighContrast.Geometry.swapConj_inv_posDef {d : ℕ} {F : BlockMat d} (hsymm : IsSymmetricBlockMat F) (hpos : Book.Ch02.BlockPosDef F) : (toFullBlockMat (blockSwap d) * (toFullBlockMat F)⁻¹ * toFullBlockMat (blockSwap d)).PosDef

The reflected inverse 𝐑F⁻¹𝐑 is positive definite for a positive block F.

theorem HCPolySupport.HighContrast.Geometry.explicitCanonicalMetric_inner_posDef {d : ℕ} {F : BlockMat d} (hsymm : IsSymmetricBlockMat F) (hpos : Book.Ch02.BlockPosDef F) : (matSqrt (toFullBlockMat F)⁻¹ * toFullBlockMat (blockSwap d) * (toFullBlockMat F)⁻¹ * toFullBlockMat (blockSwap d) * matSqrt (toFullBlockMat F)⁻¹).PosDef

The inner square-root argument in explicitCanonicalMetric is positive definite.

theorem HCPolySupport.HighContrast.Geometry.explicitCanonicalMetric_middleSqrt_posDef {d : ℕ} {F : BlockMat d} (hsymm : IsSymmetricBlockMat F) (hpos : Book.Ch02.BlockPosDef F) : (matSqrt (matSqrt (toFullBlockMat F)⁻¹ * toFullBlockMat (blockSwap d) * (toFullBlockMat F)⁻¹ * toFullBlockMat (blockSwap d) * matSqrt (toFullBlockMat F)⁻¹)).PosDef

The middle square root in explicitCanonicalMetric is positive definite.

theorem HCPolySupport.HighContrast.Geometry.explicitCanonicalMetric_outer_posDef {d : ℕ} {F : BlockMat d} (hsymm : IsSymmetricBlockMat F) (hpos : Book.Ch02.BlockPosDef F) : (matSqrt (toFullBlockMat F) * matSqrt (matSqrt (toFullBlockMat F)⁻¹ * toFullBlockMat (blockSwap d) * (toFullBlockMat F)⁻¹ * toFullBlockMat (blockSwap d) * matSqrt (toFullBlockMat F)⁻¹) * matSqrt (toFullBlockMat F)).PosDef

The full matrix before taking the lower-right block in explicitCanonicalMetric is positive definite.

theorem HCPolySupport.HighContrast.Geometry.explicitCanonicalMetric_lowerRight_posDef {d : ℕ} {F : BlockMat d} (hsymm : IsSymmetricBlockMat F) (hpos : Book.Ch02.BlockPosDef F) : Matrix.PosDef (ofFullBlockMat (matSqrt (toFullBlockMat F) * matSqrt (matSqrt (toFullBlockMat F)⁻¹ * toFullBlockMat (blockSwap d) * (toFullBlockMat F)⁻¹ * toFullBlockMat (blockSwap d) * matSqrt (toFullBlockMat F)⁻¹) * matSqrt (toFullBlockMat F))).lowerRight

The lower-right block before the final inverse in explicitCanonicalMetric is positive definite.

theorem HCPolySupport.HighContrast.Geometry.explicitCanonicalMetric_posDef {d : ℕ} {F : BlockMat d} (hsymm : IsSymmetricBlockMat F) (hpos : Book.Ch02.BlockPosDef F) : Matrix.PosDef (explicitCanonicalMetric F)

O4. The closed printed canonical metric is positive definite on symmetric positive doubled blocks.

The unconditional dichotomy

Everything above carries the printed hypotheses hsymm/hpos. The block below carries none. matSqrt takes the junk value 1 -- not 0 -- off the positive semidefinite data (HCPoly/Setup/BlockAlgebra.lean, matSqrt), so every factor of the closed expression defining explicitCanonicalMetric is positive semidefinite whatever F is; a congruence, a principal submatrix and Mathlib's Matrix.inv (which is 0 off the units) all preserve that. Hence explicitCanonicalMetric F is positive semidefinite for every F, so it is either positive definite or singular, and in the singular case the rounded grid built from it collapses to the zero matrix. That dichotomy is what lets the response cutoff kernel dispose of the degenerate branch without adding a hypothesis to its statement.

theorem HCPolySupport.HighContrast.matSqrt_posSemidef {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : Matrix ι ι ℝ) : (matSqrt M).PosSemidef

matSqrt is positive semidefinite on every input: on positive semidefinite data it is the canonical square root, and off that data it is the junk value 1. Stated in the project's root namespace, beside matSqrt itself.

theorem HCPolySupport.HighContrast.Geometry.explicitCanonicalMetric_posSemidef {d : ℕ} (F : BlockMat d) : Matrix.PosSemidef (explicitCanonicalMetric F)

The positive semidefinite link. The canonical metric is positive semidefinite for every doubled block, with no symmetry and no positivity hypothesis: the junk values of matSqrt and of Matrix.inv are themselves positive semidefinite.

theorem HCPolySupport.HighContrast.Geometry.explicitCanonicalMetric_posDef_or_inv_eq_zero {d : ℕ} (F : BlockMat d) : Matrix.PosDef (explicitCanonicalMetric F) ∨ (explicitCanonicalMetric F)⁻¹ = 0

A positive semidefinite matrix is positive definite exactly when it is a unit, so the canonical metric is either positive definite or has vanishing inverse. No hypothesis.

theorem HCPolySupport.HighContrast.Geometry.explicitRoundedGrid_eq_zero_of_inv_eq_zero {d : ℕ} (jStar : ℕ) {m : Mat d} (hm : m⁻¹ = 0) : explicitRoundedGrid jStar m = 0

Every entry of 𝒬(𝔪) carries the factor |𝔪⁻¹|^{1/2}, so the rounded grid of a matrix with vanishing inverse is the zero matrix.

theorem HCPolySupport.HighContrast.Geometry.det_roundedGrid_eq_zero_of_inv_eq_zero {d : ℕ} [NeZero d] (jStar : ℕ) {m : Mat d} (hm : m⁻¹ = 0) : Matrix.det (explicitRoundedGrid jStar m) = 0

The determinant of the rounded grid of a matrix with vanishing inverse is zero.

theorem HCPolySupport.HighContrast.Geometry.explicitCanonicalMetric_posDef_or_det_roundedGrid_eq_zero {d : ℕ} [NeZero d] (jStar : ℕ) (F : BlockMat d) : Matrix.PosDef (explicitCanonicalMetric F) ∨ Matrix.det (explicitRoundedGrid jStar (explicitCanonicalMetric F)) = 0

The metric dichotomy. For every doubled block F -- no symmetry, no positivity -- either the canonical metric m(F) is positive definite, or the rounded grid 𝒬(m(F)) built from it is singular.

theorem HCPolySupport.HighContrast.Geometry.explicitCanonicalMetric_adaptedMean_posDef (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (j : ℤ) : Matrix.PosDef (explicitCanonicalMetric (adaptedMean P (explicitRoundedGrid jStar m) j))

O4 at the rounded adapted means used by scale selection.