Operator theory

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremPolar decomposition of a bounded operator#

U |T| = T.

ContinuousLinearMap.polarFactor_comp_modulus.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E]
  [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) :
  T.polarFactor ∘SL T.modulus = T
Lean

Formalized in Tau Ceti as ContinuousLinearMap.polarFactor_comp_modulus.

Sources
LeanContinuousLinearMap.polarFactor_comp_modulus
Uses 1
Proof usesTauCeti.Complexification

TheoremThe pairwise Sylvester bound#

Let A and B be symmetric operators on finite-dimensional inner product spaces. If every eigenvalue of A is at distance at least δ from every eigenvalue of B, then δ N(X) ≤ (π / 2) N(A X - X B) for every unitarily invariant seminorm N. In particular every solution of the Sylvester equation A X - X B = C satisfies δ N(X) ≤ (π / 2) N(C).

TauCeti.UnitarilyInvariantSeminorm.mul_map_le_pi_div_two_mul_map_sylvester_apply.{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 : E →L[𝕜] E} {B : F →L[𝕜] F} {δ : ℝ}
  (N : TauCeti.UnitarilyInvariantSeminorm 𝕜 F E) (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric)
  (h : Module.End.PointSpectraSeparated ↑A ⊤ ↑B ⊤ δ) (X : F →L[𝕜] E) :
  δ * N ↑X ≤ Real.pi / 2 * N ↑((A.sylvester B) X)
Lean

Formalized in Tau Ceti as TauCeti.UnitarilyInvariantSeminorm.mul_map_le_pi_div_two_mul_map_sylvester_apply.

Other forms

The pairwise Sylvester bound on invariant subspaces. Formalized in Tau Ceti as TauCeti.UnitarilyInvariantSeminorm.mul_map_le_pi_div_two_mul_map_sylvester_apply_of_mem.

TauCeti.UnitarilyInvariantSeminorm.mul_map_le_pi_div_two_mul_map_sylvester_apply_of_mem.{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 : E →L[𝕜] E} {B : F →L[𝕜] F} {δ : ℝ}
  (N : TauCeti.UnitarilyInvariantSeminorm 𝕜 F E) (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric)
  {S : Submodule 𝕜 E} {T : Submodule 𝕜 F} (hS : ∀ x ∈ S, A x ∈ S) (hT : ∀ y ∈ T, B y ∈ T)
  (h : Module.End.PointSpectraSeparated (↑A) S (↑B) T δ) {X : F →L[𝕜] E} (hXS : ∀ (y : F), X y ∈ S)
  (hXT : ∀ y ∈ Tᗮ, X y = 0) : δ * N ↑X ≤ Real.pi / 2 * N ↑((A.sylvester B) X)
Sources
LeanTauCeti.UnitarilyInvariantSeminorm.mul_map_le_pi_div_two_mul_map_sylvester_apply · TauCeti.UnitarilyInvariantSeminorm.mul_map_le_pi_div_two_mul_map_sylvester_apply_of_mem
Uses 3 · Used by 1
Proof usesCourant–Fischer, lower direction · Ky Fan's maximum principle, attainment · The simultaneous Ky Fan estimate for the Sylvester equation
Used byThe pairwise π / 2 Davis–Kahan sin Θ theorem

TheoremThe perturbation Davis–Kahan sin Θ theorem#

Let A and B be symmetric operators on a finite-dimensional inner product space, let U be invariant under A and V invariant under B. If the eigenvalues of A on U lie in [a, b] and those of B on Vᗮ lie outside (a - δ, b + δ), then the directed sine map P_{Vᗮ} P_U from U towards V satisfies δ N(P_{Vᗮ} P_U) ≤ N(B - A) for every unitarily invariant seminorm N.

TauCeti.UnitarilyInvariantSeminorm.mul_map_starProjection_comp_starProjection_le_map_sub.{u_1, u_2}
  {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] {a b δ : ℝ} (N : TauCeti.UnitarilyInvariantSeminorm 𝕜 E E)
  {A B : E →L[𝕜] E} (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric) {U V : Submodule 𝕜 E}
  (hU : ∀ x ∈ U, A x ∈ U) (hV : ∀ x ∈ V, B x ∈ V)
  (h : Module.End.PointIntervalExteriorGap (↑A) U (↑B) Vᗮ a b δ) :
  δ * N ↑(Vᗮ.starProjection ∘SL U.starProjection) ≤ N (↑B - ↑A)
