Ky Fan sums of singular values

For a linear map A : E →ₗ[𝕜] F between finite-dimensional inner product spaces, the Ky Fan k-sum A.kyFanSum k = ∑_{i < k} σᵢ(A) is the sum of its k largest singular values. This file proves Ky Fan's maximum principle: for orthonormal families (uᵢ) in F and (vᵢ) in E with k members,

‖∑ᵢ ⟪uᵢ, A vᵢ⟫‖ ≤ σ₀(A) + ⋯ + σₖ₋₁(A),

with equality attained by the leading singular pairs. The resulting variational characterization LinearMap.kyFanSum_le_iff exhibits each Ky Fan sum as a supremum of the seminorms A ↦ ‖∑ᵢ ⟪uᵢ, A vᵢ⟫‖, so the Ky Fan sums inherit the triangle inequality, homogeneity, and invariance under isometric changes of coordinates, with no comparison of individual singular values. The same weight argument gives Ky Fan's trace inequality for a symmetric operator: over an orthonormal family with k members, the diagonal entries re ⟪T wᵢ, wᵢ⟫ sum to at most the sum of the k largest eigenvalues of T.

The bound expands A in its singular system A x = ∑ⱼ σⱼ ⟪vⱼ', x⟫ uⱼ'. The total weight that the two families place on the j-th singular pair is at most 1 by Bessel's inequality, and the weights add up to at most k by Parseval's identity; such weights against the antitone sequence of singular values give at most the sum of its first k terms (LinearMap.sum_singularValues_mul_le_kyFanSum).

Main declarations

• LinearMap.kyFanSum: the Ky Fan k-sum of singular values.
• LinearMap.norm_sum_inner_le_kyFanSum: Ky Fan's maximum principle, the upper bound.
• LinearMap.sum_re_inner_apply_le_kyFanSum: the corresponding upper bound for the real parts of the diagonal pairings.
• LinearMap.sum_antitone_mul_re_inner_le_sum_mul_singularValues: the same bound with the diagonal pairings weighted by an antitone nonnegative sequence.
• LinearMap.exists_orthonormal_sum_inner_eq_kyFanSum: the leading singular pairs attain it.
• LinearMap.IsPositive.exists_orthonormal_sum_re_inner_eq_kyFanSum: for a positive endomorphism a single orthonormal family attains it on the diagonal, ∑ᵢ re ⟪vᵢ, A vᵢ⟫ = σ₀(A) + ⋯ + σₖ₋₁(A).
• LinearMap.norm_sum_inner_add_inner_le_kyFanSum: the upper bound for families transformed by two pairs of symmetric operators whose squared norms add up to at most the identity.
• LinearMap.norm_trace_comp_linearIsometryEquiv_le_kyFanSum, LinearMap.exists_linearIsometryEquiv_trace_comp_eq_kyFanSum: for an endomorphism A of an n-dimensional space, σ₀(A) + ⋯ + σₙ₋₁(A) is the largest value of ‖tr (A Q)‖ over isometric automorphisms Q, and it is attained with tr (A Q) real.
• LinearMap.kyFanSum_le_iff: the variational characterization.
• LinearMap.kyFanSum_add_le: the Ky Fan triangle inequality.
• LinearMap.isWeaklyMajorizedBy_singularValues_add: its restatement as the weak majorization σ(A + B) ≺w σ(A) + σ(B).
• LinearMap.kyFanSum_smul, LinearMap.kyFanSum_adjoint, LinearMap.kyFanSum_linearIsometryEquiv_comp, LinearMap.kyFanSum_comp_linearIsometryEquiv: homogeneity, and invariance under adjoints and isometric changes of coordinates.
• LinearMap.kyFanSum_subtype_comp_comp_orthogonalProjectionOnto: extending a map by zero between source and target ambient spaces preserves its Ky Fan sums.
• LinearMap.IsSymmetric.sum_re_inner_apply_self_le_sum_eigenvalues: Ky Fan's trace inequality.

Provenance

The zero-extension Ky Fan identity is adapted from ForTauCeti/Analysis/InnerProductSpace/SinTheta/Perturbation.lean in the AIQ-Kitware DKPS formalization (Apache-2.0; Jon Crall and GPT-6).

References

• K. Fan, Maximum properties and inequalities for the eigenvalues of completely continuous operators, Proc. Nat. Acad. Sci. U.S.A. 37 (1951), 760–766.
• R. A. Horn and C. R. Johnson, Matrix Analysis, second edition, Cambridge University Press, 2013, Section 3.4.
• R. Bhatia, Matrix Analysis, Graduate Texts in Mathematics 169, Springer, 1997, Section IV.2.

