Courant–Fischer min–max theorem and Weyl's inequality

For a finite-dimensional inner-product space over ℝ or ℂ, the min–max theorem characterizes the decreasingly sorted eigenvalues of a symmetric endomorphism through its Rayleigh form. The same argument gives monotonicity under quadratic- form domination and Weyl's perturbation bound.

Main results

• LinearMap.IsSymmetric.re_inner_apply_self_eq_sum_eigenvalues_mul_sq: diagonal expansion of the Rayleigh form in an eigenbasis.
• LinearMap.sq_norm_apply_eq_sum_of_eigenbasis: diagonal expansion of ‖T x‖² in an eigenbasis.
• LinearMap.IsSymmetric.exists_unit_vector_re_inner_le_eigenvalue and LinearMap.IsSymmetric.exists_submodule_forall_unit_eigenvalue_le_re_inner: the two min–max directions.
• LinearMap.IsSymmetric.exists_unit_vector_re_inner_le_eigenvalue_of_le_finrank: the upper direction for subspaces of dimension at least k + 1.
• LinearMap.IsSymmetric.eigenvalues_eq_iSup_iInf_re_inner: the Courant–Fischer equality.
• LinearMap.IsSymmetric.eigenvalue_mono: monotonicity of sorted eigenvalues under quadratic-form order.
• LinearMap.IsSymmetric.abs_eigenvalue_sub_eigenvalue_le and LinearMap.IsSymmetric.abs_eigenvalue_sub_eigenvalue_le_norm: Weyl's perturbation inequality.
• LinearMap.IsSymmetric.eigenvalues_add_le and LinearMap.IsSymmetric.le_eigenvalues_add: Weyl's additive inequalities comparing the sorted eigenvalues of T + S with those of T and S.
• LinearMap.IsSymmetric.eigenvalues_le_eigenvalues_of_isometry and LinearMap.IsSymmetric.eigenvalues_le_eigenvalues_of_isometry': eigenvalue bounds for a symmetric compression along a linear isometry.

References

• R. A. Horn and C. R. Johnson, Matrix Analysis, 2nd ed., Theorems 4.2.6 and 4.3.1.
• R. Bhatia, Matrix Analysis, Corollary III.2.6.

Provenance

Ported and adapted from ForTauCeti/Analysis/InnerProductSpace/CourantFischer.lean in Kitware's DKPS formalization (Apache-2.0). The original proof development was by Claude Fable 5, with polishing by Claude Opus 4.8 and oversight by Jon Crall.

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

The squared norm in any orthonormal eigenbasis: if S (w i) = μ i • w i for all i, then ‖S x‖ ^ 2 = ∑ i, ‖μ i‖ ^ 2 * ‖w.repr x i‖ ^ 2.

theorem LinearMap.re_inner_apply_self_eq_sum_of_eigenbasis {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} (S : E →ₗ[𝕜] E) (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.le_re_inner_of_eigenbasis {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} (S : E →ₗ[𝕜] E) (w : OrthonormalBasis (Fin n) 𝕜 E) {μ : Fin n → ℝ} (hw : ∀ (i : Fin n), S (w i) = ↑(μ i) • w i) {s : Set (Fin n)} {c : ℝ} (hc : ∀ i ∈ s, c ≤ μ i) {x : E} (hx : x ∈ w.spanIndices s) : c * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (S x) x)

On the span of the eigenvectors selected by s, the quadratic form is bounded below by any lower bound on the selected values (general-eigenbasis version of le_re_inner_apply_self_of_mem_spanIndices).

theorem LinearMap.re_inner_le_of_eigenbasis {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} (S : E →ₗ[𝕜] E) (w : OrthonormalBasis (Fin n) 𝕜 E) {μ : Fin n → ℝ} (hw : ∀ (i : Fin n), S (w i) = ↑(μ i) • w i) {s : Set (Fin n)} {c : ℝ} (hc : ∀ i ∈ s, μ i ≤ c) {x : E} (hx : x ∈ w.spanIndices s) : RCLike.re (inner 𝕜 (S x) x) ≤ c * ‖x‖ ^ 2

