The exact finite-dimensional rank cutoff

The zero-based approximation number vanishes exactly at and above the rank. This is a normed-space statement: no inner product, singular-value decomposition, or choice of orthonormal basis is required. The converse uses openness of a finite rank lower bound in the operator-norm topology.

This implements OI-A24 using the canonical real-valued approximationNumber API.

theorem ContinuousLinearMap.approximationNumber_eq_zero_iff_rank_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) : T.approximationNumber n = 0 ↔ (↑T).rank ≤ ↑n

Vanishing of an approximation number characterizes the rank. Only the source needs to be finite-dimensional.

theorem ContinuousLinearMap.approximationNumber_eq_zero_iff_finrank_range_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) : T.approximationNumber n = 0 ↔ Module.finrank 𝕜 ↥(↑T).range ≤ n

The finite-rank version with a natural-number dimension.