noncomputable def LinearMap.kyFanSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (k : ℕ) : ℝ

The Ky Fan k-sum of A: the sum σ₀(A) + ⋯ + σₖ₋₁(A) of its k largest singular values.

theorem LinearMap.kyFanSum_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (k : ℕ) : A.kyFanSum k = ∑ i ∈ Finset.range k, A.singularValues i

@[simp]

theorem LinearMap.kyFanSum_zero_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : A.kyFanSum 0 = 0

@[simp]

theorem LinearMap.kyFanSum_succ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (k : ℕ) : A.kyFanSum (k + 1) = A.kyFanSum k + A.singularValues k

@[simp]

theorem LinearMap.kyFanSum_zero_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (k : ℕ) : kyFanSum 0 k = 0

theorem LinearMap.kyFanSum_nonneg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (k : ℕ) : 0 ≤ A.kyFanSum k

theorem LinearMap.kyFanSum_mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : Monotone A.kyFanSum

@[simp]

theorem LinearMap.kyFanSum_min_finrank_range {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (k : ℕ) : A.kyFanSum (min k (Module.finrank 𝕜 ↥A.range)) = A.kyFanSum k

Only the first rank A singular values can be nonzero, so the Ky Fan sums stop growing at the rank.

@[simp]

theorem LinearMap.kyFanSum_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (k : ℕ) : (adjoint A).kyFanSum k = A.kyFanSum k

Taking the adjoint preserves every Ky Fan sum, since A and adjoint A have the same singular values.

theorem LinearMap.sum_singularValues_mul_le_kyFanSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {k : ℕ} {c : Fin (Module.finrank 𝕜 E) → ℝ} (hc0 : ∀ (j : Fin (Module.finrank 𝕜 E)), 0 ≤ c j) (hc1 : ∀ (j : Fin (Module.finrank 𝕜 E)), c j ≤ 1) (hck : ∑ j : Fin (Module.finrank 𝕜 E), c j ≤ ↑k) : ∑ j : Fin (Module.finrank 𝕜 E), A.singularValues ↑j * c j ≤ A.kyFanSum k

Weights cⱼ ∈ [0, 1] of total mass at most k on the singular values of A give at most the Ky Fan k-sum: ∑ⱼ σⱼ cⱼ ≤ σ₀ + ⋯ + σₖ₋₁.

theorem LinearMap.norm_sum_inner_add_inner_le_kyFanSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {ι : Type u_6} [Fintype ι] (A : E →ₗ[𝕜] F) {P₁ Q₁ : F →ₗ[𝕜] F} {P₂ Q₂ : E →ₗ[𝕜] E} (hP₁ : P₁.IsSymmetric) (hQ₁ : Q₁.IsSymmetric) (hP₂ : P₂.IsSymmetric) (hQ₂ : Q₂.IsSymmetric) (h₁ : ∀ (y : F), ‖P₁ y‖ ^ 2 + ‖Q₁ y‖ ^ 2 ≤ ‖y‖ ^ 2) (h₂ : ∀ (x : E), ‖P₂ x‖ ^ 2 + ‖Q₂ x‖ ^ 2 ≤ ‖x‖ ^ 2) {u : ι → F} {v : ι → E} (hu : Orthonormal 𝕜 u) (hv : Orthonormal 𝕜 v) : ‖∑ i : ι, (inner 𝕜 (P₁ (u i)) (A (P₂ (v i))) + inner 𝕜 (Q₁ (u i)) (A (Q₂ (v i))))‖ ≤ A.kyFanSum (Fintype.card ι)

Ky Fan's maximum principle for pairs of contractions. Let P₁, Q₁ be symmetric operators on F with ‖P₁ y‖² + ‖Q₁ y‖² ≤ ‖y‖² for every y, and P₂, Q₂ symmetric operators on E with ‖P₂ x‖² + ‖Q₂ x‖² ≤ ‖x‖² for every x. For orthonormal families (uᵢ) in F and (vᵢ) in E with k members, ‖∑ᵢ (⟪P₁ uᵢ, A (P₂ vᵢ)⟫ + ⟪Q₁ uᵢ, A (Q₂ vᵢ)⟫)‖ is at most the Ky Fan k-sum of A.

With P₁ = P₂ = 1 and Q₁ = Q₂ = 0 this is Ky Fan's maximum principle LinearMap.norm_sum_inner_le_kyFanSum. For symmetric S on F and T on E with eigenvalues αᵢ and βⱼ, taking P₁ = sin (τ S), Q₁ = cos (τ S), P₂ = cos (τ T) and Q₂ = -sin (τ T), it bounds sums twisted by the phases sin (τ (αᵢ - βⱼ)), without passing to complex scalars.

theorem LinearMap.norm_sum_inner_le_kyFanSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {ι : Type u_6} [Fintype ι] (A : E →ₗ[𝕜] F) {u : ι → F} {v : ι → E} (hu : Orthonormal 𝕜 u) (hv : Orthonormal 𝕜 v) : ‖∑ i : ι, inner 𝕜 (u i) (A (v i))‖ ≤ A.kyFanSum (Fintype.card ι)

Ky Fan's maximum principle, the upper bound: for orthonormal families (uᵢ) in F and (vᵢ) in E with k members, ‖∑ᵢ ⟪uᵢ, A vᵢ⟫‖ is at most the Ky Fan k-sum of A.

theorem LinearMap.sum_re_inner_apply_le_kyFanSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {ι : Type u_6} [Fintype ι] (A : E →ₗ[𝕜] F) (u : ι → F) (v : ι → E) (hu : Orthonormal 𝕜 u) (hv : Orthonormal 𝕜 v) : ∑ i : ι, RCLike.re (inner 𝕜 (u i) (A (v i))) ≤ A.kyFanSum (Fintype.card ι)

The real diagonal pairing of two orthonormal families under A is bounded by the Ky Fan sum of its singular values.

theorem LinearMap.sum_antitone_mul_re_inner_le_sum_mul_singularValues {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (B : E →ₗ[𝕜] F) {n : ℕ} (u : Fin n → F) (v : Fin n → E) (hu : Orthonormal 𝕜 u) (hv : Orthonormal 𝕜 v) {w : ℕ → ℝ} (hw : ∀ (i : ℕ), i + 1 < n → w (i + 1) ≤ w i) (hw0 : 0 ≤ w (n - 1)) : ∑ i : Fin n, w ↑i * RCLike.re (inner 𝕜 (u i) (B (v i))) ≤ ∑ i : Fin n, w ↑i * B.singularValues ↑i

Weighted Ky Fan trace core. If the partial real diagonal pairings of two orthonormal families are bounded by the Ky Fan sums, pairing them with weights that are antitone on the first n indices and nonnegative at the last one is bounded by the same weighted pairing with the singular values.

theorem LinearMap.exists_orthonormal_sum_inner_eq_kyFanSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {k : ℕ} (hkE : k ≤ Module.finrank 𝕜 E) (hkF : k ≤ Module.finrank 𝕜 F) : ∃ (u : Fin k → F) (v : Fin k → E), Orthonormal 𝕜 u ∧ Orthonormal 𝕜 v ∧ ∑ i : Fin k, inner 𝕜 (u i) (A (v i)) = ↑(A.kyFanSum k)

Ky Fan's maximum principle, attainment: the first k right singular vectors and the corresponding unit left singular vectors, completed where the singular value vanishes, are orthonormal families with ∑ᵢ ⟪uᵢ, A vᵢ⟫ = σ₀(A) + ⋯ + σₖ₋₁(A).

theorem LinearMap.IsPositive.exists_orthonormal_sum_re_inner_eq_kyFanSum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E} (hA : A.IsPositive) {k : ℕ} (hk : k ≤ Module.finrank 𝕜 E) : ∃ (v : Fin k → E), Orthonormal 𝕜 v ∧ ∑ i : Fin k, RCLike.re (inner 𝕜 (v i) (A (v i))) = A.kyFanSum k

Ky Fan's maximum principle for positive endomorphisms, attainment: for a positive endomorphism A of a finite-dimensional space and k ≤ dim E, some orthonormal family of k vectors has ∑ᵢ re ⟪vᵢ, A vᵢ⟫ = σ₀(A) + ⋯ + σₖ₋₁(A).

theorem LinearMap.norm_trace_comp_linearIsometryEquiv_le_kyFanSum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) (Q : E ≃ₗᵢ[𝕜] E) : ‖(trace 𝕜 E) (A ∘ₗ ↑↑↑Q)‖ ≤ A.kyFanSum (Module.finrank 𝕜 E)

