The gauge representation of unitarily invariant seminorms

With p = min (dim E) (dim F), the gauge g = N.gauge of a unitarily invariant seminorm N on E →ₗ[𝕜] F sends x : Fin p → ℝ to N (∑ᵢ xᵢ wᵢ ⊗ vᵢ) for any orthonormal families (vᵢ) in E and (wᵢ) in F; the choice of the families does not matter because diagonal sums with the same coefficients lie in one two-sided unitary orbit. Permuting the coordinates of x or changing their signs permutes the vectors or changes their signs, so g is a symmetric gauge: a seminorm on p-tuples invariant under permuting coordinates and changing their signs. The singular value decomposition of A then reads N A = g (σ₀(A), …, σₚ₋₁(A)), the gauge representation of von Neumann and Mirsky.

Conversely, every symmetric gauge g on p-tuples defines the unitarily invariant seminorm A ↦ g (σ₀(A), …, σₚ₋₁(A)), whose subadditivity is the weak majorization σ(A + B) ≺w σ(A) + σ(B), and the two constructions are mutually inverse.

Main results

• TauCeti.UnitarilyInvariantSeminorm.gauge: the symmetric gauge of a unitarily invariant seminorm, with TauCeti.UnitarilyInvariantSeminorm.isSymmetricGauge_gauge.
• TauCeti.UnitarilyInvariantSeminorm.map_eq_gauge_singularValues: the gauge representation N A = N.gauge (σ₀(A), …, σₚ₋₁(A)); exists_isSymmetricGauge_forall_map_eq restates it for square operators with tuples of length dim E.
• TauCeti.UnitarilyInvariantSeminorm.ofIsSymmetricGauge: the unitarily invariant seminorm of a symmetric gauge; ofIsSymmetricGauge_gauge and gauge_ofIsSymmetricGauge show that the two constructions are mutually inverse.

References

• R. Bhatia, Matrix Analysis, Graduate Texts in Mathematics 169, Springer, 1997, Theorem IV.2.1.
• J. von Neumann, Some matrix-inequalities and metrization of matric-space, Tomsk Univ. Rev. 1 (1937), 286–300.
• L. Mirsky, Symmetric gauge functions and unitarily invariant norms, Quart. J. Math. Oxford Ser. (2) 11 (1960), 50–59.

noncomputable def TauCeti.UnitarilyInvariantSeminorm.gauge {𝕜 : 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 : UnitarilyInvariantSeminorm 𝕜 E F) : Seminorm ℝ (Fin (min (Module.finrank 𝕜 E) (Module.finrank 𝕜 F)) → ℝ)

The symmetric gauge of a unitarily invariant seminorm N on E →ₗ[𝕜] F: with p = min (dim E) (dim F), its value at x : Fin p → ℝ is N (∑ᵢ xᵢ wᵢ ⊗ vᵢ) for orthonormal families (vᵢ) in E and (wᵢ) in F, which does not depend on the choice of the families (TauCeti.UnitarilyInvariantSeminorm.gauge_apply). It is a symmetric gauge (TauCeti.UnitarilyInvariantSeminorm.isSymmetricGauge_gauge), and N A is its value at the singular values of A (TauCeti.UnitarilyInvariantSeminorm.map_eq_gauge_singularValues).

theorem TauCeti.UnitarilyInvariantSeminorm.gauge_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] (N : UnitarilyInvariantSeminorm 𝕜 E F) {v : Fin (min (Module.finrank 𝕜 E) (Module.finrank 𝕜 F)) → E} {w : Fin (min (Module.finrank 𝕜 E) (Module.finrank 𝕜 F)) → F} (hv : Orthonormal 𝕜 v) (hw : Orthonormal 𝕜 w) (x : Fin (min (Module.finrank 𝕜 E) (Module.finrank 𝕜 F)) → ℝ) : N.gauge x = N (∑ i : Fin (min (Module.finrank 𝕜 E) (Module.finrank 𝕜 F)), ↑(x i) • ↑(((InnerProductSpace.rankOne 𝕜) (w i)) (v i)))

