High-contrast homogenization: Entry.Geometry.SpectralExtrema

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

Spectral extrema for the Loewner thresholds

On a positive definite matrix M, the scalar Loewner thresholds specMin M and specBound M are the attained minimum and maximum Hermitian eigenvalues of M, and they equal the L2 operator norms of M⁻¹ and M respectively; for a positive continuous-functional-calculus power of M the two thresholds are the corresponding scalar powers of the originals. These spectral identities provide the projective-distance and geometry-update comparisons used in l.projective.step and in the finite run of p.global.selection.

theorem HCPolySupport.HighContrast.Geometry.specBound_eq_finset_sup_eigenvalues {d : ℕ} {M : Mat d} [NeZero d] (hM : Matrix.PosDef M) : specBound M = Finset.univ.sup' ⋯ ⋯.eigenvalues

On positive definite matrices, the upper Loewner threshold is the attained maximum Hermitian eigenvalue.

theorem HCPolySupport.HighContrast.Geometry.specMin_eq_finset_inf_eigenvalues {d : ℕ} {M : Mat d} [NeZero d] (hM : Matrix.PosDef M) : specMin M = Finset.univ.inf' ⋯ ⋯.eigenvalues

On positive definite matrices, the lower Loewner threshold is the attained minimum Hermitian eigenvalue.

theorem HCPolySupport.HighContrast.Geometry.specMin_pos {d : ℕ} {M : Mat d} [NeZero d] (hM : Matrix.PosDef M) : 0 < specMin M

On positive definite matrices, the lower Loewner threshold is strictly positive.

theorem HCPolySupport.HighContrast.Geometry.posDef_l2_opNorm_eq_specBound {d : ℕ} {M : Mat d} [NeZero d] (hM : Matrix.PosDef M) : ‖M‖ = specBound M

For positive definite matrices, the upper Loewner threshold is Mathlib's L2 operator norm.

theorem HCPolySupport.HighContrast.Geometry.posDef_inv_l2_opNorm_eq_specMin_inv {d : ℕ} {M : Mat d} [NeZero d] (hM : Matrix.PosDef M) : ‖M⁻¹‖ = (specMin M)⁻¹

For positive definite matrices, the L2 operator norm of the inverse is the inverse of the lower Loewner threshold.

theorem HCPolySupport.HighContrast.Geometry.posDef_l2_opNorm_cfc_rpow_eq_specBound_rpow {d : ℕ} {M : Mat d} [NeZero d] (hM : Matrix.PosDef M) {θ : ℝ} (hθ : 0 ≤ θ) : ‖cfc (fun (x : ℝ) => x ^ θ) M‖ = specBound M ^ θ

The L2 operator norm of a positive CFC power is the corresponding power of the upper spectral threshold.

theorem HCPolySupport.HighContrast.Geometry.posDef_inv_l2_opNorm_cfc_rpow_eq_specMin_rpow_inv {d : ℕ} {M : Mat d} [NeZero d] (hM : Matrix.PosDef M) {θ : ℝ} (hθ : 0 ≤ θ) : ‖(cfc (fun (x : ℝ) => x ^ θ) M)⁻¹‖ = (specMin M ^ θ)⁻¹

The L2 operator norm of the inverse of a positive CFC power is the inverse corresponding power of the lower spectral threshold.