For an endomorphism A of an n-dimensional inner product space and an isometric automorphism Q, ‖tr (A Q)‖ ≤ σ₀(A) + ⋯ + σₙ₋₁(A), the sum of all singular values of A.

theorem LinearMap.exists_linearIsometryEquiv_trace_comp_eq_kyFanSum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) : ∃ (Q : E ≃ₗᵢ[𝕜] E), (trace 𝕜 E) (A ∘ₗ ↑↑↑Q) = ↑(A.kyFanSum (Module.finrank 𝕜 E))

For an endomorphism A of an n-dimensional inner product space, some isometric automorphism Q has tr (A Q) = σ₀(A) + ⋯ + σₙ₋₁(A), the sum of all singular values of A. By LinearMap.norm_trace_comp_linearIsometryEquiv_le_kyFanSum this is the largest value of ‖tr (A Q)‖ over isometric automorphisms Q.

theorem LinearMap.kyFanSum_le_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {k : ℕ} {c : ℝ} : A.kyFanSum k ≤ c ↔ ∀ m ≤ k, ∀ (u : Fin m → F) (v : Fin m → E), Orthonormal 𝕜 u → Orthonormal 𝕜 v → ‖∑ i : Fin m, inner 𝕜 (u i) (A (v i))‖ ≤ c