Lean

Formalized in Tau Ceti as TauCeti.UnitarilyInvariantSeminorm.mul_map_starProjection_comp_starProjection_le_map_sub.

Other forms

The perturbation Davis–Kahan sin Θ theorem, reversed orientation. Formalized in Tau Ceti as TauCeti.UnitarilyInvariantSeminorm.mul_map_starProjection_comp_starProjection_le_map_sub_swap.

TauCeti.UnitarilyInvariantSeminorm.mul_map_starProjection_comp_starProjection_le_map_sub_swap.{u_1,
    u_2}
  {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] {a b δ : ℝ} (N : TauCeti.UnitarilyInvariantSeminorm 𝕜 E E)
  {A B : E →L[𝕜] E} (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric) {U V : Submodule 𝕜 E}
  (hU : ∀ x ∈ U, A x ∈ U) (hV : ∀ x ∈ V, B x ∈ V)
  (h : Module.End.PointIntervalExteriorGap (↑B) Vᗮ (↑A) U a b δ) :
  δ * N ↑(Vᗮ.starProjection ∘SL U.starProjection) ≤ N (↑B - ↑A)
Sources
LeanTauCeti.UnitarilyInvariantSeminorm.mul_map_starProjection_comp_starProjection_le_map_sub · TauCeti.UnitarilyInvariantSeminorm.mul_map_starProjection_comp_starProjection_le_map_sub_swap
Uses 3 · Used by 1
Proof usesCourant–Fischer, lower direction · Fan dominance · The interval/exterior Sylvester bound
Used byKy Fan perturbation sin Θ bound

TheoremFan dominance#

If every Ky Fan sum of A is at most the corresponding Ky Fan sum of C, then N A ≤ N C for every unitarily invariant seminorm N.

TauCeti.UnitarilyInvariantSeminorm.map_le_of_kyFanSum_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]
  (N : TauCeti.UnitarilyInvariantSeminorm 𝕜 E F) {A C : E →ₗ[𝕜] F}
  (h : ∀ (k : ℕ), A.kyFanSum k ≤ C.kyFanSum k) : N A ≤ N C
Lean

Formalized in Tau Ceti as TauCeti.UnitarilyInvariantSeminorm.map_le_of_kyFanSum_le.

Sources
LeanTauCeti.UnitarilyInvariantSeminorm.map_le_of_kyFanSum_le
Uses 2 · Used by 6
Proof usesCourant–Fischer, lower direction · Ky Fan's maximum principle, attainment
Used byThe perturbation Davis–Kahan sin Θ theorem · The residual Davis–Kahan sin Θ theorem · The Davis–Kahan sin 2Θ theorem · The interval/exterior Sylvester bound · The pairwise π / 2 Davis–Kahan sin Θ theorem · Sylvester bound from a disc and the exterior of a larger disc

TheoremThe Kato–Rellich theorem#

Let A be a self-adjoint partial linear map on a Hilbert space and V a symmetric partial linear map that is relatively bounded with respect to A with constants a and b < 1, that is dom A ⊆ dom V and ‖V x‖ ≤ a * ‖x‖ + b * ‖A x‖ on dom A. Then A + V, whose domain is dom A, is self-adjoint.

IsSelfAdjoint.add_of_isRelativelyBounded.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A V : E →ₗ.[𝕜] E}
  (hA : IsSelfAdjoint A) (hV : V.IsFormalAdjoint V) {a b : ℝ} (hAV : V.IsRelativelyBounded A a b)
  (hb : b < 1) : IsSelfAdjoint (A + V)
Lean

Formalized in Tau Ceti as IsSelfAdjoint.add_of_isRelativelyBounded.

Sources
LeanIsSelfAdjoint.add_of_isRelativelyBounded

StructureTauCeti.ProjValMeasure#

A projection-valued measure on the measurable sets of X, acting on a complex Hilbert space H.

The diagonal scalar measures diag ξ are supplied as finite measures, related to the projections by inner_proj. This follows the donor's carrier representation, in which the diagonal measures are uniquely determined by proj. Idempotence, self-adjointness, positivity, finite additivity, contraction, and strong countable additivity follow from these laws.