The gauge of N evaluated through arbitrary orthonormal families: with p = min (dim E) (dim F), N.gauge x = N (∑ᵢ xᵢ wᵢ ⊗ vᵢ) for all orthonormal families (vᵢ)_{i < p} in E and (wᵢ)_{i < p} in F.

theorem TauCeti.UnitarilyInvariantSeminorm.isSymmetricGauge_gauge {𝕜 : 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 : UnitarilyInvariantSeminorm 𝕜 E F) : N.gauge.IsSymmetricGauge

The gauge of a unitarily invariant seminorm is a symmetric gauge.

theorem TauCeti.UnitarilyInvariantSeminorm.map_eq_gauge_singularValues {𝕜 : 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 : UnitarilyInvariantSeminorm 𝕜 E F) (A : E →ₗ[𝕜] F) : N A = N.gauge fun (i : Fin (min (Module.finrank 𝕜 E) (Module.finrank 𝕜 F))) => A.singularValues ↑i

Gauge representation. Every unitarily invariant seminorm N on E →ₗ[𝕜] F is a symmetric gauge of the singular values: N A = g (σ₀(A), …, σₚ₋₁(A)) with p = min (dim E) (dim F) and g = N.gauge. For square operators p = dim E.

theorem TauCeti.UnitarilyInvariantSeminorm.exists_isSymmetricGauge_forall_map_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (N : UnitarilyInvariantSeminorm 𝕜 E E) : ∃ (g : Seminorm ℝ (Fin (Module.finrank 𝕜 E) → ℝ)), g.IsSymmetricGauge ∧ ∀ (A : E →ₗ[𝕜] E), N A = g fun (i : Fin (Module.finrank 𝕜 E)) => A.singularValues ↑i

Gauge representation for square operators. Every unitarily invariant seminorm N on the endomorphisms of E is a symmetric gauge of the dim E singular values of its argument. This is TauCeti.UnitarilyInvariantSeminorm.map_eq_gauge_singularValues with the gauge reindexed along min (dim E) (dim E) = dim E.

Unitarily invariant seminorms from symmetric gauges

noncomputable def TauCeti.UnitarilyInvariantSeminorm.ofIsSymmetricGauge {𝕜 : 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 : ℕ} (g : Seminorm ℝ (Fin n → ℝ)) (hg : g.IsSymmetricGauge) : UnitarilyInvariantSeminorm 𝕜 E F

The unitarily invariant seminorm A ↦ g (σ₀(A), …, σₙ₋₁(A)) of a symmetric gauge g on n-tuples. Subadditivity comes from the weak majorization σ(A + B) ≺w σ(A) + σ(B), along which symmetric gauges are monotone.

@[simp]

theorem TauCeti.UnitarilyInvariantSeminorm.ofIsSymmetricGauge_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] {n : ℕ} (g : Seminorm ℝ (Fin n → ℝ)) (hg : g.IsSymmetricGauge) (A : E →ₗ[𝕜] F) : (ofIsSymmetricGauge g hg) A = g fun (i : Fin n) => A.singularValues ↑i

@[simp]

theorem TauCeti.UnitarilyInvariantSeminorm.ofIsSymmetricGauge_gauge {𝕜 : 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 : UnitarilyInvariantSeminorm 𝕜 E F) : ofIsSymmetricGauge N.gauge ⋯ = N

A unitarily invariant seminorm is recovered from its gauge.

@[simp]

theorem TauCeti.UnitarilyInvariantSeminorm.gauge_ofIsSymmetricGauge {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (g : Seminorm ℝ (Fin (min (Module.finrank 𝕜 E) (Module.finrank 𝕜 F)) → ℝ)) (hg : g.IsSymmetricGauge) : (ofIsSymmetricGauge g hg).gauge = g

A symmetric gauge is recovered from its unitarily invariant seminorm: with p = min (dim E) (dim F), the gauge of A ↦ g (σ₀(A), …, σₚ₋₁(A)) is g. Together with TauCeti.UnitarilyInvariantSeminorm.ofIsSymmetricGauge_gauge, this makes N ↦ N.gauge a bijection between unitarily invariant seminorms on E →ₗ[𝕜] F and symmetric gauges on p-tuples.