Unitary-orbit estimates for orthogonal block sums

The orthogonal block sum of A : E₁ →ₗ[𝕜] F₁ and B : E₂ →ₗ[𝕜] F₂ is Mathlib's (A.prodMap B).withLpMap 2, acting componentwise on the Hilbert L² products. No separate block-sum construction is needed.

Two-sided unitary orbits and their convex hulls are stable under block sums. Consequently, Ky Fan domination on each block implies domination of the block sum, both for Ky Fan sums and for every rectangular unitarily invariant seminorm. These estimates combine independent bounds on orthogonal pieces without increasing their constants.

The orbit and orbit-hull statements require neither finite dimension nor completeness. Only the consequences using Fan dominance require finite-dimensional spaces.

On the spectral side, the adjoint and the Gram operator are formed blockwise, so the eigenspaces of the Gram operator of A ⊕ B are products of those of A and B: every positive singular value of A ⊕ B occurs as often as in A and B together. In particular the doubled block A ⊕ A repeats each singular value of A twice, and its Ky Fan sums are K₂ₖ(A ⊕ A) = 2 Kₖ(A).

Main results

• LinearMap.prodMap_withLpMap_mem_twoSidedUnitaryOrbitHull: stability of orbit hulls.
• LinearMap.kyFanSum_prodMap_withLpMap_le: blockwise Ky Fan domination.
• TauCeti.UnitarilyInvariantSeminorm.map_prodMap_withLpMap_le: the sharp block-sum comparison for all unitarily invariant seminorms.
• LinearMap.adjoint_prodMap_withLpMap: (A ⊕ B)† = A† ⊕ B†.
• LinearMap.finrank_eigenspace_prodMap_withLpMap: the eigenspaces of T₁ ⊕ T₂ have dimension dim ker(T₁ - μ) + dim ker(T₂ - μ).
• LinearMap.ncard_ofPred_singularValues_prodMap_withLpMap: a positive value occurs among the singular values of A ⊕ B as often as among those of A and B together.
• LinearMap.singularValues_prodMap_withLpMap_self: σᵢ(A ⊕ A) = σ_{⌊i/2⌋}(A).
• LinearMap.kyFanSum_prodMap_withLpMap_self: K₂ₖ(A ⊕ A) = 2 Kₖ(A).

References

• R. Bhatia, Matrix Analysis, Graduate Texts in Mathematics 169, Springer, 1997, Sections III.1 and IV.2.

theorem LinearMap.finrank_eigenspace_prodMap_withLpMap {K : Type u_6} {V₁ : Type u_7} {V₂ : Type u_8} [Field K] [AddCommGroup V₁] [Module K V₁] [FiniteDimensional K V₁] [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V₂] (T₁ : V₁ →ₗ[K] V₁) (T₂ : V₂ →ₗ[K] V₂) (μ : K) : Module.finrank K ↥(Module.End.eigenspace (withLpMap 2 (T₁.prodMap T₂)) μ) = Module.finrank K ↥(Module.End.eigenspace T₁ μ) + Module.finrank K ↥(Module.End.eigenspace T₂ μ)

The eigenspace of a block sum of endomorphisms is the product of the eigenspaces of the blocks, so its dimension is the sum of their dimensions.

theorem LinearMap.prodMap_withLpMap_mem_twoSidedUnitaryOrbit {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] [NormedAddCommGroup F₂] [InnerProductSpace 𝕜 F₂] {A C : E₁ →ₗ[𝕜] F₁} {B D : E₂ →ₗ[𝕜] F₂} (hA : A ∈ C.twoSidedUnitaryOrbit) (hB : B ∈ D.twoSidedUnitaryOrbit) : withLpMap 2 (A.prodMap B) ∈ (withLpMap 2 (C.prodMap D)).twoSidedUnitaryOrbit

Block sums of points in two-sided unitary orbits lie in the orbit of the block sum.

theorem LinearMap.prodMap_withLpMap_mem_twoSidedUnitaryOrbitHull {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] [NormedAddCommGroup F₂] [InnerProductSpace 𝕜 F₂] {A C : E₁ →ₗ[𝕜] F₁} {B D : E₂ →ₗ[𝕜] F₂} (hA : A ∈ C.twoSidedUnitaryOrbitHull) (hB : B ∈ D.twoSidedUnitaryOrbitHull) : withLpMap 2 (A.prodMap B) ∈ (withLpMap 2 (C.prodMap D)).twoSidedUnitaryOrbitHull

Convex unitary-orbit bounds on two blocks combine into the same bound on their orthogonal block sum.

