Documentation

TauCeti.Analysis.InnerProductSpace.UnitarilyInvariantSeminorm.Schatten

The Schatten seminorms #

For 1 ≤ p ≤ ∞ and a linear map A : E →ₗ[𝕜] F between finite-dimensional inner product spaces, the Schatten p-seminorm ‖A‖_p is the ℓᵖ norm of the singular values of A: ‖A‖_p = (∑ᵢ σᵢ(A)ᵖ)^(1/p) for finite p, and ‖A‖_∞ = maxᵢ σᵢ(A). The ℓᵖ norm on real tuples is a symmetric gauge (Seminorm.isSymmetricGauge_piLp), so the Schatten seminorm is the unitarily invariant seminorm attached to this gauge by TauCeti.UnitarilyInvariantSeminorm.ofIsSymmetricGauge. In particular its triangle inequality, ‖A + B‖_p ≤ ‖A‖_p + ‖B‖_p, comes from the weak majorization σ(A + B) ≺w σ(A) + σ(B) and is part of the seminorm structure.

The Schatten seminorm vanishes only at 0, dominates the operator norm, is invariant under taking adjoints, and satisfies the ideal inequalities ‖C A‖_p ≤ ‖C‖ ‖A‖_p and ‖A C‖_p ≤ ‖A‖_p ‖C‖ for rectangular factors C. Its endpoints are the nuclear seminorm (p = 1), the Frobenius seminorm (p = 2) and the operator norm (p = ∞).

Main declarations #

References #

