Unitarily invariant seminorms on rectangular linear maps

A seminorm N on the linear maps E →ₗ[𝕜] F between two inner product spaces is unitarily invariant when N (U A V) = N A for all unitaries U of F and V of E, acting independently on the target and the source. Square operators are the case E = F. Unitaries are represented as linear isometric equivalences F ≃ₗᵢ[𝕜] F and E ≃ₗᵢ[𝕜] E. The structure itself assumes neither finite-dimensionality nor boundedness: it is a seminorm on all algebraic linear maps E →ₗ[𝕜] F.

When E and F are finite-dimensional, the operator norm, the Frobenius norm, the Ky Fan norms and the nuclear norm are the standard examples; they are constructed in the neighbouring files OpNorm, Frobenius and KyFan of this directory.

This file sets up the structure together with the elementary vocabulary for comparing its values:

• the two-sided unitary orbit U C V of a map C, on which every unitarily invariant seminorm is constant; when E and F are finite-dimensional, the orbit of C consists exactly of the maps with the same singular values as C, so a unitarily invariant seminorm depends only on the singular values of its argument;
• the convex hull of the two-sided unitary orbit, on which every unitarily invariant seminorm is bounded by its value at C;
• finite orbit certificates, which write X as a combination ∑ᵢ aᵢ • Uᵢ C Vᵢ of points of the orbit of C, and bound N X by the coefficient mass ∑ᵢ ‖aᵢ‖ times N C;
• transport of a unitarily invariant seminorm along isometric isomorphisms of the source and the target, and, for finite-dimensional E and F, to the adjoint maps;
• invariance under replacing an endomorphism A by its operator modulus |A| = √(A† A), which has the same singular values as A.

Main declarations

• TauCeti.UnitarilyInvariantSeminorm: seminorms on E →ₗ[𝕜] F invariant under unitaries of the source and of the target.
• LinearMap.twoSidedUnitaryOrbit: the set of maps U C V with U, V unitary.
• LinearMap.mem_twoSidedUnitaryOrbit_iff_singularValues_eq: two maps lie in the same orbit exactly when they have the same singular values.
• TauCeti.UnitarilyInvariantSeminorm.map_eq_of_singularValues_eq: a unitarily invariant seminorm is determined by the singular values of its argument.
• LinearMap.twoSidedUnitaryOrbitHull: the convex combinations of points of the orbit; LinearMap.twoSidedUnitaryOrbitHull_eq_convexHull identifies it with convexHull ℝ of the orbit whenever the latter makes sense.
• LinearMap.twoSidedUnitaryOrbitHull_subset: the orbit hull is the smallest set containing the orbit and closed under convex combinations.
• TauCeti.UnitaryOrbitCertificate: a representation X = ∑ᵢ aᵢ • Uᵢ C Vᵢ, with its coefficient mass TauCeti.UnitaryOrbitCertificate.mass.
• TauCeti.UnitaryOrbitCertificate.apply_le_mass_mul: N X ≤ mass * N C.
• TauCeti.UnitaryOrbitCertificate.exists_mass_eq_one_of_mem_twoSidedUnitaryOrbitHull: points of the orbit hull have certificates of mass one, so TauCeti.UnitarilyInvariantSeminorm.map_le_of_mem_twoSidedUnitaryOrbitHull: N X ≤ N C on the hull.
• TauCeti.UnitarilyInvariantSeminorm.arrowCongr: transport along isometric isomorphisms of the source and the target.
• TauCeti.UnitarilyInvariantSeminorm.compAdjoint: the seminorm B ↦ N B† on the adjoint maps.
• TauCeti.UnitarilyInvariantSeminorm.map_operatorAbs: on endomorphisms, N |A| = N A for the operator modulus |A| = √(A† A).

Source

The structure UnitarilyInvariantSeminorm, the two-sided unitary orbit and the finite orbit certificates are adapted from the AIQ-Kitware DKPS formalization (ForTauCeti/Analysis/InnerProductSpace/UnitarilyInvariantSeminorm/Basic.lean). Original copyright (c) 2026 Kitware, Inc.; Apache-2.0.

References

• R. Bhatia, Matrix Analysis, Graduate Texts in Mathematics 169, Springer, 1997, Section IV.2.
• L. Mirsky, Symmetric gauge functions and unitarily invariant norms, Quart. J. Math. Oxford Ser. (2) 11 (1960), 50–59.

