Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.MakingMeasurementsProjective.QXPLayerIdentities.PositiveGram.Rows

Section 5 — Q/X/XHat/P identities and approximations #

Late-stage algebraic identities and approximation lemmas for the paper's Q/X/XHat/P intermediate layer.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.orthonormal_normalized_image_of_adjoint_comp_eigenvectors {κ : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] [NormedAddCommGroup F] [InnerProductSpace F] [FiniteDimensional F] (L : E →ₗ[] F) (v : κE) (lam : κ) (hv : Orthonormal v) (hlam : ∀ (i : κ), 0 < lam i) (heig : ∀ (i : κ), (LinearMap.adjoint L) (L (v i)) = (lam i) v i) :
Orthonormal fun (i : κ) => ↑(1 / (lam i)) L (v i)

Normalizing the images of positive Gram eigenvectors gives an orthonormal family.

This is the elementary singular-vector calculation underlying the rectangular polar-decomposition route. If v_i are orthonormal eigenvectors of L†L with positive eigenvalues λ_i, then the vectors λ_i^{-1/2} L v_i are orthonormal in the target Hilbert space.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.orthonormal_normalized_matrix_image_of_gram_eigenvectors {κ : Type u_1} {μ : Type u_2} {ι : Type u_3} [Fintype μ] [Fintype ι] [DecidableEq ι] (X : Matrix μ ι ) (v : κEuclideanSpace ι) (lam : κ) (hv : Orthonormal v) (hlam : ∀ (i : κ), 0 < lam i) (heig : ∀ (i : κ), (Matrix.toEuclideanLin (X.conjTranspose * X)) (v i) = (lam i) v i) :
Orthonormal fun (i : κ) => ↑(1 / (lam i)) (Matrix.toEuclideanLin X) (v i)

Matrix form of orthonormal_normalized_image_of_adjoint_comp_eigenvectors.

For a rectangular matrix X, orthonormal eigenvectors of the Gram operator Xᴴ * X with positive eigenvalues yield orthonormal normalized images under X. This is the first local linear-algebra step toward constructing the rectangular polar coisometry required for the QXP Xhat layer.

Spectral form of orthonormal_normalized_matrix_image_of_gram_eigenvectors.

After the right Gram matrix of X has been identified with a Hermitian operator Q, its positive spectral subspace gives an orthonormal family of normalized images under X. This is the form used when the rectangular polar construction is indexed by the positive spectrum of the total Q operator.

noncomputable def MIPStarRE.LDT.MakingMeasurementsProjective.normalizedMatrixImageRows {κ : Type u_1} {μ : Type u_2} {ι : Type u_3} [Fintype μ] [Fintype ι] [DecidableEq ι] (X : Matrix μ ι ) (v : κEuclideanSpace ι) (lam : κ) :
Matrix κ μ

The matrix whose rows are the normalized images of a prescribed Gram eigenvector family.