source
noncomputable def TauCeti.UnitarilyInvariantSeminorm.schatten (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (p : ENNReal) [Fact (1 ≤ p)] :
UnitarilyInvariantSeminorm 𝕜 E F

The Schatten p-seminorm ‖A‖_p, the ℓᵖ norm of the singular values of A, as a unitarily invariant seminorm: ‖A‖_p = (∑ᵢ σᵢ(A)ᵖ)^(1/p) for finite p (TauCeti.UnitarilyInvariantSeminorm.schatten_apply_of_ne_top) and ‖A‖_∞ = σ₀(A) is the operator norm (TauCeti.UnitarilyInvariantSeminorm.schatten_top).

Instances For
    source
    theorem TauCeti.UnitarilyInvariantSeminorm.schatten_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (p : ENNReal) [Fact (1 ≤ p)] (A : E →ₗ[𝕜] F) :
    (schatten 𝕜 E F p) A = ‖WithLp.toLp p fun (i : Fin (Module.finrank 𝕜 E)) => A.singularValues ↑i‖

    The Schatten p-seminorm of A is the ℓᵖ norm of the tuple (σ₀(A), …, σₙ₋₁(A)) of its singular values, where n = dim E.

    source
    theorem TauCeti.UnitarilyInvariantSeminorm.schatten_apply_of_ne_top {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (p : ENNReal) [Fact (1 ≤ p)] (hp : p ≠ ⊤) (A : E →ₗ[𝕜] F) :
    (schatten 𝕜 E F p) A = (A.singularValues.sum fun (x : ℕ) (s : ℝ) => s ^ p.toReal) ^ (1 / p.toReal)

    For finite p, the Schatten p-seminorm is ‖A‖_p = (∑ᵢ σᵢ(A)ᵖ)^(1/p).

    source
    theorem TauCeti.UnitarilyInvariantSeminorm.opNorm_apply_le_schatten_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (p : ENNReal) [Fact (1 ≤ p)] (A : E →ₗ[𝕜] F) :
    (opNorm 𝕜 E F) A ≤ (schatten 𝕜 E F p) A

    The Schatten seminorms dominate the operator norm: ‖A‖ ≤ ‖A‖_p.

    source
    @[simp]
    theorem TauCeti.UnitarilyInvariantSeminorm.schatten_apply_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (p : ENNReal) [Fact (1 ≤ p)] {A : E →ₗ[𝕜] F} :
    (schatten 𝕜 E F p) A = 0 ↔ A = 0

    The Schatten seminorms are norms: ‖A‖_p = 0 only for A = 0.

    Endpoints #

    source
    @[simp]
    theorem TauCeti.UnitarilyInvariantSeminorm.schatten_one {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] :
    schatten 𝕜 E F 1 = nuclear 𝕜 E F

    At p = 1, the Schatten seminorm is the nuclear seminorm ∑ᵢ σᵢ(A).

    source
    @[simp]
    theorem TauCeti.UnitarilyInvariantSeminorm.schatten_two {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] :
    schatten 𝕜 E F 2 = frobenius 𝕜 E F

    At p = 2, the Schatten seminorm is the Frobenius seminorm √(∑ᵢ σᵢ(A)²).

    source
    @[simp]
    theorem TauCeti.UnitarilyInvariantSeminorm.schatten_top {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] :
    schatten 𝕜 E F ⊤ = opNorm 𝕜 E F

    At p = ∞, the Schatten seminorm is the operator norm σ₀(A).

    Adjoints and ideal inequalities #

    source
    @[simp]
    theorem TauCeti.UnitarilyInvariantSeminorm.compAdjoint_schatten {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (p : ENNReal) [Fact (1 ≤ p)] :
    (schatten 𝕜 E F p).compAdjoint = schatten 𝕜 F E p

    The adjoint transport of the Schatten p-seminorm on E →ₗ[𝕜] F is the Schatten p-seminorm on F →ₗ[𝕜] E.

    source
    @[simp]
    theorem TauCeti.UnitarilyInvariantSeminorm.schatten_apply_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (p : ENNReal) [Fact (1 ≤ p)] (A : E →ₗ[𝕜] F) :
    (schatten 𝕜 F E p) (LinearMap.adjoint A) = (schatten 𝕜 E F p) A

    The Schatten seminorms are invariant under taking adjoints: ‖A†‖_p = ‖A‖_p.

    source
    theorem TauCeti.UnitarilyInvariantSeminorm.schatten_comp_le_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (p : ENNReal) [Fact (1 ≤ p)] {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 G] (C : F →ₗ[𝕜] G) (A : E →ₗ[𝕜] F) {c : ℝ} (hC : ∀ (y : F), ‖C y‖ ≤ c * ‖y‖) :
    (schatten 𝕜 E G p) (C ∘ₗ A) ≤ c * (schatten 𝕜 E F p) A

    Ideal inequality, left factor. If ‖C y‖ ≤ c * ‖y‖ for every y (for c ≥ 0: if C has operator norm at most c), then ‖C A‖_p ≤ c * ‖A‖_p. The factor C : F →ₗ[𝕜] G may change the target space.

    source
    theorem TauCeti.UnitarilyInvariantSeminorm.schatten_comp_le_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (p : ENNReal) [Fact (1 ≤ p)] {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 G] (A : E →ₗ[𝕜] F) (C : G →ₗ[𝕜] E) {c : ℝ} (hc : 0 ≤ c) (hC : ∀ (x : G), ‖C x‖ ≤ c * ‖x‖) :
    (schatten 𝕜 G F p) (A ∘ₗ C) ≤ c * (schatten 𝕜 E F p) A

    Ideal inequality, right factor. If 0 ≤ c and ‖C x‖ ≤ c * ‖x‖ for every x, then ‖A C‖_p ≤ c * ‖A‖_p. The factor C : G →ₗ[𝕜] E may change the source space; the sign condition on c cannot be dropped, since for G = 0 every c bounds C.

    source
    theorem TauCeti.UnitarilyInvariantSeminorm.schatten_comp_comp_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (p : ENNReal) [Fact (1 ≤ p)] {G : Type u_4} {H : Type u_5} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [FiniteDimensional 𝕜 H] (C : F →ₗ[𝕜] G) (A : E →ₗ[𝕜] F) (D : H →ₗ[𝕜] E) {c d : ℝ} (hC : ∀ (y : F), ‖C y‖ ≤ c * ‖y‖) (hd : 0 ≤ d) (hD : ∀ (x : H), ‖D x‖ ≤ d * ‖x‖) :
    (schatten 𝕜 H G p) (C ∘ₗ A ∘ₗ D) ≤ c * d * (schatten 𝕜 E F p) A

    Two-sided ideal inequality. If ‖C y‖ ≤ c * ‖y‖ for every y, and 0 ≤ d and ‖D x‖ ≤ d * ‖x‖ for every x, then ‖C A D‖_p ≤ c * d * ‖A‖_p.