TauCeti.ProjValMeasure.{u_3, u_4} (X : Type u_3) [MeasurableSpace X] (H : Type u_4)
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : Type (max u_3 u_4)
Lean

Formalized in Tau Ceti as TauCeti.ProjValMeasure.

Sources
LeanTauCeti.ProjValMeasure
Used by 2
Used byTauCeti.ProjValMeasure.integral · Spectral theorem for normal operators

DefinitionTauCeti.ProjValMeasure.integral#

The integral of a bounded Borel symbol against a projection-valued measure P, P.integral f = ∫ f dP, as a unital star algebra homomorphism. It is characterised by integral_ofSimpleFunc on simple symbols and its continuity (continuous_integral); see eq_integral_of_continuous.

TauCeti.ProjValMeasure.integral.{u_1, u_2} {X : Type u_1} {H : Type u_2} [MeasurableSpace X]
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  (P : TauCeti.ProjValMeasure X H) : TauCeti.BoundedBorelFunction X →⋆ₐ[ℂ] H →L[ℂ] H
Lean

Formalized in Tau Ceti as TauCeti.ProjValMeasure.integral.

Sources
LeanTauCeti.ProjValMeasure.integral
Uses 1 · Used by 1
Statement usesTauCeti.ProjValMeasure
Used bySpectral theorem for normal operators

DefinitionTauCeti.OperatorIdealFamily.traceClass#

The trace-class operator-ideal family, whose gauge is the nuclear gauge ν(T) = ∑' n, aₙ(T): the extended sum of the approximation numbers.

TauCeti.OperatorIdealFamily.traceClass.{u, v, w} (𝕜 : Type u) [RCLike 𝕜] :
  TauCeti.OperatorIdealFamily 𝕜
Lean

Formalized in Tau Ceti as TauCeti.OperatorIdealFamily.traceClass.

Sources
LeanTauCeti.OperatorIdealFamily.traceClass
Uses 2
Statement usesContinuousLinearMap.singularValue
Proof usesKy Fan triangle inequality

DefinitionTauCeti.OperatorIdealFamily.hilbertSchmidt#

The Hilbert–Schmidt operator-ideal family. Its gauge is the square root E_b(T)^(1/2) of the Hilbert–Schmidt energy, computed in a Hilbert basis b of the source chosen once and for all; by gauge_hilbertSchmidt every Hilbert basis gives the same value.

TauCeti.OperatorIdealFamily.hilbertSchmidt.{u, v, w} (𝕜 : Type u) [RCLike 𝕜] :
  TauCeti.OperatorIdealFamily 𝕜
Lean

Formalized in Tau Ceti as TauCeti.OperatorIdealFamily.hilbertSchmidt.

Sources
LeanTauCeti.OperatorIdealFamily.hilbertSchmidt
Uses 2
Proof usesMinkowski's inequality for unconditional sums in ℝ≥0∞ · Parseval's identity for a functional

DefinitionContinuousLinearMap.singularValue#

The n-th approximation number aₙ(T) of a bounded linear map T: the infimum of the operator norms ‖T - R‖ over all bounded linear maps R of rank at most n. The indexing is zero-based, so a₀(T) = ‖T‖ (singularValue_zero).

On finite-dimensional Hilbert spaces these are the singular values of T.

