Real diagonal operators and the operator singular-value decomposition

This module contains no norm structure. It supplies the diagonal operators used by both rectangular orbit majorization and square symmetric-gauge representation.

The diagonal operator of a real vector in an orthonormal basis

noncomputable def TauCeti.diagOp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} (b : OrthonormalBasis (Fin n) 𝕜 E) (x : Fin n → ℝ) : E →ₗ[𝕜] E

The operator with (real) diagonal x in the orthonormal basis b: diagOp b x (b i) = x i • b i.

Equations

• TauCeti.diagOp b x = ∑ i : Fin n, ↑(x i) • ↑(((InnerProductSpace.rankOne 𝕜) (b i)) (b i))

@[simp]

theorem TauCeti.diagOp_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} (b : OrthonormalBasis (Fin n) 𝕜 E) (x : Fin n → ℝ) (v : E) : (diagOp b x) v = ∑ i : Fin n, ↑(x i) • inner 𝕜 (b i) v • b i

The defining formula: diagOp b x expands v in the basis and scales the i-th coefficient by x i.

theorem TauCeti.diagOp_apply_basis {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} (b : OrthonormalBasis (Fin n) 𝕜 E) (x : Fin n → ℝ) (j : Fin n) : (diagOp b x) (b j) = ↑(x j) • b j

A diagonal operator scales each basis vector by its own entry. This is the form used to compare two diagonal operators, since equality on a basis suffices.

theorem TauCeti.diagOp_add {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} (b : OrthonormalBasis (Fin n) 𝕜 E) (x y : Fin n → ℝ) : diagOp b (x + y) = diagOp b x + diagOp b y

diagOp b is additive in the diagonal.

theorem TauCeti.diagOp_real_smul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} (b : OrthonormalBasis (Fin n) 𝕜 E) (c : ℝ) (x : Fin n → ℝ) : diagOp b (c • x) = ↑c • diagOp b x

diagOp b is homogeneous in the diagonal, with the real scalar cast into 𝕜.

theorem TauCeti.diagOp_const {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} (b : OrthonormalBasis (Fin n) 𝕜 E) (r : ℝ) : (diagOp b fun (x : Fin n) => r) = ↑r • LinearMap.id

A constant real diagonal is a scalar multiple of the identity. This is the bridge between the functional-calculus form r • id and the diagonal form the singular-value lemmas are stated in.

theorem TauCeti.diagOp_const_pair {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (b : OrthonormalBasis (Fin 2) 𝕜 E) (r : ℝ) : diagOp b ![r, r] = ↑r • LinearMap.id

The two-entry constant diagonal, in the ![r, r] shape the planar singular-value lemmas use.

theorem TauCeti.isSymmetric_diagOp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} (b : OrthonormalBasis (Fin n) 𝕜 E) (x : Fin n → ℝ) : (diagOp b x).IsSymmetric

A real diagonal operator is symmetric.

theorem TauCeti.adjoint_diagOp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (b : OrthonormalBasis (Fin n) 𝕜 E) (x : Fin n → ℝ) : LinearMap.adjoint (diagOp b x) = diagOp b x

A real diagonal operator is self-adjoint. This is why a unitarily invariant norm applied to diagOp yields a symmetric gauge on vectors.

theorem TauCeti.diagOp_comp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} (b : OrthonormalBasis (Fin n) 𝕜 E) (x y : Fin n → ℝ) : diagOp b x ∘ₗ diagOp b y = diagOp b (x * y)

Diagonal operators in the same basis multiply diagonally.

theorem TauCeti.singularValues_diagOp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : Module.finrank 𝕜 E = n) (b : OrthonormalBasis (Fin n) 𝕜 E) {x : Fin n → ℝ} (hx_anti : Antitone x) (hx0 : ∀ (i : Fin n), 0 ≤ x i) (i : Fin n) : (diagOp b x).singularValues ↑i = x i

The singular values of a diagonal operator with antitone nonnegative diagonal are the diagonal itself.

The operator SVD factorization

theorem TauCeti.exists_unitary_diagOp_factorization {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : Module.finrank 𝕜 E = n) (b : OrthonormalBasis (Fin n) 𝕜 E) (A : E →ₗ[𝕜] E) : ∃ (U : E ≃ₗᵢ[𝕜] E) (V : E ≃ₗᵢ[𝕜] E), A = ↑U.toLinearEquiv ∘ₗ (diagOp b fun (i : Fin n) => A.singularValues ↑i) ∘ₗ ↑V.toLinearEquiv

Operator SVD: relative to any fixed orthonormal basis b, every square operator factors as A = U ∘ diag(σ(A)) ∘ V with U, V unitary.