Equality of approximation-number sequences

Two continuous linear maps have the same approximation numbers when their ℝ≥0-valued singular-value sequences agree at every index. The two maps may act between different seminormed spaces, including spaces in different universes. This relation is reflexive, symmetric, and transitive. Equal sequences also have equal Ky Fan prefix gauges, so properties determined solely by approximation numbers can be transported between these operators.

Provenance

Adapted from ForTauCeti/Analysis/OperatorIdeal/ApproximationNumber/SameSequence.lean in AIQ-Kitware/aiq-dkps-formalization (Kitware, Inc., Apache-2.0), using TauCeti's nonnegative singularValue sequence.

def ContinuousLinearMap.SameSingularValues {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup H] [NormedSpace 𝕜 H] (S : E →L[𝕜] F) (T : G →L[𝕜] H) : Prop

Equality of the zero-based approximation-number sequences of two maps, possibly between different seminormed spaces.

theorem ContinuousLinearMap.sameSingularValues_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup H] [NormedSpace 𝕜 H] (S : E →L[𝕜] F) (T : G →L[𝕜] H) : S.SameSingularValues T ↔ ∀ (n : ℕ), S.singularValue n = T.singularValue n

Two maps have the same approximation-number sequence if and only if their nonnegative singular values agree at every index.

@[simp]

theorem ContinuousLinearMap.sameSingularValues_refl {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) : T.SameSingularValues T

Every bounded map has the same approximation numbers as itself.

theorem ContinuousLinearMap.sameSingularValues_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup H] [NormedSpace 𝕜 H] {S : E →L[𝕜] F} {T : G →L[𝕜] H} (h : S.SameSingularValues T) : T.SameSingularValues S

Equality of approximation-number sequences is symmetric.

theorem ContinuousLinearMap.sameSingularValues_trans {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} {I : Type u_6} {J : Type u_7} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup H] [NormedSpace 𝕜 H] [SeminormedAddCommGroup I] [NormedSpace 𝕜 I] [SeminormedAddCommGroup J] [NormedSpace 𝕜 J] {S : E →L[𝕜] F} {T : G →L[𝕜] H} {U : I →L[𝕜] J} (hST : S.SameSingularValues T) (hTU : T.SameSingularValues U) : S.SameSingularValues U

Equality of approximation-number sequences is transitive.

theorem ContinuousLinearMap.SameSingularValues.kyFanGauge_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup H] [NormedSpace 𝕜 H] {S : E →L[𝕜] F} {T : G →L[𝕜] H} (h : S.SameSingularValues T) (k : ℕ) : S.kyFanGauge k = T.kyFanGauge k

Equality of approximation-number sequences implies equality of all Ky Fan gauges.