ContinuousLinearMap.singularValue.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3}
  [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
  [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) : NNReal
Lean

Formalized in Tau Ceti as ContinuousLinearMap.singularValue.

Sources
LeanContinuousLinearMap.singularValue
Used by 8
Used byKy Fan two-sided ideal inequality · TauCeti.OperatorIdealFamily.traceClass · The singular-value Hoffman–Wielandt inequality · Eckart–Young for Ky Fan gauges · Fatou inequality for the trace-class gauge · Ky Fan triangle inequality · Ky Fan's maximum principle · Weyl's perturbation bound for singular values

TheoremThe exact mass of the Haagerup–Zsidó kernel#

∫_ℝ ‖k(t)‖ dt = π / 2.

TauCeti.HaagerupZsido.integral_norm_reciprocalKernel :
  ∫ (t : ℝ), ‖TauCeti.HaagerupZsido.reciprocalKernel t‖ = Real.pi / 2
Lean

Formalized in Tau Ceti as TauCeti.HaagerupZsido.integral_norm_reciprocalKernel.

Sources
LeanTauCeti.HaagerupZsido.integral_norm_reciprocalKernel

TheoremKy Fan two-sided ideal inequality#

Kₖ(A T B) ≤ ‖A‖ Kₖ(T) ‖B‖.

ContinuousLinearMap.kyFanGauge_comp_comp_le.{u_1, u_2, u_3, u_4, u_5} {𝕜 : 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]
  (A : G →L[𝕜] H) (T : F →L[𝕜] G) (B : E →L[𝕜] F) (k : ℕ) :
  (A ∘SL T ∘SL B).kyFanGauge k ≤ ‖A‖₊ * T.kyFanGauge k * ‖B‖₊
Lean

Formalized in Tau Ceti as ContinuousLinearMap.kyFanGauge_comp_comp_le.

Sources
LeanContinuousLinearMap.kyFanGauge_comp_comp_le
Uses 1
Statement usesContinuousLinearMap.singularValue

TheoremThe residual Davis–Kahan sin Θ theorem#

Let A and M be symmetric operators on finite-dimensional inner product spaces E and F, let U be invariant under A, and let X : F → E be linear. If the eigenvalues of M lie in [a, b] and those of A on Uᗮ lie outside (a - δ, b + δ), then δ N(P_{Uᗮ} X) ≤ N(A X - X M) for every unitarily invariant seminorm N.

TauCeti.UnitarilyInvariantSeminorm.mul_map_starProjection_comp_le_map_sylvester_apply.{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 δ : ℝ} (N : TauCeti.UnitarilyInvariantSeminorm 𝕜 F E) {A : E →L[𝕜] E}
  {M : F →L[𝕜] F} (hA : (↑A).IsSymmetric) (hM : (↑M).IsSymmetric) {U : Submodule 𝕜 E}
  (hU : ∀ x ∈ U, A x ∈ U) (h : Module.End.PointIntervalExteriorGap ↑M ⊤ (↑A) Uᗮ a b δ)
  (X : F →L[𝕜] E) : δ * N ↑(Uᗮ.starProjection ∘SL X) ≤ N ↑((A.sylvester M) X)
Lean

Formalized in Tau Ceti as TauCeti.UnitarilyInvariantSeminorm.mul_map_starProjection_comp_le_map_sylvester_apply.

Sources
LeanTauCeti.UnitarilyInvariantSeminorm.mul_map_starProjection_comp_le_map_sylvester_apply
Uses 3 · Used by 1
Proof usesCourant–Fischer, lower direction · Fan dominance · The interval/exterior Sylvester bound
Used byKy Fan residual sin Θ bound

TheoremThe simultaneous Ky Fan estimate for the Sylvester equation#

Let A and B be symmetric operators on finite-dimensional inner product spaces. If every eigenvalue of A is at distance at least δ from every eigenvalue of B, then for every k the Ky Fan k-sums satisfy δ Kₖ(X) ≤ (π / 2) Kₖ(A X - X B). In particular every solution of the Sylvester equation A X - X B = C satisfies δ Kₖ(X) ≤ (π / 2) Kₖ(C) for all k at once.

ContinuousLinearMap.mul_kyFanSum_le_pi_div_two_mul_kyFanSum_sylvester_apply.{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 : E →L[𝕜] E} {B : F →L[𝕜] F} {δ : ℝ} (hA : (↑A).IsSymmetric)
  (hB : (↑B).IsSymmetric) (h : Module.End.PointSpectraSeparated ↑A ⊤ ↑B ⊤ δ) (X : F →L[𝕜] E)
  (k : ℕ) : δ * (↑X).kyFanSum k ≤ Real.pi / 2 * (↑((A.sylvester B) X)).kyFanSum k
Lean

Formalized in Tau Ceti as ContinuousLinearMap.mul_kyFanSum_le_pi_div_two_mul_kyFanSum_sylvester_apply.

Sources
LeanContinuousLinearMap.mul_kyFanSum_le_pi_div_two_mul_kyFanSum_sylvester_apply
Uses 2 · Used by 1
Proof usesThe exterior reciprocal Fourier identity · Ky Fan's maximum principle, attainment
Used byThe pairwise Sylvester bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.