Min–max bounds for approximation numbers

The approximation number aₙ(T) of a bounded linear map T : E →L[𝕜] F is defined as the distance from T to the maps of rank at most n. This file gives the two variational bounds that make it computable from the geometry of T, in the spirit of the Courant–Fischer principle.

• Coercive subspaces bound aₙ(T) from below. If V ≤ E has rank greater than n and c ‖x‖ ≤ ‖T x‖ for every x ∈ V, then c ≤ aₙ(T). Every map R of rank at most n kills a nonzero vector of V, and on that vector T - R agrees with T. This needs neither an inner product nor completeness, only a normed source space. Over ℝ or ℂ it suffices to check the bound on unit vectors, and the subspace may be given as the span of n + 1 linearly independent vectors.
• Orthogonal tails compute aₙ(T). On a complete inner product space E, aₙ(T) is the infimum, over subspaces V of rank at most n, of the operator norm of T restricted to Vᗮ. Composing T with the orthogonal projection onto V gives an approximant of rank at most n whose error is T on Vᗮ. Conversely, for an approximant R of rank at most n the subspace V = (ker R)ᗮ has rank at most n, and R vanishes up to norm zero on Vᗮ = closure (ker R), so T restricted to Vᗮ is no larger than T - R.
• The converse min–max localization. The coercive-subspace bound has a converse on a pair of spaces E, F exactly when every strict lower bound r < aₙ(T) is beaten by a uniform coercivity bound on the span of n + 1 linearly independent vectors. This is the property TauCeti.HasMinMaxLowerBound 𝕜 E F; it says that aₙ(T) is the supremum of the coercivity constants of T on (n + 1)-dimensional subspaces, and it is the input from which the Ky Fan triangle inequality for approximation numbers is derived.
• Complete source spaces have the localization property. Over ℝ or ℂ, let E be complete and c ≥ 0. Either T is c-coercive on an (n + 1)-dimensional span, or T is c-contractive on the orthogonal complement of a subspace of rank at most n. This is the argument behind Sylvester's law of inertia, applied to the hermitian form ‖T x‖² - c² ‖x‖². A maximal subspace on which the form is nonnegative has dimension at most n, unless the first alternative holds. The form is nonpositive on the subspace orthogonal to it for the form, and that subspace is the orthogonal complement of a subspace of rank at most n, by the Riesz representation of the form. For r < c < aₙ(T), the second alternative would give aₙ(T) ≤ c by the orthogonal-tail bound.

Main declarations

• ContinuousLinearMap.le_singularValue_of_lt_rank: a subspace of rank greater than n on which T is c-coercive forces c ≤ aₙ(T).
• ContinuousLinearMap.le_singularValue_of_lt_rank_of_unit_norm: the same, with the coercivity bound checked on unit vectors.
• ContinuousLinearMap.le_singularValue_of_linearIndependent: the same, for the span of n + 1 linearly independent vectors.
• ContinuousLinearMap.singularValue_id: the approximation numbers of the identity are 1 below the rank of the space and 0 from it on.
• ContinuousLinearMap.singularValue_le_nnnorm_comp_orthogonal: aₙ(T) ≤ ‖T|_{Vᗮ}‖ for every subspace V of rank at most n.
• ContinuousLinearMap.singularValue_eq_iInf_nnnorm_comp_orthogonal: on a complete inner product space, aₙ(T) is the infimum of ‖T|_{Vᗮ}‖ over subspaces V of rank at most n.
• ContinuousLinearMap.exists_linearIndependent_or_exists_rank_le: on a complete inner product space, T is c-coercive on the span of n + 1 linearly independent vectors or c-contractive on the orthogonal complement of a subspace of rank at most n.
• ContinuousLinearMap.singularValue_orthogonalProjectionOnto_comp_comp_subtypeL_le: compressing a map to subspaces of its source and target does not increase its approximation numbers.
• TauCeti.HasMinMaxLowerBound: the converse min–max localization property of a pair of spaces.
• TauCeti.hasMinMaxLowerBound_iff_forall_isLUB: a pair has this property exactly when, for every T and n, aₙ(T) is the least upper bound of the coercivity constants of T on spans of n + 1 linearly independent vectors.
• TauCeti.HasMinMaxLowerBound.exists_rank_eq_coercive: on a pair with the property, a strict lower bound for the first i approximation numbers of T is a coercivity constant of T on a subspace of rank i.
• TauCeti.HasMinMaxLowerBound.of_completeSpace: a complete inner product space has the converse min–max localization property towards every inner product space.
• TauCeti.HasMinMaxLowerBound.exists_singularValue_le_compression: on a pair with the property, the first k approximation numbers of T are those of a compression of T to finite-dimensional subspaces, up to any δ > 0.
• TauCeti.HasMinMaxLowerBound.exists_singularValue_le_compression_endomorphism: the same for an endomorphism, compressed to a single finite-dimensional subspace.