def LinearMap.twoSidedUnitaryOrbit {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (C : E →ₗ[𝕜] F) : Set (E →ₗ[𝕜] F)

The two-sided unitary orbit of C : E →ₗ[𝕜] F: the maps U ∘ C ∘ V for unitaries U of the target and V of the source.

theorem LinearMap.mem_twoSidedUnitaryOrbit {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {C X : E →ₗ[𝕜] F} : X ∈ C.twoSidedUnitaryOrbit ↔ ∃ (U : F ≃ₗᵢ[𝕜] F) (V : E ≃ₗᵢ[𝕜] E), ↑↑↑U ∘ₗ C ∘ₗ ↑↑↑V = X

theorem LinearMap.linearIsometryEquiv_comp_comp_mem_twoSidedUnitaryOrbit {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (C : E →ₗ[𝕜] F) (U : F ≃ₗᵢ[𝕜] F) (V : E ≃ₗᵢ[𝕜] E) : ↑↑↑U ∘ₗ C ∘ₗ ↑↑↑V ∈ C.twoSidedUnitaryOrbit

@[simp]

theorem LinearMap.self_mem_twoSidedUnitaryOrbit {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (C : E →ₗ[𝕜] F) : C ∈ C.twoSidedUnitaryOrbit

theorem LinearMap.twoSidedUnitaryOrbit_eq_of_mem {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {C X : E →ₗ[𝕜] F} (h : X ∈ C.twoSidedUnitaryOrbit) : X.twoSidedUnitaryOrbit = C.twoSidedUnitaryOrbit

Two-sided unitary orbits are equivalence classes: the orbit of any of its points is the whole orbit.

theorem LinearMap.singularValues_eq_of_mem_twoSidedUnitaryOrbit {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {C X : E →ₗ[𝕜] F} (h : X ∈ C.twoSidedUnitaryOrbit) : X.singularValues = C.singularValues

Maps in the same two-sided unitary orbit have the same singular values.

theorem LinearMap.mem_twoSidedUnitaryOrbit_iff_singularValues_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {C X : E →ₗ[𝕜] F} : X ∈ C.twoSidedUnitaryOrbit ↔ X.singularValues = C.singularValues

Determination of the orbit by singular values. Two maps between finite-dimensional inner product spaces lie in the same two-sided unitary orbit exactly when they have the same singular values.

The convex hull of the two-sided unitary orbit

def LinearMap.twoSidedUnitaryOrbitHull {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (C : E →ₗ[𝕜] F) : Set (E →ₗ[𝕜] F)

The convex hull of the two-sided unitary orbit of C: the convex combinations ∑ᵢ tᵢ • Xᵢ of maps Xᵢ in the two-sided unitary orbit of C, with real weights tᵢ ≥ 0 summing to 1. The weights act through ℝ → 𝕜: for a general RCLike field 𝕜 the space E →ₗ[𝕜] F carries no ℝ-module instance to which convexHull ℝ could be applied.

theorem LinearMap.mem_twoSidedUnitaryOrbitHull {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {C X : E →ₗ[𝕜] F} : X ∈ C.twoSidedUnitaryOrbitHull ↔ ∃ (n : ℕ) (t : Fin n → ℝ) (Y : Fin n → E →ₗ[𝕜] F), (∀ (i : Fin n), 0 ≤ t i) ∧ ∑ i : Fin n, t i = 1 ∧ (∀ (i : Fin n), Y i ∈ C.twoSidedUnitaryOrbit) ∧ ∑ i : Fin n, ↑(t i) • Y i = X

theorem LinearMap.twoSidedUnitaryOrbit_subset_twoSidedUnitaryOrbitHull {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (C : E →ₗ[𝕜] F) : C.twoSidedUnitaryOrbit ⊆ C.twoSidedUnitaryOrbitHull

@[simp]

theorem LinearMap.self_mem_twoSidedUnitaryOrbitHull {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (C : E →ₗ[𝕜] F) : C ∈ C.twoSidedUnitaryOrbitHull

theorem LinearMap.twoSidedUnitaryOrbitHull_eq_convexHull {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] (C : E →ₗ[𝕜] F) : C.twoSidedUnitaryOrbitHull = (convexHull ℝ) C.twoSidedUnitaryOrbit

When F is also a real vector space compatibly with its 𝕜-structure (for instance when 𝕜 is ℝ or ℂ), the orbit hull is the convex hull convexHull ℝ of the two-sided unitary orbit.

theorem LinearMap.twoSidedUnitaryOrbitHull_eq_of_mem {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {C X : E →ₗ[𝕜] F} (h : X ∈ C.twoSidedUnitaryOrbit) : X.twoSidedUnitaryOrbitHull = C.twoSidedUnitaryOrbitHull

The orbit hull depends only on the orbit: it is the same for every point of the orbit.

theorem LinearMap.smul_add_smul_mem_twoSidedUnitaryOrbitHull {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {C X Y : E →ₗ[𝕜] F} (hX : X ∈ C.twoSidedUnitaryOrbitHull) (hY : Y ∈ C.twoSidedUnitaryOrbitHull) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : ↑a • X + ↑b • Y ∈ C.twoSidedUnitaryOrbitHull

The orbit hull is convex: it is closed under convex combinations of two of its points.

theorem LinearMap.linearIsometryEquiv_comp_comp_mem_twoSidedUnitaryOrbitHull {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {C X : E →ₗ[𝕜] F} (h : X ∈ C.twoSidedUnitaryOrbitHull) (U : F ≃ₗᵢ[𝕜] F) (V : E ≃ₗᵢ[𝕜] E) : ↑↑↑U ∘ₗ X ∘ₗ ↑↑↑V ∈ C.twoSidedUnitaryOrbitHull

The orbit hull is invariant under unitaries of the source and of the target.

theorem LinearMap.twoSidedUnitaryOrbitHull_subset {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {C : E →ₗ[𝕜] F} {S : Set (E →ₗ[𝕜] F)} (hS : C.twoSidedUnitaryOrbit ⊆ S) (hconv : ∀ X ∈ S, ∀ Y ∈ S, ∀ (a b : ℝ), 0 ≤ a → 0 ≤ b → a + b = 1 → ↑a • X + ↑b • Y ∈ S) : C.twoSidedUnitaryOrbitHull ⊆ S

Minimality of the orbit hull. The orbit hull of C is contained in every set that contains the two-sided unitary orbit of C and is closed under convex combinations of two of its points.

theorem LinearMap.twoSidedUnitaryOrbitHull_subset_of_mem {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {C X : E →ₗ[𝕜] F} (h : X ∈ C.twoSidedUnitaryOrbitHull) : X.twoSidedUnitaryOrbitHull ⊆ C.twoSidedUnitaryOrbitHull

The orbit hull of a point of the orbit hull of C is contained in the orbit hull of C.

structure TauCeti.UnitarilyInvariantSeminorm (𝕜 : Type u_6) (E : Type u_7) (F : Type u_8) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] extends Seminorm 𝕜 (E →ₗ[𝕜] F) : Type (max u_7 u_8)

A unitarily invariant seminorm on the linear maps E →ₗ[𝕜] F: a seminorm N with N (U ∘ A ∘ V) = N A for every unitary U of the target F and every unitary V of the source E, acting independently. Square operators are the case E = F.

• toFun : (E →ₗ[𝕜] F) → ℝ
• map_zero' : self.toFun 0 = 0
• add_le' (r s : E →ₗ[𝕜] F) : self.toFun (r + s) ≤ self.toFun r + self.toFun s
• neg' (r : E →ₗ[𝕜] F) : self.toFun (-r) = self.toFun r
• smul' (a : 𝕜) (x : E →ₗ[𝕜] F) : self.toFun (a • x) = ‖a‖ * self.toFun x
• map_linearIsometryEquiv_comp_comp' (U : F ≃ₗᵢ[𝕜] F) (V : E ≃ₗᵢ[𝕜] E) (A : E →ₗ[𝕜] F) : self.toSeminorm (↑↑↑U ∘ₗ A ∘ₗ ↑↑↑V) = self.toSeminorm A

  Invariance under unitaries of the target and of the source.

@[instance_reducible]

instance TauCeti.UnitarilyInvariantSeminorm.instFunLikeLinearMapIdReal {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] : FunLike (UnitarilyInvariantSeminorm 𝕜 E F) (E →ₗ[𝕜] F) ℝ

instance TauCeti.UnitarilyInvariantSeminorm.instSeminormClassLinearMapId {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] : SeminormClass (UnitarilyInvariantSeminorm 𝕜 E F) 𝕜 (E →ₗ[𝕜] F)

theorem TauCeti.UnitarilyInvariantSeminorm.ext {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {N M : UnitarilyInvariantSeminorm 𝕜 E F} (h : ∀ (A : E →ₗ[𝕜] F), N A = M A) : N = M

theorem TauCeti.UnitarilyInvariantSeminorm.ext_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {N M : UnitarilyInvariantSeminorm 𝕜 E F} : N = M ↔ ∀ (A : E →ₗ[𝕜] F), N A = M A

@[simp]

theorem TauCeti.UnitarilyInvariantSeminorm.coe_toSeminorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (N : UnitarilyInvariantSeminorm 𝕜 E F) : ⇑N.toSeminorm = ⇑N

theorem TauCeti.UnitarilyInvariantSeminorm.map_linearIsometryEquiv_comp_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (N : UnitarilyInvariantSeminorm 𝕜 E F) (U : F ≃ₗᵢ[𝕜] F) (V : E ≃ₗᵢ[𝕜] E) (A : E →ₗ[𝕜] F) : N (↑↑↑U ∘ₗ A ∘ₗ ↑↑↑V) = N A

Unitary invariance: N (U ∘ A ∘ V) = N A for unitaries U of the target and V of the source.

@[simp]

theorem TauCeti.UnitarilyInvariantSeminorm.map_linearIsometryEquiv_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (N : UnitarilyInvariantSeminorm 𝕜 E F) (U : F ≃ₗᵢ[𝕜] F) (A : E →ₗ[𝕜] F) : N (↑↑↑U ∘ₗ A) = N A

@[simp]

theorem TauCeti.UnitarilyInvariantSeminorm.map_comp_linearIsometryEquiv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (N : UnitarilyInvariantSeminorm 𝕜 E F) (V : E ≃ₗᵢ[𝕜] E) (A : E →ₗ[𝕜] F) : N (A ∘ₗ ↑↑↑V) = N A

theorem TauCeti.UnitarilyInvariantSeminorm.map_eq_of_mem_twoSidedUnitaryOrbit {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (N : UnitarilyInvariantSeminorm 𝕜 E F) {C X : E →ₗ[𝕜] F} (h : X ∈ C.twoSidedUnitaryOrbit) : N X = N C

A unitarily invariant seminorm is constant on each two-sided unitary orbit.

theorem TauCeti.UnitarilyInvariantSeminorm.map_eq_of_singularValues_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (N : UnitarilyInvariantSeminorm 𝕜 E F) [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {A B : E →ₗ[𝕜] F} (h : A.singularValues = B.singularValues) : N A = N B

Determination by singular values. On maps between finite-dimensional inner product spaces, a unitarily invariant seminorm takes equal values at maps with the same singular values.

Transport along isometric isomorphisms

noncomputable def TauCeti.UnitarilyInvariantSeminorm.arrowCongr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {E' : Type u_4} {F' : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [NormedAddCommGroup F'] [InnerProductSpace 𝕜 F'] (eE : E ≃ₗᵢ[𝕜] E') (eF : F ≃ₗᵢ[𝕜] F') : UnitarilyInvariantSeminorm 𝕜 E F ≃ UnitarilyInvariantSeminorm 𝕜 E' F'

Transport of unitarily invariant seminorms along isometric isomorphisms eE : E ≃ E' of the sources and eF : F ≃ F' of the targets: N corresponds to the seminorm A ↦ N (eF⁻¹ ∘ A ∘ eE) on E' →ₗ[𝕜] F', which is again unitarily invariant.

@[simp]

theorem TauCeti.UnitarilyInvariantSeminorm.arrowCongr_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {E' : Type u_4} {F' : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [NormedAddCommGroup F'] [InnerProductSpace 𝕜 F'] (N : UnitarilyInvariantSeminorm 𝕜 E F) (eE : E ≃ₗᵢ[𝕜] E') (eF : F ≃ₗᵢ[𝕜] F') (A : E' →ₗ[𝕜] F') : ((arrowCongr eE eF) N) A = N (↑↑↑eF.symm ∘ₗ A ∘ₗ ↑↑↑eE)

@[simp]

theorem TauCeti.UnitarilyInvariantSeminorm.arrowCongr_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {E' : Type u_4} {F' : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [NormedAddCommGroup F'] [InnerProductSpace 𝕜 F'] (eE : E ≃ₗᵢ[𝕜] E') (eF : F ≃ₗᵢ[𝕜] F') : (arrowCongr eE eF).symm = arrowCongr eE.symm eF.symm

@[simp]

theorem TauCeti.UnitarilyInvariantSeminorm.arrowCongr_eq_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (N : UnitarilyInvariantSeminorm 𝕜 E F) (U : E ≃ₗᵢ[𝕜] E) (V : F ≃ₗᵢ[𝕜] F) : (arrowCongr U V) N = N

Transport along unitaries of the source and the target leaves every unitarily invariant seminorm unchanged.

Transport to the adjoint maps

noncomputable def TauCeti.UnitarilyInvariantSeminorm.compAdjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (N : UnitarilyInvariantSeminorm 𝕜 E F) [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] : UnitarilyInvariantSeminorm 𝕜 F E

The adjoint transport of a unitarily invariant seminorm N on E →ₗ[𝕜] F: the seminorm B ↦ N B† on F →ₗ[𝕜] E, again unitarily invariant.

@[simp]

theorem TauCeti.UnitarilyInvariantSeminorm.compAdjoint_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (N : UnitarilyInvariantSeminorm 𝕜 E F) [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (B : F →ₗ[𝕜] E) : N.compAdjoint B = N (LinearMap.adjoint B)

@[simp]

theorem TauCeti.UnitarilyInvariantSeminorm.compAdjoint_compAdjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (N : UnitarilyInvariantSeminorm 𝕜 E F) [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] : N.compAdjoint.compAdjoint = N

The operator modulus

@[simp]

theorem TauCeti.UnitarilyInvariantSeminorm.map_operatorAbs {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (N : UnitarilyInvariantSeminorm 𝕜 E E) (A : E →ₗ[𝕜] E) : N A.operatorAbs = N A

Modulus invariance. A unitarily invariant seminorm on the endomorphisms of a finite-dimensional inner product space takes the same value at an endomorphism A and at its modulus |A| = √(A† A).

Finite orbit certificates

structure TauCeti.UnitaryOrbitCertificate {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (ι : Type u_6) [Fintype ι] (C X : E →ₗ[𝕜] F) : Type (max (max (max u_1 u_2) u_3) u_6)

A finite unitary orbit certificate for X over C, indexed by a finite type ι: a representation X = ∑ᵢ aᵢ • Uᵢ ∘ C ∘ Vᵢ of X as a linear combination of points of the two-sided unitary orbit of C. Its coefficient mass ∑ᵢ ‖aᵢ‖ bounds every unitarily invariant seminorm of X by the same seminorm of C (TauCeti.UnitaryOrbitCertificate.apply_le_mass_mul).

• coeff : ι → 𝕜

  The coefficients aᵢ.

• left : ι → F ≃ₗᵢ[𝕜] F

  The unitaries Uᵢ of the target.

• right : ι → E ≃ₗᵢ[𝕜] E

  The unitaries Vᵢ of the source.

• sum_smul_comp_comp_eq : ∑ i : ι, self.coeff i • ↑↑↑(self.left i) ∘ₗ C ∘ₗ ↑↑↑(self.right i) = X

  The representation ∑ᵢ aᵢ • Uᵢ ∘ C ∘ Vᵢ = X.

theorem TauCeti.UnitaryOrbitCertificate.ext {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {inst✝ : RCLike 𝕜} {inst✝¹ : NormedAddCommGroup E} {inst✝² : InnerProductSpace 𝕜 E} {inst✝³ : NormedAddCommGroup F} {inst✝⁴ : InnerProductSpace 𝕜 F} {ι : Type u_6} {inst✝⁵ : Fintype ι} {C X : E →ₗ[𝕜] F} {x y : UnitaryOrbitCertificate ι C X} (coeff : x.coeff = y.coeff) (left : x.left = y.left) (right : x.right = y.right) : x = y

theorem TauCeti.UnitaryOrbitCertificate.ext_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {inst✝ : RCLike 𝕜} {inst✝¹ : NormedAddCommGroup E} {inst✝² : InnerProductSpace 𝕜 E} {inst✝³ : NormedAddCommGroup F} {inst✝⁴ : InnerProductSpace 𝕜 F} {ι : Type u_6} {inst✝⁵ : Fintype ι} {C X : E →ₗ[𝕜] F} {x y : UnitaryOrbitCertificate ι C X} : x = y ↔ x.coeff = y.coeff ∧ x.left = y.left ∧ x.right = y.right

noncomputable def TauCeti.UnitaryOrbitCertificate.mass {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_6} [Fintype ι] {C X : E →ₗ[𝕜] F} (c : UnitaryOrbitCertificate ι C X) : ℝ

The coefficient mass ∑ᵢ ‖aᵢ‖ of an orbit certificate.

theorem TauCeti.UnitaryOrbitCertificate.mass_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_6} [Fintype ι] {C X : E →ₗ[𝕜] F} (c : UnitaryOrbitCertificate ι C X) : c.mass = ∑ i : ι, ‖c.coeff i‖

theorem TauCeti.UnitaryOrbitCertificate.mass_nonneg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_6} [Fintype ι] {C X : E →ₗ[𝕜] F} (c : UnitaryOrbitCertificate ι C X) : 0 ≤ c.mass

theorem TauCeti.UnitaryOrbitCertificate.apply_le_mass_mul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_6} [Fintype ι] {C X : E →ₗ[𝕜] F} (c : UnitaryOrbitCertificate ι C X) (N : UnitarilyInvariantSeminorm 𝕜 E F) : N X ≤ c.mass * N C

Certificate bound: if X has an orbit certificate over C of mass m, then N X ≤ m * N C for every unitarily invariant seminorm N.

def TauCeti.UnitaryOrbitCertificate.reindex {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_6} {κ : Type u_7} [Fintype ι] [Fintype κ] {C X : E →ₗ[𝕜] F} (c : UnitaryOrbitCertificate ι C X) (e : ι ≃ κ) : UnitaryOrbitCertificate κ C X

Reindexing an orbit certificate along an equivalence of its finite index types.

@[simp]

theorem TauCeti.UnitaryOrbitCertificate.coeff_reindex {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_6} {κ : Type u_7} [Fintype ι] [Fintype κ] {C X : E →ₗ[𝕜] F} (c : UnitaryOrbitCertificate ι C X) (e : ι ≃ κ) (k : κ) : (c.reindex e).coeff k = c.coeff (e.symm k)

@[simp]

theorem TauCeti.UnitaryOrbitCertificate.left_reindex {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_6} {κ : Type u_7} [Fintype ι] [Fintype κ] {C X : E →ₗ[𝕜] F} (c : UnitaryOrbitCertificate ι C X) (e : ι ≃ κ) (k : κ) : (c.reindex e).left k = c.left (e.symm k)

@[simp]

theorem TauCeti.UnitaryOrbitCertificate.right_reindex {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_6} {κ : Type u_7} [Fintype ι] [Fintype κ] {C X : E →ₗ[𝕜] F} (c : UnitaryOrbitCertificate ι C X) (e : ι ≃ κ) (k : κ) : (c.reindex e).right k = c.right (e.symm k)

@[simp]

theorem TauCeti.UnitaryOrbitCertificate.mass_reindex {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_6} {κ : Type u_7} [Fintype ι] [Fintype κ] {C X : E →ₗ[𝕜] F} (c : UnitaryOrbitCertificate ι C X) (e : ι ≃ κ) : (c.reindex e).mass = c.mass

theorem TauCeti.UnitaryOrbitCertificate.exists_mass_eq_one_of_mem_twoSidedUnitaryOrbitHull {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {C X : E →ₗ[𝕜] F} (h : X ∈ C.twoSidedUnitaryOrbitHull) : ∃ (n : ℕ) (c : UnitaryOrbitCertificate (Fin n) C X), c.mass = 1

Certificates from convex combinations. Every point X = ∑ᵢ tᵢ • Uᵢ C Vᵢ of the convex hull of the two-sided unitary orbit of C has an orbit certificate over C of mass one.

theorem TauCeti.UnitarilyInvariantSeminorm.map_le_of_mem_twoSidedUnitaryOrbitHull {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (N : UnitarilyInvariantSeminorm 𝕜 E F) {C X : E →ₗ[𝕜] F} (h : X ∈ C.twoSidedUnitaryOrbitHull) : N X ≤ N C

A unitarily invariant seminorm is bounded on the convex hull of the two-sided unitary orbit of C by its value at C.