Operator Ideal

Results named in Tau Ceti's TauCeti.Analysis.OperatorIdeal modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremEckart–Young for Ky Fan gauges#

Between finite-dimensional inner product spaces, the Ky Fan gauge Kₖ(T) of a bounded linear map is the Ky Fan k-sum σ₀(T) + ⋯ + σₖ₋₁(T) of its singular values.

ContinuousLinearMap.kyFanGauge_eq_kyFanSum.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F]
  [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (T : E →L[𝕜] F) (k : ℕ) :
  ↑(T.kyFanGauge k) = (↑T).kyFanSum k

Lean

Formalized in Tau Ceti as ContinuousLinearMap.kyFanGauge_eq_kyFanSum.

Other forms

Eckart–Young. Formalized in Tau Ceti as ContinuousLinearMap.singularValue_eq_linearMap_singularValues.

ContinuousLinearMap.singularValue_eq_linearMap_singularValues.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F]
  (T : E →L[𝕜] F) (n : ℕ) : ↑(T.singularValue n) = (↑T).singularValues n

Sources

• Tau Ceti documentation: ContinuousLinearMap.kyFanGauge_eq_kyFanSum
• Source of ContinuousLinearMap.kyFanGauge_eq_kyFanSum in TauCeti/Analysis/OperatorIdeal/ApproximationNumber/KyFan.lean

LeanContinuousLinearMap.kyFanGauge_eq_kyFanSum · ContinuousLinearMap.singularValue_eq_linearMap_singularValues

Uses 2 · Used by 4

Statement usesContinuousLinearMap.singularValue

Proof usesCourant–Fischer, lower direction

Used byThe singular-value Hoffman–Wielandt inequality · Ky Fan triangle inequality · Ky Fan's maximum principle · Weyl's perturbation bound for singular values

TheoremFatou inequality for the trace-class gauge#

For a series converging in operator norm, the gauge of its sum is at most the sum of the gauges, even when that sum is infinite.

ContinuousLinearMap.nuclearENorm_le_tsum_of_hasSum.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1}
  {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_4}
  {T : ι → E →L[𝕜] F} {S : E →L[𝕜] F} (hT : HasSum T S) :
  S.nuclearENorm ≤ ∑' (i : ι), (T i).nuclearENorm

Lean

Formalized in Tau Ceti as ContinuousLinearMap.nuclearENorm_le_tsum_of_hasSum.

Sources

• Tau Ceti documentation: ContinuousLinearMap.nuclearENorm_le_tsum_of_hasSum
• Source of ContinuousLinearMap.nuclearENorm_le_tsum_of_hasSum in TauCeti/Analysis/OperatorIdeal/Nuclear/Basic.lean

LeanContinuousLinearMap.nuclearENorm_le_tsum_of_hasSum

Uses 2

Statement usesContinuousLinearMap.singularValue

Proof usesKy Fan triangle inequality

TheoremKy Fan triangle inequality#

For bounded linear maps from a complete inner product space to an inner product space, the Ky Fan gauges are subadditive: Kₖ(S + T) ≤ Kₖ(S) + Kₖ(T).

ContinuousLinearMap.kyFanGauge_add_le.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3}
  [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F]
  [InnerProductSpace 𝕜 F] [CompleteSpace E] (S T : E →L[𝕜] F) (k : ℕ) :
  (S + T).kyFanGauge k ≤ S.kyFanGauge k + T.kyFanGauge k

Lean

Formalized in Tau Ceti as ContinuousLinearMap.kyFanGauge_add_le.

Other forms

Ky Fan triangle inequality from the converse min–max localization. Formalized in Tau Ceti as TauCeti.HasMinMaxLowerBound.kyFanGauge_add_le.

TauCeti.HasMinMaxLowerBound.kyFanGauge_add_le.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F]
  [InnerProductSpace 𝕜 F] (h : TauCeti.HasMinMaxLowerBound 𝕜 E F) (S T : E →L[𝕜] F) (k : ℕ) :
  (S + T).kyFanGauge k ≤ S.kyFanGauge k + T.kyFanGauge k

Sources

• Tau Ceti documentation: ContinuousLinearMap.kyFanGauge_add_le
• Source of ContinuousLinearMap.kyFanGauge_add_le in TauCeti/Analysis/OperatorIdeal/ApproximationNumber/KyFan.lean