Equations
Instances For
    noncomputable def MIPStarRE.LDT.MakingMeasurementsProjective.positiveGramSpectrumImageRows {μ : Type u_1} {ι : Type u_2} [Fintype μ] [Fintype ι] [DecidableEq ι] (X : Matrix μ ι ) (Q : Matrix ι ι ) (hQ : Q.IsHermitian) :
    Matrix { i : ι // 0 < hQ.eigenvalues i } μ

    The matrix of normalized images indexed by the positive spectrum of a Hermitian Gram operator.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem MIPStarRE.LDT.MakingMeasurementsProjective.normalized_matrix_image_rows_mul_conjTranspose {κ : Type u_1} {μ : Type u_2} {ι : Type u_3} [DecidableEq κ] [Fintype μ] [Fintype ι] [DecidableEq ι] (X : Matrix μ ι ) (v : κEuclideanSpace ι) (lam : κ) (hv : Orthonormal v) (hlam : ∀ (i : κ), 0 < lam i) (heig : ∀ (i : κ), (Matrix.toEuclideanLin (X.conjTranspose * X)) (v i) = (lam i) v i) :

      The normalized positive Gram images assemble into a coisometry matrix.

      This is the row-matrix form of the preceding orthonormality statement. It is the bridge from the singular-vector calculation to the matrix equation Xhat Xhat† = I used by the QXP layer.

      theorem MIPStarRE.LDT.MakingMeasurementsProjective.normalized_matrix_image_rows_transpose_mixed {κ : Type u_1} {μ : Type u_2} {ι : Type u_3} [Fintype μ] [Fintype ι] [DecidableEq ι] (X : Matrix μ ι ) (v : κEuclideanSpace ι) (lam : κ) (hlam : ∀ (i : κ), 0 < lam i) (heig : ∀ (i : κ), (Matrix.toEuclideanLin (X.conjTranspose * X)) (v i) = (lam i) v i) :
      X.conjTranspose * (normalizedMatrixImageRows X v lam).transpose = Matrix.of fun (j : ι) (i : κ) => (lam i) * (v i).ofLp j

      The transpose of the normalized-image row matrix satisfies the mixed Gram identity on the chosen eigenvector family.

      This is the finite-dimensional calculation [ X^\dagger(\lambda_i^{-1/2}Xv_i)=\lambda_i^{1/2}v_i, ] recorded as a matrix identity with one column for each eigenvector.

      theorem MIPStarRE.LDT.MakingMeasurementsProjective.positive_gram_spectrum_image_rows_transpose_mixed {μ : Type u_1} {ι : Type u_2} [Fintype μ] [Fintype ι] [DecidableEq ι] (X : Matrix μ ι ) (Q : Matrix ι ι ) (hQ : Q.IsHermitian) (hgram : X.conjTranspose * X = Q) :
      X.conjTranspose * (positiveGramSpectrumImageRows X Q hQ).transpose = Matrix.of fun (j : ι) (i : { i : ι // 0 < hQ.eigenvalues i }) => (hQ.eigenvalues i) * (hQ.eigenvectorBasis i).ofLp j

      Spectral form of normalized_matrix_image_rows_transpose_mixed.

      On the positive spectral part of the Gram operator, the adjoint of X sends the normalized image of an eigenvector back to the eigenvector multiplied by the positive square root of its eigenvalue. This is the matrix identity which records the nonzero singular values in the rectangular polar construction.

      Spectral expansion of the CFC square root of a positive Hermitian matrix.

      This is the square-root analogue of the Hermitian spectral expansion. It is used below to compare the mixed product produced by the positive Gram-image columns with the operator CFC.sqrt Q on the whole ambient space, including the zero eigenspace.

      Rows dual to the positive Gram eigenvectors.

      Multiplying the positive mixed columns by this matrix sums those columns against the conjugate eigenvector coordinates. Thus the product is the spectral expansion of the square root of the Gram operator.

      Equations
      Instances For

        The conjugate eigenvector rows over the positive Gram spectrum are orthonormal.

        This is the right-singular-vector companion to the normalized image-row coisometry. It is independent of the matrix X; it uses only the orthonormality of the Hermitian eigenvector basis for Q.

        The positive Gram-image rows recover the square root of the Gram operator.

        The identity Xᴴ * (positiveGramSpectrumImageRows X Q hQ)ᵀ records the positive spectral columns sqrt(λ_i) v_i. Multiplying by the conjugate eigenvector rows gives the spectral expansion of CFC.sqrt Q; the zero eigenspace contributes nothing because Q is positive semidefinite.

        theorem MIPStarRE.LDT.MakingMeasurementsProjective.matrix_image_eq_zero_of_nonpositive_gram_eigenvalue {μ : Type u_1} {ι : Type u_2} [Fintype μ] [Fintype ι] [DecidableEq ι] (X : Matrix μ ι ) (Q : Matrix ι ι ) (hQ : Q.IsHermitian) (hQ_pos : Q.PosSemidef) (hgram : X.conjTranspose * X = Q) (i : ι) (hi : ¬0 < hQ.eigenvalues i) :

        Zero Gram eigenvectors are killed by the rectangular matrix.

        If Q = Xᴴ * X is positive semidefinite and an eigenvalue of Q is not strictly positive, then it is zero. The corresponding eigenvector therefore lies in the kernel of X. This is the algebraic reason why the arbitrary completion directions in the rectangular polar construction do not contribute to the mixed product Xᴴ * Xhat.

        theorem MIPStarRE.LDT.MakingMeasurementsProjective.adjoint_image_eq_zero_of_orthogonal_positive_gram_images {μ : Type u_1} {ι : Type u_2} [Fintype μ] [Fintype ι] [DecidableEq ι] (X : Matrix μ ι ) (Q : Matrix ι ι ) (hQ : Q.IsHermitian) (hQ_pos : Q.PosSemidef) (hgram : X.conjTranspose * X = Q) (y : EuclideanSpace μ) (hy : ∀ (i : { i : ι // 0 < hQ.eigenvalues i }), inner (↑(1 / (hQ.eigenvalues i)) (Matrix.toEuclideanLin X) (hQ.eigenvectorBasis i)) y = 0) :

        Vectors orthogonal to the positive Gram images are killed by X†.

        The proof tests the adjoint vector against the complete eigenvector basis of Q = Xᴴ * X. Positive eigenvectors are handled by the normalized-image orthogonality assumption, while non-positive eigenvectors are killed by X itself. This is the kernel statement needed when completing the positive left singular-vector rows to a full unitary.

        Spectral form of normalized_matrix_image_rows_mul_conjTranspose.

        The rows indexed by the strictly positive eigenvalues of the Hermitian Gram operator are the normalized images of the corresponding Gram eigenvectors. They therefore assemble into a coisometry.

        The strictly positive Gram spectrum has cardinality at most the row dimension of the rectangular matrix.

        The proof uses the normalized-image orthonormal family above: an orthonormal family in EuclideanSpace ℂ μ is linearly independent, so its index set cannot be larger than the dimension of that space.