High-contrast homogenization: Setup.SpectralNorm

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

The scalar Loewner bound is the spectral norm

The reference text writes |M| for the spectral norm of a symmetric positive semidefinite matrix, and the encoding used throughout is the scalar Loewner bound specBound M = inf {t ≥ 0 : M ≤ t I}. This file identifies the two: for a positive semidefinite matrix, specBound M is the ℓ² operator norm of M, that is, the norm carried by the identification of Mat d with the continuous endomorphisms of EuclideanSpace ℝ (Fin d).

One half is unconditional: Cauchy-Schwarz bounds the quadratic form of any matrix by its operator norm times the squared length, so specBound M ≤ ‖M‖ always. The converse uses positive semidefiniteness through the square root: if 0 ≤ M ≤ t I then M² ≤ t M — because t M - M² = M^{1/2}(t I - M)M^{1/2} — and therefore ‖M x‖² ≤ t² ‖x‖².

theorem HCPolySupport.HighContrast.specBound_le_norm {d : ℕ} (M : Mat d) : specBound M ≤ ‖M‖

The scalar Loewner bound is at most the operator norm, for every matrix: Cauchy-Schwarz bounds the quadratic form of M by ‖M‖ times the squared length.

theorem HCPolySupport.HighContrast.norm_le_specBound {d : ℕ} {M : Mat d} (hM : Matrix.PosSemidef M) : ‖M‖ ≤ specBound M

The operator norm is at most the scalar Loewner bound on positive semidefinite data. If 0 ≤ M ≤ t I then M² ≤ t M ≤ t² I, because t M - M² = M^{1/2}(t I - M)M^{1/2}.

theorem HCPolySupport.HighContrast.specBound_eq_norm {d : ℕ} {M : Mat d} (hM : Matrix.PosSemidef M) : specBound M = ‖M‖

specBound is the spectral norm. On positive semidefinite data the scalar Loewner bound is exactly the ℓ² operator norm, so specBound is the |·| of the reference text.