LeanContinuousLinearMap.kyFanGauge_add_le · TauCeti.HasMinMaxLowerBound.kyFanGauge_add_le

Uses 3 · Used by 2

Statement usesContinuousLinearMap.singularValue

Proof usesEckart–Young for Ky Fan gauges · Ky Fan's maximum principle, attainment

Used byTauCeti.OperatorIdealFamily.traceClass · Fatou inequality for the trace-class gauge

TheoremKy Fan's maximum principle#

For a bounded linear map T between inner product spaces and orthonormal families (uᵢ) in F and (vᵢ) in E with k members, ‖∑ᵢ ⟪uᵢ, T vᵢ⟫‖ ≤ a₀(T) + ⋯ + aₖ₋₁(T).

ContinuousLinearMap.norm_sum_inner_le_kyFanGauge.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F]
  [InnerProductSpace 𝕜 F] {ι : Type u_4} [Fintype ι] (T : E →L[𝕜] F) {u : ι → F} {v : ι → E}
  (hu : Orthonormal 𝕜 u) (hv : Orthonormal 𝕜 v) :
  ‖∑ i, inner 𝕜 (u i) (T (v i))‖ ≤ ↑(T.kyFanGauge (Fintype.card ι))

Lean

Formalized in Tau Ceti as ContinuousLinearMap.norm_sum_inner_le_kyFanGauge.

Other forms

Ky Fan's maximum principle for positive operators, approximate attainment. Formalized in Tau Ceti as ContinuousLinearMap.IsPositive.exists_orthonormal_kyFanGauge_le_sum_re_inner_add.

ContinuousLinearMap.IsPositive.exists_orthonormal_kyFanGauge_le_sum_re_inner_add.{u_1, u_2}
  {𝕜 : 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, m ≤ k ∧ Orthonormal 𝕜 v ∧ ↑(T.kyFanGauge k) ≤ ∑ i, RCLike.re (inner 𝕜 (v i) (T (v i))) + ε

Ky Fan's maximum principle for positive operators. Formalized in Tau Ceti as ContinuousLinearMap.IsPositive.kyFanGauge_le_iff.

ContinuousLinearMap.IsPositive.kyFanGauge_le_iff.{u_1, u_2} {𝕜 : 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, RCLike.re (inner 𝕜 (v i) (T (v i))) ≤ c

Sources

• Tau Ceti documentation: ContinuousLinearMap.norm_sum_inner_le_kyFanGauge
• Source of ContinuousLinearMap.norm_sum_inner_le_kyFanGauge in TauCeti/Analysis/OperatorIdeal/ApproximationNumber/KyFan.lean

LeanContinuousLinearMap.norm_sum_inner_le_kyFanGauge · ContinuousLinearMap.IsPositive.exists_orthonormal_kyFanGauge_le_sum_re_inner_add · ContinuousLinearMap.IsPositive.kyFanGauge_le_iff

Uses 3

Statement usesContinuousLinearMap.singularValue

Proof usesEckart–Young for Ky Fan gauges · Ky Fan's maximum principle, attainment

TheoremWeyl's perturbation bound for singular values#

Each singular value of a linear map between finite-dimensional inner product spaces is 1-Lipschitz in the operator norm: |σₙ(A) - σₙ(B)| ≤ ‖A - B‖.

LinearMap.abs_singularValues_sub_singularValues_le.{u_1, u_2, u_3} {𝕜 : 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 : ℕ) :
  |A.singularValues n - B.singularValues n| ≤ ‖LinearMap.toContinuousLinearMap (A - B)‖

Lean

Formalized in Tau Ceti as LinearMap.abs_singularValues_sub_singularValues_le.

Sources

• Tau Ceti documentation: LinearMap.abs_singularValues_sub_singularValues_le
• Source of LinearMap.abs_singularValues_sub_singularValues_le in TauCeti/Analysis/OperatorIdeal/ApproximationNumber/EckartYoung.lean

LeanLinearMap.abs_singularValues_sub_singularValues_le

Uses 2

Proof usesContinuousLinearMap.singularValue · Eckart–Young for Ky Fan gauges

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.