Finite-dimensional Hilbert spaces

This file contains small reusable lemmas about finite-dimensional Hilbert spaces which are independent of the low individual degree test. The first ingredient is the elementary fact that a Hilbert space embeds linearly and isometrically into any finite-dimensional Hilbert space of at least the same dimension. The second translates this dimension-controlled isometry into a rectangular matrix with orthonormal rows.

References

The construction is the standard one: choose orthonormal bases in the two spaces and send the first basis into the corresponding initial segment of the second basis. The resulting matrix statement is the finite-dimensional coisometry identity used in the paper's rectangular Xhat construction.

noncomputable def LinearIsometry.ofFinrankLE {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (h : Module.finrank 𝕜 E ≤ Module.finrank 𝕜 F) : E →ₗᵢ[𝕜] F

A finite-dimensional Hilbert space admits a linear isometric embedding into any finite-dimensional Hilbert space whose dimension is at least as large.

The map is obtained by choosing orthonormal bases in the two spaces and sending the i-th basis vector of the source to the i-th vector of the target, where the target index is viewed through the inclusion of finite initial segments.

Equations

• LinearIsometry.ofFinrankLE h = (((stdOrthonormalBasis 𝕜 E).toBasis.constr 𝕜) fun (i : Fin (Module.finrank 𝕜 E)) => (stdOrthonormalBasis 𝕜 F) (Fin.castLE h i)).isometryOfOrthonormal ⋯ ⋯

theorem Matrix.toEuclideanLin_conjTranspose_mul_self {𝕜 : Type u_1} [RCLike 𝕜] {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m n 𝕜) : toEuclideanLin (A.conjTranspose * A) = LinearMap.adjoint (toEuclideanLin A) ∘ₗ toEuclideanLin A

The matrix of an adjoint product is the adjoint-composition of the corresponding Euclidean linear map.

theorem Matrix.mul_conjTranspose_eq_one_of_orthonormal_rows {𝕜 : Type u_1} [RCLike 𝕜] {m : Type u_2} {n : Type u_3} [DecidableEq m] [Fintype n] (row : m → EuclideanSpace 𝕜 n) (hrow : Orthonormal 𝕜 row) : (of fun (i : m) (j : n) => (row i).ofLp j) * (of fun (i : m) (j : n) => (row i).ofLp j).conjTranspose = 1

A matrix whose rows form an orthonormal family is a coisometry.

theorem Matrix.exists_mul_conjTranspose_eq_one_of_card_le {𝕜 : Type u_1} [RCLike 𝕜] {m : Type u_2} {n : Type u_3} [Fintype m] [DecidableEq m] [Fintype n] (h : Fintype.card m ≤ Fintype.card n) : ∃ (X : Matrix m n 𝕜), X * X.conjTranspose = 1

A rectangular matrix with orthonormal rows exists whenever the row index set has cardinality at most the column index set.

Equivalently, if m ≤ n in finite dimension, then there is an m × n matrix X satisfying X X† = I_m. The proof chooses a linear isometric embedding EuclideanSpace 𝕜 m →ₗᵢ[𝕜] EuclideanSpace 𝕜 n and then takes the adjoint of its matrix.