Ky Fan gauges of positive operators

For a positive operator T on a Hilbert space, the Ky Fan gauge Kₖ(T) = a₀(T) + ⋯ + aₖ₋₁(T) is the supremum of the diagonal sums ∑ᵢ re ⟪vᵢ, T vᵢ⟫ along orthonormal families of at most k vectors (ContinuousLinearMap.IsPositive.kyFanGauge_le_iff). This is Ky Fan's maximum principle for positive operators: one orthonormal family does the work of the two families in the general principle ContinuousLinearMap.norm_sum_inner_le_kyFanGauge.

The upper bound is the general principle. For the lower bound, the converse min–max localization TauCeti.HasMinMaxLowerBound.exists_singularValue_le_compression_endomorphism approximates the first k approximation numbers of T by those of a compression of T to a finite-dimensional subspace U, and the compression is again positive. On U the leading singular pairs attain the Ky Fan sum as ∑ᵢ ⟪uᵢ, T vᵢ⟫, and positivity of the quadratic form, 2 re ⟪u, T v⟫ ≤ re ⟪u, T u⟫ + re ⟪v, T v⟫, shows that the diagonal sum along (vᵢ) attains it too (LinearMap.IsPositive.exists_orthonormal_sum_re_inner_eq_kyFanSum).

The variational description gives the converse of the Ky Fan triangle inequality for positive operators, Kₖ(S) + Kₗ(T) ≤ Kₖ₊ₗ(S + T) (ContinuousLinearMap.IsPositive.kyFanGauge_add_kyFanGauge_le): two nearly maximizing families span a subspace of dimension at most k + l, and the diagonal sums of S and T along each family are at most their traces on that subspace. Combined with Kₖ(S + T) ≤ Kₖ(S) + Kₖ(T), this is the estimate making the logarithmic means Kₙ(T) / log (1 + n) additive in the limit on positive operators, and hence Dixmier traces additive on the positive part of the logarithmic ideal.

Main declarations

• ContinuousLinearMap.IsPositive.exists_orthonormal_kyFanGauge_le_sum_re_inner_add: up to any ε > 0, some orthonormal family of at most k vectors attains Kₖ(T) on the diagonal.
• ContinuousLinearMap.IsPositive.kyFanGauge_le_iff: Ky Fan's maximum principle for positive operators.
• ContinuousLinearMap.IsPositive.kyFanGauge_add_kyFanGauge_le: Kₖ(S) + Kₗ(T) ≤ Kₖ₊ₗ(S + T) for positive S and T.
• ContinuousLinearMap.IsPositive.kyFanGauge_mono: Kₖ(S) ≤ Kₖ(T) when 0 ≤ S ≤ T.

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.
• A. Connes, Noncommutative Geometry, Academic Press, 1994, Chapter IV, §2.β.
• B. Simon, Trace Ideals and Their Applications, second edition, AMS, 2005, Chapter 1.

theorem ContinuousLinearMap.IsPositive.exists_orthonormal_kyFanGauge_le_sum_re_inner_add {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : T.IsPositive) (k : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (m : ℕ) (v : Fin m → E), m ≤ k ∧ Orthonormal 𝕜 v ∧ ↑(T.kyFanGauge k) ≤ ∑ i : Fin m, RCLike.re (inner 𝕜 (v i) (T (v i))) + ε

Ky Fan's maximum principle for positive operators, approximate attainment: for a positive operator T on a Hilbert space and ε > 0, some orthonormal family of at most k vectors has a₀(T) + ⋯ + aₖ₋₁(T) ≤ ∑ᵢ re ⟪vᵢ, T vᵢ⟫ + ε.

theorem ContinuousLinearMap.IsPositive.kyFanGauge_le_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : T.IsPositive) {k : ℕ} {c : ℝ} : ↑(T.kyFanGauge k) ≤ c ↔ ∀ m ≤ k, ∀ (v : Fin m → E), Orthonormal 𝕜 v → ∑ i : Fin m, RCLike.re (inner 𝕜 (v i) (T (v i))) ≤ c

Ky Fan's maximum principle for positive operators. For a positive operator T on a Hilbert space, a₀(T) + ⋯ + aₖ₋₁(T) ≤ c exactly when ∑ᵢ re ⟪vᵢ, T vᵢ⟫ ≤ c for every orthonormal family (vᵢ) of at most k vectors.

theorem ContinuousLinearMap.IsPositive.kyFanGauge_add_kyFanGauge_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {S T : E →L[𝕜] E} (hS : S.IsPositive) (hT : T.IsPositive) (k l : ℕ) : S.kyFanGauge k + T.kyFanGauge l ≤ (S + T).kyFanGauge (k + l)

Ky Fan superadditivity for positive operators. For positive operators S and T on a Hilbert space, Kₖ(S) + Kₗ(T) ≤ Kₖ₊ₗ(S + T), where Kₖ is the sum of the first k approximation numbers. Together with the triangle inequality Kₖ(S + T) ≤ Kₖ(S) + Kₖ(T) this gives Kₖ(S + T) ≤ Kₖ(S) + Kₖ(T) ≤ K₂ₖ(S + T).

theorem ContinuousLinearMap.IsPositive.kyFanGauge_mono {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {S T : E →L[𝕜] E} (hS : S.IsPositive) (hST : S ≤ T) (k : ℕ) : S.kyFanGauge k ≤ T.kyFanGauge k

Loewner monotonicity of Ky Fan gauges. If 0 ≤ S ≤ T, then Kₖ(S) ≤ Kₖ(T).