High-contrast homogenization: Geometry.ProjectiveDistance

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

The projective distance between positive matrices

The reference text defines, for positive m₀, m₁,

d_pr([m₀],[m₁]) = ½ (log λ_max(m₀^{-1/2} m₁ m₀^{-1/2})
                      - log λ_min(m₀^{-1/2} m₁ m₀^{-1/2})),

which is e.scale.selection.projective.distance. Writing X := m₀^{-1/2} m₁ m₀^{-1/2}, which is positive definite, the two eigenvalues are read off by the relative size of HCPoly.Geometry.RelativeSize:

• relSize m₁ m₀ = ‖X‖ = λ_max(X) holds by the definition of relSize;
• relSize m₀ m₁ = ‖X⁻¹‖ = λ_min(X)⁻¹, which is relSize_eq_norm_normalize_inv.

Because log (λ_min(X)) = - log (‖X⁻¹‖), the printed difference of logarithms is the sum used here as the definition:

projDist m₀ m₁ = ½ (log (relSize m₁ m₀) + log (relSize m₀ m₁)).

This encoding never names an eigenvalue and never inverts a matrix, so the symmetry projDist_comm, the scale invariance projDist_smul_left and projDist_smul_right — the invariances that make the bracket notation [m] legitimate — and the triangle inequality all reduce to the least-scalar-bound characterization relSize_le_iff.

The workhorse for the canonical-geometry estimates is projDist_le_of_le: a two-sided Loewner sandwich a m₀ ≤ m₁ ≤ b m₀ bounds the distance by ½ log (b/a). The triangle inequality is exactly that bound applied to the composition of two sandwiches with the sharp constants.

Statements whose truth needs ‖(1 : Matrix n n ℝ)‖ = 1 carry a Nonempty instance on the index type; on an empty index type every relative size vanishes and the definition degenerates.

Logarithm arithmetic

The logarithm is kept opaque: these helpers speak only about abstract positive reals, and no later proof lets a linear-arithmetic step see Real.log applied to a matrix expression.

The distance

noncomputable def HCPolySupport.HighContrast.projDist {n : Type u_1} [Fintype n] [DecidableEq n] (m₀ m₁ : Matrix n n ℝ) : ℝ

The projective distance of e.scale.selection.projective.distance, encoded through the relative sizes of the pair in both directions.

Equations

• HCPolySupport.HighContrast.projDist m₀ m₁ = 1 / 2 * (Real.log (HCPolySupport.HighContrast.relSize m₁ m₀) + Real.log (HCPolySupport.HighContrast.relSize m₀ m₁))

theorem HCPolySupport.HighContrast.projDist_def {n : Type u_1} [Fintype n] [DecidableEq n] (m₀ m₁ : Matrix n n ℝ) : projDist m₀ m₁ = 1 / 2 * (Real.log (relSize m₁ m₀) + Real.log (relSize m₀ m₁))

theorem HCPolySupport.HighContrast.projDist_eq_norm_form {n : Type u_1} [Fintype n] [DecidableEq n] {m₀ m₁ : Matrix n n ℝ} (h₀ : m₀.PosDef) (h₁ : m₁.PosDef) : projDist m₀ m₁ = 1 / 2 * (Real.log ‖matSqrt m₀⁻¹ * m₁ * matSqrt m₀⁻¹‖ + Real.log ‖(matSqrt m₀⁻¹ * m₁ * matSqrt m₀⁻¹)⁻¹‖)

The printed form. With X = m₀^{-1/2} m₁ m₀^{-1/2} the definition is the reference text's difference of the logarithms of the extreme eigenvalues of X: the first term is log ‖X‖ and the second is - log (λ_min X).

theorem HCPolySupport.HighContrast.projDist_comm {n : Type u_1} [Fintype n] [DecidableEq n] (m₀ m₁ : Matrix n n ℝ) : projDist m₀ m₁ = projDist m₁ m₀

The projective distance is symmetric.

theorem HCPolySupport.HighContrast.projDist_self {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {m : Matrix n n ℝ} (hm : m.PosDef) : projDist m m = 0

The projective distance from a positive definite matrix to itself is zero.

theorem HCPolySupport.HighContrast.projDist_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {m₀ m₁ : Matrix n n ℝ} (h₀ : m₀.PosDef) (h₁ : m₁.PosDef) : 0 ≤ projDist m₀ m₁

The projective distance is nonnegative.

Invariances

theorem HCPolySupport.HighContrast.projDist_smul_left {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {c : ℝ} (hc : 0 < c) {m₀ m₁ : Matrix n n ℝ} (h₀ : m₀.PosDef) (h₁ : m₁.PosDef) : projDist (c • m₀) m₁ = projDist m₀ m₁

Scaling the first matrix by a positive scalar leaves the distance unchanged.

theorem HCPolySupport.HighContrast.projDist_smul_right {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {c : ℝ} (hc : 0 < c) {m₀ m₁ : Matrix n n ℝ} (h₀ : m₀.PosDef) (h₁ : m₁.PosDef) : projDist m₀ (c • m₁) = projDist m₀ m₁

Scaling the second matrix by a positive scalar leaves the distance unchanged.

The two-sided bound

theorem HCPolySupport.HighContrast.projDist_le_of_le {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {m₀ m₁ : Matrix n n ℝ} (h₀ : m₀.PosDef) (h₁ : m₁.PosDef) {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hlow : a • m₀ ≤ m₁) (hhigh : m₁ ≤ b • m₀) : projDist m₀ m₁ ≤ 1 / 2 * Real.log (b / a)

The workhorse bound. A two-sided Loewner sandwich a m₀ ≤ m₁ ≤ b m₀ bounds the projective distance by ½ log (b/a).

The triangle inequality

theorem HCPolySupport.HighContrast.projDist_triangle {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {m₀ m₁ m₂ : Matrix n n ℝ} (h₀ : m₀.PosDef) (h₁ : m₁.PosDef) (h₂ : m₂.PosDef) : projDist m₀ m₂ ≤ projDist m₀ m₁ + projDist m₁ m₂

The triangle inequality of e.scale.selection.projective.distance. The sharp constants of the two sandwiches compose, and the logarithm of the quotient of the composed constants splits into the two distances.