Diagonal sums of rank-one maps

For families v : ι → E, w : ι → F and real coefficients x : ι → ℝ, the diagonal sum LinearMap.diagonalSum 𝕜 v w x = ∑ᵢ xᵢ wᵢ ⊗ vᵢ sends y to ∑ᵢ xᵢ ⟪vᵢ, y⟫ wᵢ. For orthonormal families and a nonincreasing nonnegative tuple x, it is the map with singular system (vᵢ, wᵢ, xᵢ), and the singular value decomposition writes every map between finite-dimensional spaces in this form (LinearMap.exists_orthonormal_eq_sum_singularValues_smul_rankOne).

This file records how diagonal sums depend on their data: they are real-linear in the coefficients; permuting the coefficients or changing the sign of one of them permutes the vectors or changes the sign of one vector; and over two pairs of orthonormal families, diagonal sums with the same coefficients lie in the same two-sided unitary orbit (LinearMap.diagonalSum_mem_twoSidedUnitaryOrbit). These are the symmetries behind Fan dominance and the gauge representation of unitarily invariant seminorms.

noncomputable def LinearMap.diagonalSum (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_4} [Fintype ι] (v : ι → E) (w : ι → F) (x : ι → ℝ) : E →ₗ[𝕜] F

The map ∑ᵢ xᵢ wᵢ ⊗ vᵢ, sending y to ∑ᵢ xᵢ ⟪vᵢ, y⟫ wᵢ. For orthonormal families (vᵢ) and (wᵢ) and a nonnegative tuple x, this is the map with singular system (vᵢ, wᵢ, xᵢ).

theorem LinearMap.diagonalSum_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_4} [Fintype ι] (v : ι → E) (w : ι → F) (x : ι → ℝ) : diagonalSum 𝕜 v w x = ∑ i : ι, ↑(x i) • ↑(((InnerProductSpace.rankOne 𝕜) (w i)) (v i))

theorem LinearMap.diagonalSum_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_4} [Fintype ι] (v : ι → E) (w : ι → F) (x : ι → ℝ) (y : E) : (diagonalSum 𝕜 v w x) y = ∑ i : ι, ↑(x i) • inner 𝕜 (v i) y • w i

theorem LinearMap.linearIsometryEquiv_comp_diagonalSum_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_4} [Fintype ι] (U : F ≃ₗᵢ[𝕜] F) (V : E ≃ₗᵢ[𝕜] E) (v : ι → E) (w : ι → F) (x : ι → ℝ) : ↑↑↑U ∘ₗ diagonalSum 𝕜 v w x ∘ₗ ↑↑↑V = diagonalSum 𝕜 (⇑V.symm ∘ v) (⇑U ∘ w) x

Unitaries on either side act on the vectors of a diagonal sum.

theorem LinearMap.diagonalSum_add_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_4} [Fintype ι] (v : ι → E) (w : ι → F) (x y : ι → ℝ) (a b : ℝ) : diagonalSum 𝕜 v w (a • x + b • y) = ↑a • diagonalSum 𝕜 v w x + ↑b • diagonalSum 𝕜 v w y

theorem LinearMap.diagonalSum_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_4} [Fintype ι] (v : ι → E) (w : ι → F) (x y : ι → ℝ) : diagonalSum 𝕜 v w (x + y) = diagonalSum 𝕜 v w x + diagonalSum 𝕜 v w y

theorem LinearMap.diagonalSum_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_4} [Fintype ι] (v : ι → E) (w : ι → F) (a : ℝ) (x : ι → ℝ) : diagonalSum 𝕜 v w (a • x) = ↑a • diagonalSum 𝕜 v w x

theorem LinearMap.diagonalSum_neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_4} [Fintype ι] (v : ι → E) (w : ι → F) (x : ι → ℝ) : diagonalSum 𝕜 v w (-x) = -diagonalSum 𝕜 v w x

theorem LinearMap.norm_diagonalSum_apply_sq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_4} [Fintype ι] (v : ι → E) {w : ι → F} (hw : Orthonormal 𝕜 w) (x : ι → ℝ) (y : E) : ‖(diagonalSum 𝕜 v w x) y‖ ^ 2 = ∑ i : ι, x i ^ 2 * ‖inner 𝕜 (v i) y‖ ^ 2

Over an orthonormal family (wᵢ), ‖(∑ᵢ xᵢ wᵢ ⊗ vᵢ) y‖² = ∑ᵢ xᵢ² ‖⟪vᵢ, y⟫‖².

theorem LinearMap.diagonalSum_comp_perm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_4} [Fintype ι] (v : ι → E) (w : ι → F) (x : ι → ℝ) (π : Equiv.Perm ι) : diagonalSum 𝕜 v w (x ∘ ⇑π) = diagonalSum 𝕜 (v ∘ ⇑(Equiv.symm π)) (w ∘ ⇑(Equiv.symm π)) x

Permuting the coefficients of a diagonal sum permutes its vectors.

theorem LinearMap.diagonalSum_update_neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (v : ι → E) (w : ι → F) (x : ι → ℝ) (i : ι) : diagonalSum 𝕜 v w (Function.update x i (-x i)) = diagonalSum 𝕜 v (Function.update w i (-w i)) x

Changing the sign of one coefficient of a diagonal sum changes the sign of one vector.

theorem LinearMap.diagonalSum_mem_twoSidedUnitaryOrbit {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_4} [Fintype ι] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {v v' : ι → E} {w w' : ι → F} (hv : Orthonormal 𝕜 v) (hv' : Orthonormal 𝕜 v') (hw : Orthonormal 𝕜 w) (hw' : Orthonormal 𝕜 w') (x : ι → ℝ) : diagonalSum 𝕜 v' w' x ∈ (diagonalSum 𝕜 v w x).twoSidedUnitaryOrbit

Diagonal sums over two pairs of orthonormal families with the same coefficients are related by unitaries of the source and of the target.