Courant–Fischer min-max and Weyl's eigenvalue perturbation inequality

For a symmetric operator T on a finite-dimensional inner product space over 𝕜 = ℝ, ℂ, Mathlib provides the decreasingly sorted eigenvalues LinearMap.IsSymmetric.eigenvalues together with an orthonormal eigenbasis LinearMap.IsSymmetric.eigenvectorBasis. This file proves the discrete Courant–Fischer characterization of these sorted eigenvalues — the directional bounds and the characteristic sup-inf equality — and derives from it Weyl's eigenvalue perturbation inequality.

Main results

• LinearMap.IsSymmetric.re_inner_apply_self_eq_sum_eigenvalues_mul_sq: diagonalization of the quadratic form, re ⟪T x, x⟫ = ∑ i, λᵢ * ‖(b.repr x) i‖ ^ 2 in the eigenbasis b of T.
• LinearMap.IsSymmetric.exists_unit_vector_re_inner_le_eigenvalue: Courant–Fischer, upper direction — every subspace of dimension k + 1 contains a unit vector x with re ⟪T x, x⟫ ≤ λₖ(T).
• LinearMap.IsSymmetric.exists_submodule_forall_unit_eigenvalue_le_re_inner: Courant–Fischer, lower direction — some subspace of dimension k + 1 satisfies λₖ(T) ≤ re ⟪T x, x⟫ for all unit vectors x in it.
• LinearMap.IsSymmetric.eigenvalues_eq_iSup_iInf_re_inner: the Courant–Fischer min-max equality λₖ(T) = ⨆ (V, dim V = k+1), ⨅ (x ∈ V, ‖x‖ = 1), re ⟪T x, x⟫.
• LinearMap.IsSymmetric.eigenvalues_eq_of_eigenbasis: an antitone list diagonalizing T in some orthonormal basis is the sorted eigenvalue list.
• LinearMap.IsSymmetric.eigenvalue_mono: Loewner monotonicity of the sorted eigenvalues in the quadratic form.
• TauCeti.abs_eigenvalue_sub_eigenvalue_le: Weyl's inequality at LinearMap level, with the operator-norm bound supplied pointwise.
• TauCeti.abs_eigenvalue_sub_eigenvalue_le_norm: Weyl's inequality for self-adjoint continuous linear maps, |λₖ(T) − λₖ(S)| ≤ ‖T − S‖.

References

• R. A. Horn and C. R. Johnson, Matrix Analysis, 2nd ed., Theorem 4.2.6 (Courant–Fischer) and Theorem 4.3.1 (Weyl).
• R. Bhatia, Matrix Analysis, Corollary III.2.6 (Weyl).

Namespace note

The eigenvalue results extend LinearMap.IsSymmetric (dot notation on the Mathlib symmetry certificate, matching IsSymmetric.eigenvalues); the two-operator Weyl inequalities are helper facts under TauCeti.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: ForMathlib/Analysis/InnerProductSpace/CourantFischer.lean at Davis--Kahan commit fc38eb48b9b49f2e1d87fe0c7022dc5e262820a7.
• Original declarations: the Courant–Fischer / Weyl API listed above, with the former names specSubspace, re_inner_map_self_eq_sum_eigenvalues_mul_sq, forall_unit_vector_eigenvalue_le_re_inner, abs_eigenvalues_sub_le, abs_eigenvalues_sub_le_opNorm, eigenvalues_le_eigenvalues_of_re_inner_le, map_mem_specSubspace.
• Original authors / copyright: formalized by Claude Fable 5, golfed/polished by Claude Opus 4.8; Apache 2.0. To be re-authored per upstream AI-contribution policy at PR time.
• Extraction class: redesigned per the signature-polish backlog; the min-max equality endpoint is new in the redesign.
• Spectra influence: none — this module imports only Mathlib.

