Unitarily invariant seminorms on rectangular linear maps

The structure extends Seminorm and adds invariance under independent unitary actions on its domain and codomain. This module supplies its function and seminorm instances, finite two-sided orbit certificates, singular-value invariance, and isometric transport.

Provenance

Adapted from the square and rectangular unitarily invariant seminorm modules in the Davis--Kahan/DKPS formalization (Kitware, Inc.). The finite orbit and isometric-transport proofs were originally part of the rectangular module.

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

A seminorm on rectangular linear maps, invariant under independent unitary changes of domain and codomain coordinates. Square operators use 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
• unitary_invariant' (U : ↥(unitary (F →ₗ[𝕜] F))) (V : ↥(unitary (E →ₗ[𝕜] E))) (A : E →ₗ[𝕜] F) : self.toFun (↑U ∘ₗ A ∘ₗ ↑V) = self.toFun A

  Two-sided unitary invariance. The left unitary acts on the codomain.

@[instance_reducible]

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

A unitarily invariant seminorm is a function on rectangular maps, injectively so: the seminorm laws and the invariance field are propositions.

Equations

• TauCeti.UnitarilyInvariantSeminorm.instFunLikeLinearMapIdReal = { coe := fun (N : TauCeti.UnitarilyInvariantSeminorm 𝕜 E F) => N.toFun, coe_injective := ⋯ }

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

The seminorm laws of the underlying Seminorm, transported to the coercion, so that the generic Seminorm API (apply_nonneg, map_neg_eq_map, …) applies directly.

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

Two unitarily invariant seminorms agreeing at every rectangular map are equal.

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

