High-contrast homogenization: Entry.Geometry.ProjectiveMetric

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

Metric support for the projective distance

For positive definite matrices m₀ m₁ : Mat d, the projective distance projectiveDistance m₀ m₁ is half the logarithm of the optimal relative Loewner spread. The spectral thresholds specMin and specBound of the normalized relative matrix normalizedMat m₀ m₁ are attained at its eigenvalues, and they are exactly the sharp lower and upper thresholds of the relative comparisons t • m₀ against m₁, so the distance is 1 / 2 * Real.log (U / L) for those two thresholds. The distance is nonnegative, vanishes exactly on the positive-scalar equivalence classes, is invariant under positive scaling of its right endpoint, and satisfies the triangle inequality; from the identity it equals half the logarithm of the eccentricity ‖m‖ * ‖m⁻¹‖. These are the metric facts used by l.projective.step, and the triangle inequality is used in the finite run of p.global.selection.

theorem HCPolySupport.HighContrast.Geometry.spectral_extrema_attained {d : ℕ} {M : Mat d} [NeZero d] (hM : Matrix.PosDef M) : ∃ (i : Fin d) (j : Fin d), specMin M = ⋯.eigenvalues i ∧ specBound M = ⋯.eigenvalues j ∧ ∀ (k : Fin d), ⋯.eigenvalues i ≤ ⋯.eigenvalues k ∧ ⋯.eigenvalues k ≤ ⋯.eigenvalues j

The lower and upper Loewner thresholds are attained eigenvalues.

theorem HCPolySupport.HighContrast.Geometry.normalizedMat_posDef {d : ℕ} {m₀ m₁ : Mat d} (h₀ : Matrix.PosDef m₀) (h₁ : Matrix.PosDef m₁) : Matrix.PosDef (normalizedMat m₀ m₁)

The normalized relative matrix of two positive matrices is positive definite.

theorem HCPolySupport.HighContrast.Geometry.matLoewnerLE_smul_left_iff_specMin {d : ℕ} {m₀ m₁ : Mat d} [NeZero d] (h₀ : Matrix.PosDef m₀) (h₁ : Matrix.PosDef m₁) (t : ℝ) : MatLoewnerLE (t • m₀) m₁ ↔ t ≤ specMin (normalizedMat m₀ m₁)

Lower relative Loewner comparisons are exactly the lower spectral threshold of the normalized relative matrix.

theorem HCPolySupport.HighContrast.Geometry.matLoewnerLE_right_iff_specBound_le {d : ℕ} {m₀ m₁ : Mat d} [NeZero d] (h₀ : Matrix.PosDef m₀) (h₁ : Matrix.PosDef m₁) (t : ℝ) : MatLoewnerLE m₁ (t • m₀) ↔ specBound (normalizedMat m₀ m₁) ≤ t

Upper relative Loewner comparisons are exactly the upper spectral threshold of the normalized relative matrix.

theorem HCPolySupport.HighContrast.Geometry.projectiveDistance_eq_log_relative_spread {d : ℕ} {m₀ m₁ : Mat d} [NeZero d] (h₀ : Matrix.PosDef m₀) (h₁ : Matrix.PosDef m₁) : ∃ (L : ℝ) (U : ℝ), 0 < L ∧ L ≤ U ∧ (∀ (t : ℝ), MatLoewnerLE (t • m₀) m₁ ↔ t ≤ L) ∧ (∀ (t : ℝ), MatLoewnerLE m₁ (t • m₀) ↔ U ≤ t) ∧ L = specMin (normalizedMat m₀ m₁) ∧ U = specBound (normalizedMat m₀ m₁) ∧ projectiveDistance m₀ m₁ = 1 / 2 * Real.log (U / L)

The projective distance is the logarithm of the optimal relative Loewner spread.

theorem HCPolySupport.HighContrast.Geometry.projectiveDistance_nonneg {d : ℕ} {m₀ m₁ : Mat d} [NeZero d] (h₀ : Matrix.PosDef m₀) (h₁ : Matrix.PosDef m₁) : 0 ≤ projectiveDistance m₀ m₁

The projective distance between positive matrices is nonnegative.

theorem HCPolySupport.HighContrast.Geometry.projectiveDistance_smul_right {d : ℕ} {m₀ m₁ : Mat d} [NeZero d] (h₀ : Matrix.PosDef m₀) (h₁ : Matrix.PosDef m₁) {c : ℝ} (hc : 0 < c) : projectiveDistance m₀ (c • m₁) = projectiveDistance m₀ m₁

The projective distance is invariant under positive scaling in the right endpoint.

theorem HCPolySupport.HighContrast.Geometry.projectiveDistance_eq_zero_iff {d : ℕ} {m₀ m₁ : Mat d} [NeZero d] (h₀ : Matrix.PosDef m₀) (h₁ : Matrix.PosDef m₁) : projectiveDistance m₀ m₁ = 0 ↔ ProjectiveEq m₀ m₁

The projective distance vanishes exactly on the positive-scalar equivalence relation.

theorem HCPolySupport.HighContrast.Geometry.projectiveDistance_triangle {d : ℕ} {m₀ m₁ m₂ : Mat d} [NeZero d] (h₀ : Matrix.PosDef m₀) (h₁ : Matrix.PosDef m₁) (h₂ : Matrix.PosDef m₂) : projectiveDistance m₀ m₂ ≤ projectiveDistance m₀ m₁ + projectiveDistance m₁ m₂

The projective distance satisfies the triangle inequality on positive matrices.

theorem HCPolySupport.HighContrast.Geometry.projectiveDistance_one_eq_log_eccentricity {d : ℕ} {m : Mat d} [NeZero d] (hm : Matrix.PosDef m) : projectiveDistance 1 m = 1 / 2 * Real.log (‖m‖ * ‖m⁻¹‖)

The projective distance from the identity is the logarithm of the eccentricity expression using Mathlib's L2 operator norm.