theorem inf_ne_bot_of_finrank_lt {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {V W : Submodule 𝕜 E} (h : Module.finrank 𝕜 E < Module.finrank 𝕜 ↥V + Module.finrank 𝕜 ↥W) : V ⊓ W ≠ ⊥

Two subspaces whose dimensions overshoot the ambient one must meet.

The contrapositive of Submodule.finrank_add_finrank_le_of_disjoint, in the form the min--max arguments below use it; both of them derived it inline from finrank_sup_add_finrank_inf_eq.

theorem Finset.card_filter_lt {n k : ℕ} (hk : k ≤ n) : {j : Fin n | ↑j < k}.card = k

The first k indices of Fin n number exactly k.

A Finset counting fact with no eigenvalue content, kept here because this is the module both of its consumers already import — Analysis/InnerProductSpace/KyFan.lean for the Ky Fan trace inequality and Analysis/OperatorIdeal/ApproximationNumber/FiniteDimensional.lean for a span dimension. Each had its own private copy, differing only by a prime on the name.

Mathlib has Fin.card_Iio but not this filter form, which is the shape a Finset.sum_const leaves behind.

The quadratic form in the eigenbasis

theorem LinearMap.IsSymmetric.re_inner_apply_self_eq_sum_eigenvalues_mul_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (x : E) : RCLike.re (inner 𝕜 (T x) x) = ∑ i : Fin n, hT.eigenvalues hn i * ‖((hT.eigenvectorBasis hn).repr x).ofLp i‖ ^ 2

The quadratic form re ⟪T x, x⟫ of a symmetric operator T expressed in its eigenbasis: it is the eigenvalue-weighted sum of the squared norms of the coordinates of x. This is the diagonalization of the quadratic form. (For symmetric T the inner product ⟪T x, x⟫ is real, so no information is lost by taking the real part.)

theorem LinearMap.IsSymmetric.re_inner_apply_self_le_of_mem_spanIndices {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) {s : Set (Fin n)} {c : ℝ} (hc : ∀ i ∈ s, hT.eigenvalues hn i ≤ c) {x : E} (hx : x ∈ (hT.eigenvectorBasis hn).spanIndices s) : RCLike.re (inner 𝕜 (T x) x) ≤ c * ‖x‖ ^ 2

On the span of a selected subfamily of the eigenbasis, the quadratic form is bounded by any bound on the selected eigenvalues: if x ∈ b.spanIndices s (so its coordinates vanish off s) and every selected eigenvalue satisfies λᵢ ≤ c, then re ⟪T x, x⟫ ≤ c ‖x‖².

theorem LinearMap.IsSymmetric.le_re_inner_apply_self_of_mem_spanIndices {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) {s : Set (Fin n)} {c : ℝ} (hc : ∀ i ∈ s, c ≤ hT.eigenvalues hn i) {x : E} (hx : x ∈ (hT.eigenvectorBasis hn).spanIndices s) : c * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (T x) x)

Dual of re_inner_apply_self_le_of_mem_spanIndices: if x ∈ b.spanIndices s and every selected eigenvalue satisfies c ≤ λᵢ, then c ‖x‖² ≤ re ⟪T x, x⟫.

Discrete Courant–Fischer directional bounds