theorem TauCeti.UnitarilyInvariantSeminorm.unitary_invariant_of_isometry {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {f : (E →ₗ[𝕜] F) → ℝ} (h : ∀ (U : F ≃ₗᵢ[𝕜] F) (V : E ≃ₗᵢ[𝕜] E) (A : E →ₗ[𝕜] F), f (↑U.toLinearEquiv ∘ₗ A ∘ₗ ↑V.toLinearEquiv) = f A) (U : ↥(unitary (F →ₗ[𝕜] F))) (V : ↥(unitary (E →ₗ[𝕜] E))) (A : E →ₗ[𝕜] F) : f (↑U ∘ₗ A ∘ₗ ↑V) = f A

Prove the unitary field using the equivalent linear-isometry action. This changes only the representation of a unitary, not the seminorm.

@[simp]

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

A rectangular UI seminorm vanishes at zero.

theorem TauCeti.UnitarilyInvariantSeminorm.nonneg {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (N : UnitarilyInvariantSeminorm 𝕜 E F) (A : E →ₗ[𝕜] F) : 0 ≤ N A

A rectangular UI seminorm is nonnegative -- derived from the seminorm laws, not assumed as a field.

theorem TauCeti.UnitarilyInvariantSeminorm.add_le {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (N : UnitarilyInvariantSeminorm 𝕜 E F) (A B : E →ₗ[𝕜] F) : N (A + B) ≤ N A + N B

Subadditivity.

theorem TauCeti.UnitarilyInvariantSeminorm.sum_le {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (N : UnitarilyInvariantSeminorm 𝕜 E F) {ι : Type u_5} (s : Finset ι) (A : ι → E →ₗ[𝕜] F) : N (∑ i ∈ s, A i) ≤ ∑ i ∈ s, N (A i)

A rectangular UI seminorm of a finite sum is bounded by the sum of the individual seminorms.

This is the finite replacement for the integral triangle inequality in the unitary-orbit proof of the π/2 Sylvester theorem.

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

The two-sided unitary orbit of a rectangular map.

A point of twoSidedUnitaryOrbit C has the form U ∘ C ∘ V with unitary left and right factors. The phase of a complex Fourier coefficient is intended to be absorbed into U, so the convex hull of this set is the correct barycentric target for the arbitrary-spectrum π/2 proof.

The definition is field-uniform: over ℝ, the only scalar phases absorbed into the orbit are the real unitary signs, while a complex proof must descend to a real orbit before invoking this API.

Equations

• TauCeti.UnitarilyInvariantSeminorm.twoSidedUnitaryOrbit C = {Y : E →ₗ[𝕜] F | ∃ (U : F ≃ₗᵢ[𝕜] F) (V : E ≃ₗᵢ[𝕜] E), Y = ↑U.toLinearEquiv ∘ₗ C ∘ₗ ↑V.toLinearEquiv}

def TauCeti.UnitarilyInvariantSeminorm.HasFiniteUnitaryOrbitCertificate {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (mass : ℝ) (X C : E →ₗ[𝕜] F) : Prop

A finite two-sided unitary-orbit certificate for bounding X by C.

A certificate of mass mass writes X as a finite linear combination of maps Uᵢ ∘ C ∘ Vᵢ, where each Uᵢ and Vᵢ is unitary and the sum of coefficient norms is at most mass.

For the arbitrary-spectrum π/2 theorem, the difficult analytic task is exactly to construct such a certificate for ((δ : 𝕜) • X) from the Sylvester defect C with mass π / 2.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.UnitarilyInvariantSeminorm.hasFiniteUnitaryOrbitCertificate_of_fintype {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_5} [Fintype ι] {mass : ℝ} {X C : E →ₗ[𝕜] F} (a : ι → 𝕜) (U : ι → F ≃ₗᵢ[𝕜] F) (V : ι → E ≃ₗᵢ[𝕜] E) (hX : X = ∑ i : ι, a i • ↑(U i).toLinearEquiv ∘ₗ C ∘ₗ ↑(V i).toLinearEquiv) (hmass : ∑ i : ι, ‖a i‖ ≤ mass) : HasFiniteUnitaryOrbitCertificate mass X C

Reindex a finite certificate candidate from an arbitrary finite type by Fin n.

This lemma keeps all Fin n bookkeeping out of the convex-geometric proof. It is purely finite algebra and has no analytic or field-specific content.

@[instance_reducible]

def TauCeti.UnitarilyInvariantSeminorm.realModuleLinearMap {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] : Module ℝ (E →ₗ[𝕜] F)

Restrict scalars on the rectangular-map space from 𝕜 to ℝ for the real convex-hull argument.

Equations

• TauCeti.UnitarilyInvariantSeminorm.realModuleLinearMap = Module.compHom (E →ₗ[𝕜] F) (algebraMap ℝ 𝕜)

theorem TauCeti.UnitarilyInvariantSeminorm.hasFiniteUnitaryOrbitCertificate_of_smul_mem_convexHull {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {m mass : ℝ} (hm : 0 ≤ m) (hmass : m ≤ mass) {X Y C : E →ₗ[𝕜] F} (hY : Y ∈ (convexHull ℝ) (twoSidedUnitaryOrbit C)) (hX : X = ↑m • Y) : HasFiniteUnitaryOrbitCertificate mass X C

Convert an exact convex-hull barycentric representation into a finite unitary-orbit certificate.

Suppose Y lies in the real convex hull of the two-sided unitary orbit of C, and X = m • Y for a nonnegative real mass m ≤ mass. Then X has a finite unitary-orbit certificate of mass mass.

This theorem discharges the entire exact finite-dimensional convex-combination stage of the π/2 proof. The remaining analytic theorem only has to produce a bounded-mass barycentric orbit representation. The argument is valid over both ℝ and ℂ; any complexification/descent issue must already have been resolved before establishing the real convex-hull hypothesis.

theorem TauCeti.UnitarilyInvariantSeminorm.smul_eq {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (N : UnitarilyInvariantSeminorm 𝕜 E F) (a : 𝕜) (A : E →ₗ[𝕜] F) : N (a • A) = ‖a‖ * N A

Absolute homogeneity.

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

A rectangular UI seminorm is invariant under negation.

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

Two-sided unitary invariance, with U acting on the codomain and V on the domain. Note the argument order follows the composition U ∘ A ∘ V, not the alphabet.

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

Left unitary invariance.

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

Right unitary invariance.

theorem TauCeti.UnitarilyInvariantSeminorm.apply_le_of_finiteUnitaryOrbitCertificate {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (N : UnitarilyInvariantSeminorm 𝕜 E F) {mass : ℝ} {X C : E →ₗ[𝕜] F} (hcert : HasFiniteUnitaryOrbitCertificate mass X C) : N X ≤ mass * N C

Every rectangular UI seminorm is bounded by the mass of a finite two-sided unitary-orbit certificate.

This theorem deliberately contains all norm-theoretic content needed by the π/2 front. The remaining hard theorem may therefore focus solely on constructing the orbit certificate.

theorem TauCeti.UnitarilyInvariantSeminorm.exists_unitary_factorization_of_singularValues_eq {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {A B : E →ₗ[𝕜] F} (hσ : A.singularValues = B.singularValues) : ∃ (U : F ≃ₗᵢ[𝕜] F) (V : E ≃ₗᵢ[𝕜] E), A = ↑U.toLinearEquiv ∘ₗ B ∘ₗ ↑V.toLinearEquiv

Equal singular-value data determines a rectangular map up to left and right unitary factors. The right unitary aligns the two Gram eigenbases; Gram rigidity then supplies the left unitary.

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

A rectangular unitarily invariant norm depends only on the complete singular-value sequence.

noncomputable def TauCeti.UnitarilyInvariantSeminorm.codomainIsometryTransport {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [FiniteDimensional 𝕜 H] (N : UnitarilyInvariantSeminorm 𝕜 E F) (ι : H →ₗᵢ[𝕜] F) : UnitarilyInvariantSeminorm 𝕜 E H

Pull a rectangular UI norm back along an isometric embedding of the codomain. The transported norm measures A : E → H by measuring ι ∘ A : E → F.

Equations

• N.codomainIsometryTransport ι = { toSeminorm := Seminorm.of (fun (A : E →ₗ[𝕜] H) => N (ι.toLinearMap ∘ₗ A)) ⋯ ⋯, unitary_invariant' := ⋯ }

@[simp]

theorem TauCeti.UnitarilyInvariantSeminorm.codomainIsometryTransport_apply {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [FiniteDimensional 𝕜 H] (N : UnitarilyInvariantSeminorm 𝕜 E F) (ι : H →ₗᵢ[𝕜] F) (A : E →ₗ[𝕜] H) : (N.codomainIsometryTransport ι) A = N (ι.toLinearMap ∘ₗ A)

Codomain transport, unfolded.

noncomputable def TauCeti.UnitarilyInvariantSeminorm.domainIsometryTransport {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [FiniteDimensional 𝕜 H] (N : UnitarilyInvariantSeminorm 𝕜 E F) (ι : H →ₗᵢ[𝕜] E) : UnitarilyInvariantSeminorm 𝕜 H F

Pull a rectangular UI norm back along the adjoint of an isometric embedding of the domain. The transported norm measures A : H → F by the zero-padded map A ∘ ι⋆ : E → F.

Equations

• N.domainIsometryTransport ι = { toSeminorm := Seminorm.of (fun (A : H →ₗ[𝕜] F) => N (A ∘ₗ LinearMap.adjoint ι.toLinearMap)) ⋯ ⋯, unitary_invariant' := ⋯ }

@[simp]

theorem TauCeti.UnitarilyInvariantSeminorm.domainIsometryTransport_apply {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [FiniteDimensional 𝕜 H] (N : UnitarilyInvariantSeminorm 𝕜 E F) (ι : H →ₗᵢ[𝕜] E) (A : H →ₗ[𝕜] F) : (N.domainIsometryTransport ι) A = N (A ∘ₗ LinearMap.adjoint ι.toLinearMap)

Domain transport, unfolded.