References

• A. Pietsch, Eigenvalues and s-Numbers, Cambridge Studies in Advanced Mathematics 13, Cambridge University Press (1987), Chapter 2.
• I. C. Gohberg, M. G. Krein, Introduction to the Theory of Linear Nonselfadjoint Operators, Translations of Mathematical Monographs 18, AMS (1969), Chapter II.

Lower bounds from coercive subspaces

theorem ContinuousLinearMap.le_singularValue_of_lt_rank {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) {n : ℕ} {V : Submodule 𝕜 E} (hV : ↑n < Module.rank 𝕜 ↥V) {c : ℝ} (hc : ∀ x ∈ V, c * ‖x‖ ≤ ‖T x‖) : c ≤ ↑(T.singularValue n)

Coercive-subspace lower bound. If V has rank greater than n and c ‖x‖ ≤ ‖T x‖ for every x ∈ V, then c ≤ aₙ(T).

theorem ContinuousLinearMap.le_singularValue_of_linearIndependent {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) {n : ℕ} {v : Fin (n + 1) → E} (hv : LinearIndependent 𝕜 v) {c : ℝ} (hc : ∀ x ∈ Submodule.span 𝕜 (Set.range v), c * ‖x‖ ≤ ‖T x‖) : c ≤ ↑(T.singularValue n)

Independent-family lower bound. If T is c-coercive on the span of n + 1 linearly independent vectors, then c ≤ aₙ(T).

@[simp]

theorem ContinuousLinearMap.singularValue_id {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (n : ℕ) : (ContinuousLinearMap.id 𝕜 E).singularValue n = if ↑n < Module.rank 𝕜 E then 1 else 0

Approximation numbers of the identity. On a normed space of rank r, a possibly infinite cardinal, aₙ(id) = 1 for n < r and aₙ(id) = 0 for r ≤ n.

theorem ContinuousLinearMap.singularValue_id_of_finiteDimensional {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] (n : ℕ) : (ContinuousLinearMap.id 𝕜 E).singularValue n = if n < Module.finrank 𝕜 E then 1 else 0

Approximation numbers of a finite-dimensional identity. aₙ(id) = 1 below the dimension and aₙ(id) = 0 at and above it.

theorem ContinuousLinearMap.le_singularValue_of_lt_rank_of_unit_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) {n : ℕ} {V : Submodule 𝕜 E} (hV : ↑n < Module.rank 𝕜 ↥V) {c : ℝ} (hc : ∀ x ∈ V, ‖x‖ = 1 → c ≤ ‖T x‖) : c ≤ ↑(T.singularValue n)

Coercive-subspace lower bound on unit vectors. If V has rank greater than n and c ≤ ‖T x‖ for every unit vector x ∈ V, then c ≤ aₙ(T).

The orthogonal-tail formula

theorem ContinuousLinearMap.rank_comp_starProjection_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type u_3} [TopologicalSpace F] [AddCommMonoid F] [Module 𝕜 F] (T : E →L[𝕜] F) {n : ℕ} {V : Submodule 𝕜 E} [V.HasOrthogonalProjection] (hV : Module.rank 𝕜 ↥V ≤ ↑n) : (↑(T ∘SL V.starProjection)).rank ≤ ↑n

Composing with the projection onto a subspace of rank at most n has rank at most n. The target needs only a topology and a module structure; no target norm is used.

theorem ContinuousLinearMap.nnnorm_sub_comp_starProjection_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type u_3} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (V : Submodule 𝕜 E) [V.HasOrthogonalProjection] : ‖T - T ∘SL V.starProjection‖₊ ≤ ‖T ∘SL Vᗮ.subtypeL‖₊