Dual of le_re_inner_of_eigenbasis.

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_unit_vector_re_inner_le_eigenvalue_of_le_finrank {𝕜 : 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 : ↑k + 1 ≤ Module.finrank 𝕜 ↥V) : ∃ x ∈ V, ‖x‖ = 1 ∧ RCLike.re (inner 𝕜 (T x) x) ≤ hT.eigenvalues hn k

Courant–Fischer, upper direction, for large subspaces. On any subspace V of dimension at least k + 1 there is a unit vector x with re ⟪T x, x⟫ ≤ λₖ(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.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 LinearMap.IsSymmetric.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 LinearMap.IsSymmetric.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 LinearMap.IsSymmetric.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).

The bound is expressed directly in the norm of a continuous linear map.

theorem LinearMap.IsSymmetric.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| ≤ ‖toContinuousLinearMap (T - S)‖

Weyl's inequality for linear maps, using the operator norm of the corresponding continuous linear map. Unlike the preceding theorem, the symmetry hypotheses and eigenvalue enumeration are directly attached to LinearMaps.

theorem LinearMap.IsSymmetric.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 LinearMap.IsSymmetric.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.

Weyl's additive inequalities

theorem LinearMap.IsSymmetric.eigenvalues_add_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) {i j k : Fin n} (hk : ↑i + ↑j ≤ ↑k) : ⋯.eigenvalues hn k ≤ hT.eigenvalues hn i + hS.eigenvalues hn j

Weyl's additive inequality, upper form: for symmetric operators T and S and indices with i + j ≤ k, the decreasingly sorted eigenvalues satisfy λₖ(T + S) ≤ λᵢ(T) + λⱼ(S). Indices start at 0, so for k = i + j this is the classical λ_{i+j-1}(T + S) ≤ λᵢ(T) + λⱼ(S) in one-based indexing.

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

theorem LinearMap.IsSymmetric.le_eigenvalues_add {𝕜 : 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) {i j k : Fin n} (hk : ↑k + n ≤ ↑i + ↑j + 1) : hT.eigenvalues hn i + hS.eigenvalues hn j ≤ ⋯.eigenvalues hn k

Weyl's additive inequality, lower form: for symmetric operators T and S on an n-dimensional space and indices with k + n ≤ i + j + 1, the decreasingly sorted eigenvalues satisfy λᵢ(T) + λⱼ(S) ≤ λₖ(T + S). For k + n = i + j + 1 this is the classical λᵢ(T) + λⱼ(S) ≤ λ_{i+j-n}(T + S) in one-based indexing.

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

theorem LinearMap.IsSymmetric.eigenvalues_le_eigenvalues_of_isometry {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {n m : ℕ} {T : E →ₗ[𝕜] E} {S : F →ₗ[𝕜] F} (hT : T.IsSymmetric) (hS : S.IsSymmetric) (hE : Module.finrank 𝕜 E = n) (hF : Module.finrank 𝕜 F = m) (ι : F →ₗᵢ[𝕜] E) (hST : ∀ (x : F), inner 𝕜 (S x) x = inner 𝕜 (T (ι x)) (ι x)) (hmn : m ≤ n) (k : Fin m) : hS.eigenvalues hF k ≤ hT.eigenvalues hE (Fin.castLE hmn k)

Cauchy interlacing for a compression, upper bound. If S is the compression of the symmetric operator T along a linear isometry ι, then λₖ(S) ≤ λₖ(T).

theorem LinearMap.IsSymmetric.eigenvalues_le_eigenvalues_of_isometry' {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {n m : ℕ} {T : E →ₗ[𝕜] E} {S : F →ₗ[𝕜] F} (hT : T.IsSymmetric) (hS : S.IsSymmetric) (hE : Module.finrank 𝕜 E = n) (hF : Module.finrank 𝕜 F = m) (ι : F →ₗᵢ[𝕜] E) (hST : ∀ (x : F), inner 𝕜 (S x) x = inner 𝕜 (T (ι x)) (ι x)) (hmn : m ≤ n) (k : Fin m) : hT.eigenvalues hE (Fin.cast ⋯ (k.addNat (n - m))) ≤ hS.eigenvalues hF k

Cauchy interlacing for a compression, lower bound. If S is the compression of the symmetric operator T along a linear isometry ι, then λ_{k + (n - m)}(T) ≤ λₖ(S).