theorem LinearMap.kyFanSum_prodMap_withLpMap_le {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] [NormedAddCommGroup F₂] [InnerProductSpace 𝕜 F₂] [FiniteDimensional 𝕜 E₁] [FiniteDimensional 𝕜 E₂] [FiniteDimensional 𝕜 F₁] [FiniteDimensional 𝕜 F₂] {A C : E₁ →ₗ[𝕜] F₁} {B D : E₂ →ₗ[𝕜] F₂} (hA : ∀ (k : ℕ), A.kyFanSum k ≤ C.kyFanSum k) (hB : ∀ (k : ℕ), B.kyFanSum k ≤ D.kyFanSum k) (k : ℕ) : (withLpMap 2 (A.prodMap B)).kyFanSum k ≤ (withLpMap 2 (C.prodMap D)).kyFanSum k

Ky Fan domination on each block implies Ky Fan domination on the orthogonal block sum.

@[simp]

theorem LinearMap.adjoint_prodMap_withLpMap {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] [NormedAddCommGroup F₂] [InnerProductSpace 𝕜 F₂] [FiniteDimensional 𝕜 E₁] [FiniteDimensional 𝕜 E₂] [FiniteDimensional 𝕜 F₁] [FiniteDimensional 𝕜 F₂] (A : E₁ →ₗ[𝕜] F₁) (B : E₂ →ₗ[𝕜] F₂) : adjoint (withLpMap 2 (A.prodMap B)) = withLpMap 2 ((adjoint A).prodMap (adjoint B))

Adjoint of a block sum. (A ⊕ B)† = A† ⊕ B†.

theorem LinearMap.ncard_ofPred_singularValues_prodMap_withLpMap {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] [NormedAddCommGroup F₂] [InnerProductSpace 𝕜 F₂] [FiniteDimensional 𝕜 E₁] [FiniteDimensional 𝕜 E₂] [FiniteDimensional 𝕜 F₁] [FiniteDimensional 𝕜 F₂] (A : E₁ →ₗ[𝕜] F₁) (B : E₂ →ₗ[𝕜] F₂) {s : ℝ} (hs : 0 < s) : {i : ℕ | (withLpMap 2 (A.prodMap B)).singularValues i = s}.ncard = {i : ℕ | A.singularValues i = s}.ncard + {i : ℕ | B.singularValues i = s}.ncard

A positive value s occurs among the singular values of A ⊕ B as often as among those of A and of B together.

theorem LinearMap.singularValues_prodMap_withLpMap_self {𝕜 : Type u_1} {E₁ : Type u_2} {F₁ : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] [FiniteDimensional 𝕜 E₁] [FiniteDimensional 𝕜 F₁] (A : E₁ →ₗ[𝕜] F₁) (i : ℕ) : (withLpMap 2 (A.prodMap A)).singularValues i = A.singularValues (i / 2)

Singular values of a doubled block. The singular values of A ⊕ A are those of A, each repeated twice: σᵢ(A ⊕ A) = σ_{⌊i/2⌋}(A).

theorem LinearMap.kyFanSum_prodMap_withLpMap_self {𝕜 : Type u_1} {E₁ : Type u_2} {F₁ : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] [FiniteDimensional 𝕜 E₁] [FiniteDimensional 𝕜 F₁] (A : E₁ →ₗ[𝕜] F₁) (k : ℕ) : (withLpMap 2 (A.prodMap A)).kyFanSum (2 * k) = 2 * A.kyFanSum k

Ky Fan sums of a doubled block. K₂ₖ(A ⊕ A) = 2 Kₖ(A).

theorem TauCeti.UnitarilyInvariantSeminorm.map_prodMap_withLpMap_le {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] [NormedAddCommGroup F₂] [InnerProductSpace 𝕜 F₂] [FiniteDimensional 𝕜 E₁] [FiniteDimensional 𝕜 E₂] [FiniteDimensional 𝕜 F₁] [FiniteDimensional 𝕜 F₂] (N : UnitarilyInvariantSeminorm 𝕜 (WithLp 2 (E₁ × E₂)) (WithLp 2 (F₁ × F₂))) {A C : E₁ →ₗ[𝕜] F₁} {B D : E₂ →ₗ[𝕜] F₂} (hA : ∀ (k : ℕ), A.kyFanSum k ≤ C.kyFanSum k) (hB : ∀ (k : ℕ), B.kyFanSum k ≤ D.kyFanSum k) : N (LinearMap.withLpMap 2 (A.prodMap B)) ≤ N (LinearMap.withLpMap 2 (C.prodMap D))

Blockwise Ky Fan estimates give the sharp comparison for every unitarily invariant seminorm on the orthogonal block sums.