theorem LinearMap.IsSymmetric.exists_unit_vector_re_inner_le_eigenvalue {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (k : Fin n) (V : Submodule 𝕜 E) (hV : Module.finrank 𝕜 ↥V = ↑k + 1) : ∃ x ∈ V, ‖x‖ = 1 ∧ RCLike.re (inner 𝕜 (T x) x) ≤ hT.eigenvalues hn k

Courant–Fischer, upper direction. On any subspace V of dimension k + 1 there is a unit vector x with re ⟪T x, x⟫ ≤ λₖ(T), where λ is the decreasing enumeration LinearMap.IsSymmetric.eigenvalues of the eigenvalues of the symmetric operator T.

theorem LinearMap.IsSymmetric.exists_submodule_forall_unit_eigenvalue_le_re_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (k : Fin n) : ∃ (V : Submodule 𝕜 E), Module.finrank 𝕜 ↥V = ↑k + 1 ∧ ∀ x ∈ V, ‖x‖ = 1 → hT.eigenvalues hn k ≤ RCLike.re (inner 𝕜 (T x) x)

Courant–Fischer, lower direction. There is a subspace V of dimension k + 1 on which every unit vector x satisfies λₖ(T) ≤ re ⟪T x, x⟫, where λ is the decreasing enumeration LinearMap.IsSymmetric.eigenvalues of the eigenvalues of the symmetric operator T.

Witness: V = span {bᵢ : i ≤ k}; on it the quadratic form is bounded below by λₖ since all involved eigenvalues are ≥ λₖ.

The Courant–Fischer min-max equality

theorem LinearMap.IsSymmetric.eigenvalues_eq_iSup_iInf_re_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (k : Fin n) : hT.eigenvalues hn k = ⨆ (V : { V : Submodule 𝕜 E // Module.finrank 𝕜 ↥V = ↑k + 1 }), ⨅ (x : { x : E // x ∈ ↑V ∧ ‖x‖ = 1 }), RCLike.re (inner 𝕜 (T ↑x) ↑x)

Courant–Fischer min-max equality. The k-th (decreasingly sorted) eigenvalue of a symmetric operator on a finite-dimensional inner product space over 𝕜 = ℝ, ℂ is the supremum, over the subspaces V of dimension k + 1, of the infimum of the Rayleigh quotient re ⟪T x, x⟫ over the unit vectors of V.

Horn & Johnson, Matrix Analysis 2nd ed., Theorem 4.2.6.

Sorted-eigenvalue uniqueness and Loewner monotonicity

Courant–Fischer consequences needed by the Ky Fan / unitarily-invariant-norm development: an antitone list diagonalizing a symmetric operator in some orthonormal basis is the sorted eigenvalue list, and the sorted eigenvalues are monotone in the quadratic form (Loewner order).

theorem LinearMap.IsSymmetric.re_inner_apply_self_eq_sum_of_eigenbasis {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} {S : E →ₗ[𝕜] E} (hS : S.IsSymmetric) (w : OrthonormalBasis (Fin n) 𝕜 E) {μ : Fin n → ℝ} (hw : ∀ (i : Fin n), S (w i) = ↑(μ i) • w i) (x : E) : RCLike.re (inner 𝕜 (S x) x) = ∑ i : Fin n, μ i * ‖(w.repr x).ofLp i‖ ^ 2

Diagonalization of the quadratic form in any orthonormal eigenbasis: if S (w i) = μ i • w i for all i, then re ⟪S x, x⟫ = ∑ i, μ i * ‖w.repr x i‖ ^ 2.

theorem LinearMap.IsSymmetric.eigenvalues_eq_of_eigenbasis {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {S : E →ₗ[𝕜] E} (hS : S.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (w : OrthonormalBasis (Fin n) 𝕜 E) {μ : Fin n → ℝ} (hμ : Antitone μ) (hw : ∀ (i : Fin n), S (w i) = ↑(μ i) • w i) : hS.eigenvalues hn = μ

Sorted-eigenvalue uniqueness. If an orthonormal basis w diagonalizes the symmetric operator S with an antitone value list μ, then μ is the sorted eigenvalue list: hS.eigenvalues hn = μ. (Courant–Fischer: both lists satisfy the same minimax characterization.)

theorem LinearMap.IsSymmetric.eigenvalue_mono {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {T S : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hS : S.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (h : ∀ (x : E), RCLike.re (inner 𝕜 (T x) x) ≤ RCLike.re (inner 𝕜 (S x) x)) (k : Fin n) : hT.eigenvalues hn k ≤ hS.eigenvalues hn k

Loewner monotonicity of the sorted eigenvalues. If the quadratic form of T is dominated by that of S, then so is every sorted eigenvalue.

theorem LinearMap.IsSymmetric.map_mem_spanIndices {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (s : Set (Fin n)) {x : E} (hx : x ∈ (hT.eigenvectorBasis hn).spanIndices s) : T x ∈ (hT.eigenvectorBasis hn).spanIndices s

The span of a selected subfamily of the eigenbasis of a symmetric operator is invariant under the operator.

Weyl's inequality

theorem TauCeti.abs_eigenvalue_sub_eigenvalue_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {T S : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hS : S.IsSymmetric) (hn : Module.finrank 𝕜 E = n) {ε : ℝ} (hε : ∀ (x : E), ‖(T - S) x‖ ≤ ε * ‖x‖) (k : Fin n) : |hT.eigenvalues hn k - hS.eigenvalues hn k| ≤ ε

Weyl's inequality for symmetric operators on a finite-dimensional inner product space over 𝕜 = ℝ, ℂ: the k-th (decreasingly sorted) eigenvalues of T and S differ by at most the operator norm of T − S.

At LinearMap level there is no operator norm, so the bound is supplied as the pointwise hypothesis ∀ x, ‖(T − S) x‖ ≤ ε * ‖x‖; see TauCeti.abs_eigenvalue_sub_eigenvalue_le_norm for the continuous-linear-map operator-norm form.

Horn & Johnson, Matrix Analysis 2nd ed., Theorem 4.3.1; Bhatia, Matrix Analysis, Corollary III.2.6.

theorem TauCeti.abs_eigenvalue_sub_eigenvalue_le_norm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {T S : E →L[𝕜] E} (hT : (↑T).IsSymmetric) (hS : (↑S).IsSymmetric) (hn : Module.finrank 𝕜 E = n) (k : Fin n) : |hT.eigenvalues hn k - hS.eigenvalues hn k| ≤ ‖T - S‖

Weyl's inequality, operator-norm form, for symmetric (equivalently, self-adjoint) continuous linear maps on a finite-dimensional inner product space: the k-th sorted eigenvalues of T and S differ by at most ‖T − S‖. The symmetry hypotheses are stated on the underlying linear maps so that the signature does not require the adjoint star structure (whose instance needs CompleteSpace E, which FiniteDimensional deliberately does not register as an instance).

Related Lean work: YuanheZ/lean-stat-learning-theory, SLT/MatrixInfra/Perturb.lean at commit 216e578c9576bab6b0abc3ba6c65762536768e96, proves the same operator-norm endpoint. The present proof belongs to the local Courant--Fischer chain and is retained to keep the development self-contained.

theorem TauCeti.abs_eigenvalues_sub_le_opNorm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {T S : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hS : S.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (k : Fin n) : |hT.eigenvalues hn k - hS.eigenvalues hn k| ≤ ‖LinearMap.toContinuousLinearMap (T - S)‖

Weyl's inequality, LinearMap form: the bound is the operator norm of T - S read through LinearMap.toContinuousLinearMap.

Two things about this declaration are not free choices, and both are worth stating rather than leaving to be rediscovered.

The name does not follow the convention its neighbours use (abs_eigenvalue_sub_eigenvalue_le, abs_eigenvalue_sub_eigenvalue_le_norm) because it is pinned as data: comparator/candidate-02-courant-fischer-weyl.json lists TauCeti.abs_eigenvalues_sub_le_opNorm in its theorem_names, and the paired immutable challenge statement in Challenge/MathlibCandidate/CourantFischerWeyl/Conformance.lean declares it under that name. Renaming it here would silently orphan the conformance comparison, which no compiler checks.

The duplication with abs_eigenvalue_sub_eigenvalue_le_norm is only apparent. The eigenvalue API is stated for LinearMap.IsSymmetric, so the LinearMap form is the one that needs no coercion in its hypotheses; the continuous form above needs (T : E →ₗ[𝕜] E) in both. They bound the same quantity by norms of two different objects.

theorem TauCeti.eigenvalues_congr {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {S₁ S₂ : E →ₗ[𝕜] E} (h : S₁ = S₂) (hS₁ : S₁.IsSymmetric) (hS₂ : S₂.IsSymmetric) (hn : Module.finrank 𝕜 E = n) : hS₁.eigenvalues hn = hS₂.eigenvalues hn

Sorted eigenvalues are congruent along an operator equality (the eigenvalue enumeration depends only on the operator, not on the symmetry proof).

theorem TauCeti.eigenvalues_cast {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) {m : ℕ} (hm : Module.finrank 𝕜 E = m) (hn : Module.finrank 𝕜 E = n) (hmn : m = n) (i : Fin m) : hT.eigenvalues hm i = hT.eigenvalues hn (Fin.cast hmn i)

The eigenvalue enumeration does not depend on which witness of the dimension indexes it: two witnesses finrank 𝕜 E = m and finrank 𝕜 E = n enumerate the same eigenvalues, read across the induced Fin m ≃ Fin n.

Both spellings occur in practice. A matrix over Fin n has Matrix.IsHermitian.eigenvalues₀ indexed by Fin (Fintype.card (Fin n)), while the operator theory it is transported to indexes by Fin n; Fintype.card (Fin n) = n is a theorem and not definitional, so the two index types are genuinely different.