The variational characterization of the Ky Fan sums: A.kyFanSum k ≤ c exactly when ‖∑ᵢ ⟪uᵢ, A vᵢ⟫‖ ≤ c for all orthonormal families (uᵢ) in F and (vᵢ) in E with at most k members.

theorem LinearMap.kyFanSum_add_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A B : E →ₗ[𝕜] F) (k : ℕ) : (A + B).kyFanSum k ≤ A.kyFanSum k + B.kyFanSum k

The Ky Fan triangle inequality: Kₖ(A + B) ≤ Kₖ(A) + Kₖ(B) for every k.

theorem LinearMap.isWeaklyMajorizedBy_singularValues_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A B : E →ₗ[𝕜] F) (n : ℕ) : TauCeti.IsWeaklyMajorizedBy (fun (i : Fin n) => (A + B).singularValues ↑i) fun (i : Fin n) => A.singularValues ↑i + B.singularValues ↑i

Singular-value triangle majorization. For every length n, the first n singular values of A + B are weakly majorized by the coordinatewise sums of the first n singular values of A and of B.

@[simp]

theorem LinearMap.kyFanSum_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (c : 𝕜) (A : E →ₗ[𝕜] F) (k : ℕ) : (c • A).kyFanSum k = ‖c‖ * A.kyFanSum k

The Ky Fan sums are absolutely homogeneous: Kₖ(c • A) = ‖c‖ Kₖ(A).

@[simp]

theorem LinearMap.kyFanSum_neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (k : ℕ) : (-A).kyFanSum k = A.kyFanSum k

@[simp]

theorem LinearMap.kyFanSum_linearIsometryEquiv_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {F' : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] [NormedAddCommGroup F'] [InnerProductSpace 𝕜 F'] [FiniteDimensional 𝕜 F'] (U : F ≃ₗᵢ[𝕜] F') (A : E →ₗ[𝕜] F) (k : ℕ) : (↑↑↑U ∘ₗ A).kyFanSum k = A.kyFanSum k

Composing on the left with an isometric isomorphism leaves the Ky Fan sums unchanged.

@[simp]

theorem LinearMap.kyFanSum_comp_linearIsometryEquiv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {E' : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [FiniteDimensional 𝕜 E'] (A : E →ₗ[𝕜] F) (V : E' ≃ₗᵢ[𝕜] E) (k : ℕ) : (A ∘ₗ ↑↑↑V).kyFanSum k = A.kyFanSum k

Composing on the right with an isometric isomorphism leaves the Ky Fan sums unchanged.

@[simp]

theorem LinearMap.kyFanSum_subtype_comp_comp_orthogonalProjectionOnto {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (U : Submodule 𝕜 E) (W : Submodule 𝕜 F) (T : ↥U →ₗ[𝕜] ↥W) (k : ℕ) : (W.subtype ∘ₗ T ∘ₗ ↑U.orthogonalProjectionOnto).kyFanSum k = T.kyFanSum k

Extending a map T : U → W by zero on Uᗮ, then including the image in the target ambient space, does not change its Ky Fan singular-value sums.

theorem LinearMap.IsSymmetric.sum_re_inner_apply_self_le_sum_eigenvalues {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) {ι : Type u_6} [Fintype ι] {w : ι → E} (hw : Orthonormal 𝕜 w) : ∑ i : ι, RCLike.re (inner 𝕜 (T (w i)) (w i)) ≤ ∑ j : Fin n with ↑j < Fintype.card ι, hT.eigenvalues hn j

Ky Fan's trace inequality: for a symmetric T and an orthonormal family (wᵢ) with k members, ∑ᵢ re ⟪T wᵢ, wᵢ⟫ is at most the sum λ₀ + ⋯ + λₖ₋₁ of the k largest eigenvalues of T.