Zero extension of a finite-dimensional rectangular map

The embedding into the orthogonal direct sum preserves the singular-value sequence.

noncomputable def TauCeti.zeroExtension {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ[𝕜] F) : WithLp 2 (E × F) →ₗ[𝕜] WithLp 2 (E × F)

Zero extension of a rectangular map to a square endomorphism.

Equations

• TauCeti.zeroExtension A = ↑(WithLp.linearEquiv 2 𝕜 (E × F)).symm ∘ₗ { toFun := fun (z : E × F) => (0, A z.1), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ ↑(WithLp.linearEquiv 2 𝕜 (E × F))

@[simp]

theorem TauCeti.zeroExtension_apply {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ[𝕜] F) (z : WithLp 2 (E × F)) : (zeroExtension A) z = WithLp.toLp 2 (0, A z.ofLp.1)

The zero extension places A in the second component and zero in the first, which is what makes a rectangular operator into a square one without changing its singular values.

theorem TauCeti.zeroExtension_add {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A B : E →ₗ[𝕜] F) : zeroExtension (A + B) = zeroExtension A + zeroExtension B

Zero extension is additive.

theorem TauCeti.zeroExtension_smul {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (a : 𝕜) (A : E →ₗ[𝕜] F) : zeroExtension (a • A) = a • zeroExtension A

Zero extension commutes with scalar multiplication.

theorem TauCeti.singularValues_zeroExtension {𝕜 : 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 : E →ₗ[𝕜] F) : (zeroExtension A).singularValues = A.singularValues

Singular values are unchanged by zero extension, apart from zero padding.