The projection approximant's error is bounded by the norm on the orthogonal complement.

theorem ContinuousLinearMap.singularValue_le_nnnorm_comp_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type u_3} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) {n : ℕ} {V : Submodule 𝕜 E} (hV : Module.rank 𝕜 ↥V ≤ ↑n) : T.singularValue n ≤ ‖T ∘SL Vᗮ.subtypeL‖₊

Orthogonal-tail upper bound. For every subspace V of rank at most n, aₙ(T) is at most the operator norm of T restricted to Vᗮ.

theorem ContinuousLinearMap.singularValue_eq_iInf_nnnorm_comp_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type u_3} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] (T : E →L[𝕜] F) (n : ℕ) : T.singularValue n = ⨅ (V : { V : Submodule 𝕜 E // Module.rank 𝕜 ↥V ≤ ↑n }), ‖T ∘SL (↑V)ᗮ.subtypeL‖₊

Orthogonal-tail min–max formula. On a complete inner product space, aₙ(T) is the infimum, over subspaces V of rank at most n, of the operator norm of T restricted to Vᗮ.

theorem ContinuousLinearMap.exists_linearIndependent_or_exists_rank_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] (T : E →L[𝕜] F) (n : ℕ) {c : ℝ} (hc : 0 ≤ c) : (∃ (v : Fin (n + 1) → E), LinearIndependent 𝕜 v ∧ ∀ x ∈ Submodule.span 𝕜 (Set.range v), c * ‖x‖ ≤ ‖T x‖) ∨ ∃ (U : Submodule 𝕜 E), Module.rank 𝕜 ↥U ≤ ↑n ∧ ∀ x ∈ Uᗮ, ‖T x‖ ≤ c * ‖x‖

Coercive subspace or contractive orthogonal tail. Let T : E →L[𝕜] F be a bounded linear map on a complete inner product space, n : ℕ and c ≥ 0. Either T is c-coercive, c ‖x‖ ≤ ‖T x‖, on the span of n + 1 linearly independent vectors, or there is a subspace U of rank at most n on whose orthogonal complement ‖T x‖ ≤ c ‖x‖.

theorem ContinuousLinearMap.singularValue_orthogonalProjectionOnto_comp_comp_subtypeL_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (W : Submodule 𝕜 F) [W.HasOrthogonalProjection] (V : Submodule 𝕜 E) (T : E →L[𝕜] F) (n : ℕ) : (W.orthogonalProjectionOnto ∘SL T ∘SL V.subtypeL).singularValue n ≤ T.singularValue n

Compressing T to subspaces V ≤ E and W ≤ F, by the inclusion of V and the orthogonal projection onto W, does not increase its approximation numbers.

The converse min–max localization

def TauCeti.HasMinMaxLowerBound (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : Prop

A pair of spaces E, F has the converse min–max localization property when, for every bounded linear map T : E →L[𝕜] F and every n, each nonnegative strict lower bound 0 ≤ r < aₙ(T) is improved by a uniform coercivity bound s ‖x‖ ≤ ‖T x‖, with r < s, on the span of some n + 1 linearly independent vectors.

Together with the coercive-subspace bound ContinuousLinearMap.le_singularValue_of_linearIndependent this says that aₙ(T) is the supremum of the coercivity constants of T on (n + 1)-dimensional subspaces (HasMinMaxLowerBound.isLUB_singularValue).

theorem TauCeti.hasMinMaxLowerBound_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : HasMinMaxLowerBound 𝕜 E F ↔ ∀ (T : E →L[𝕜] F) (n : ℕ) {r : ℝ}, 0 ≤ r → r < ↑(T.singularValue n) → ∃ (s : ℝ), r < s ∧ ∃ (v : Fin (n + 1) → E), LinearIndependent 𝕜 v ∧ ∀ x ∈ Submodule.span 𝕜 (Set.range v), s * ‖x‖ ≤ ‖T x‖

Unfolding HasMinMaxLowerBound.

theorem TauCeti.HasMinMaxLowerBound.exists_rank_eq_coercive {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (h : HasMinMaxLowerBound 𝕜 E F) (T : E →L[𝕜] F) {i : ℕ} {t : ℝ} (ht : 0 ≤ t) (hi : ∀ k < i, t < ↑(T.singularValue k)) : ∃ (V : Submodule 𝕜 E), Module.rank 𝕜 ↥V = ↑i ∧ ∀ x ∈ V, t * ‖x‖ ≤ ‖T x‖

Coercive subspaces of a prescribed rank. On a pair with the converse min–max localization property, if 0 ≤ t lies strictly below the first i approximation numbers of T, then T is t-coercive on a subspace of rank i. The source may be seminormed.

theorem TauCeti.hasMinMaxLowerBound_iff_forall_isLUB {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : HasMinMaxLowerBound 𝕜 E F ↔ ∀ (T : E →L[𝕜] F) (n : ℕ), IsLUB {s : NNReal | ∃ (v : Fin (n + 1) → E), LinearIndependent 𝕜 v ∧ ∀ x ∈ Submodule.span 𝕜 (Set.range v), ↑s * ‖x‖ ≤ ‖T x‖} (T.singularValue n)

The set of coercivity constants of T on spans of n + 1 linearly independent vectors is bounded above by aₙ(T), and aₙ(T) is its least upper bound exactly on pairs with the converse min–max localization property.

theorem TauCeti.HasMinMaxLowerBound.isLUB_singularValue {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (h : HasMinMaxLowerBound 𝕜 E F) (T : E →L[𝕜] F) (n : ℕ) : IsLUB {s : NNReal | ∃ (v : Fin (n + 1) → E), LinearIndependent 𝕜 v ∧ ∀ x ∈ Submodule.span 𝕜 (Set.range v), ↑s * ‖x‖ ≤ ‖T x‖} (T.singularValue n)

Finite-restriction supremum. On a pair with the converse min–max localization property, aₙ(T) is the least upper bound of the coercivity constants of T on spans of n + 1 linearly independent vectors.

theorem TauCeti.HasMinMaxLowerBound.of_completeSpace {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] : HasMinMaxLowerBound 𝕜 E F

Converse min–max localization. If E is a complete inner product space, then for every bounded T : E →L[𝕜] F into an inner product space and every 0 ≤ r < aₙ(T), the map T is s-coercive with r < s on the span of n + 1 linearly independent vectors. Thus aₙ(T) is the supremum of the coercivity constants of T on (n + 1)-dimensional subspaces (TauCeti.HasMinMaxLowerBound.isLUB_singularValue).

theorem TauCeti.HasMinMaxLowerBound.exists_singularValue_le_compression {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (h : HasMinMaxLowerBound 𝕜 E F) (T : E →L[𝕜] F) (k : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (V : Submodule 𝕜 E) (x : FiniteDimensional 𝕜 ↥V), ∀ n < k, ↑(T.singularValue n) ≤ ↑(((Submodule.map (↑T) V).orthogonalProjectionOnto ∘SL T ∘SL V.subtypeL).singularValue n) + δ

Finite-dimensional compressions. On a pair with the converse min–max localization property, for every k and δ > 0 there is a finite-dimensional subspace V such that the compression V → T(V) of T, followed by the orthogonal projection onto T(V), lowers none of the first k approximation numbers of T by more than δ.

theorem TauCeti.HasMinMaxLowerBound.exists_singularValue_le_compression_endomorphism {𝕜 : Type u_4} [RCLike 𝕜] {E : Type u_7} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (h : HasMinMaxLowerBound 𝕜 E E) (T : E →L[𝕜] E) (k : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (U : Submodule 𝕜 E) (x : FiniteDimensional 𝕜 ↥U), ∀ n < k, ↑(T.singularValue n) ≤ ↑((U.orthogonalProjectionOnto ∘SL T ∘SL U.subtypeL).singularValue n) + δ

Finite-dimensional compressions of endomorphisms. On a space with the converse min–max localization property towards itself, for every k and δ > 0 there is a finite-dimensional subspace U such that the compression P_U T|_U : U → U of an endomorphism T lowers none of the first k approximation numbers of T by more than δ. Unlike TauCeti.HasMinMaxLowerBound.exists_singularValue_le_compression, the same subspace is used for the source and the target, so that the compression of a positive operator is positive.