Section 5 — Rectangular SVD constructors for Q/X/XHat/P data #
Rectangular-SVD matrix identities and constructors for the paper's
Q/X/XHat/P intermediate layer.
The rectangular singular-value reconstruction of X.
If U and V are the square unitary factors and S is the rectangular
diagonal singular-value matrix, this is the matrix
U * S * V† appearing in the paper.
Equations
Instances For
The rectangular-SVD candidate for Xhat.
This is the paper's matrix U * I_{m × d} * V†, where Iro is the rectangular
row-coisometry replacing the displayed rectangular identity matrix.
Equations
- MIPStarRE.LDT.MakingMeasurementsProjective.rectangularSvdXHat U V Iro = U * Iro * V.conjTranspose
Instances For
The domain-space middle operator in the product X† * Xhat.
For rectangular-SVD data this is V * (S† * Iro) * V†, the operator on the
original Hilbert space which is later identified with sqrt Q.
Equations
- MIPStarRE.LDT.MakingMeasurementsProjective.rectangularSvdDomainMiddle V S Iro = V * (S.conjTranspose * Iro) * V.conjTranspose
Instances For
The row-space middle operator in the product X * Xhat†.
For rectangular-SVD data this is U * (S * Iro†) * U†, the formal counterpart
of the square matrix Σ_{m × m} in the paper.
Equations
- MIPStarRE.LDT.MakingMeasurementsProjective.rectangularSvdRangeMiddle U S Iro = U * (S * Iro.conjTranspose) * U.conjTranspose
Instances For
Left multiplication by a unitary group element preserves rectangular row coisometries.
If W W† = I, then (U W)(U W)† = I. This is the square-unitary part of
the paper's calculation of lem:X-hat-squared.
Right multiplication by the adjoint of a unitary group element preserves rectangular row coisometries.
If W W† = I, then (W V†)(W V†)† = I. This is the right-square-unitary
part of the paper's calculation of lem:X-hat-squared.
The row-coisometry identity for the rectangular SVD choice of Xhat,
with the square factors represented as unitary group elements.
The mixed product obtained by multiplying the rectangular SVD formulae.
This lemma contains only the matrix algebra. The spectral identification of the
right hand side with a square root is supplied separately, since downstream
constructors usually know the square root in the form CFC.sqrt Q.
The mixed product obtained by multiplying the rectangular SVD formulae, with the left square factor represented as a unitary group element.
The first mixed product obtained from the rectangular SVD formulae.
This is the first identity in the paper's lem:X-times-X-hat, written in the
rectangular notation used by the formalization. If
X = U * S * Vᴴ and Xhat = U * Iro * Vᴴ, then
X * Xhatᴴ = U * (S * Iroᴴ) * Uᴴ. The middle factor S * Iroᴴ is the
formal counterpart of the square matrix Σ_{m × m} appearing in the paper.
The first mixed product obtained from the rectangular SVD formulae, with the right square factor represented as a unitary group element.
A positive operator whose square is Q is the CFC square root of Q.
This is the uniqueness of the positive square root, stated in the matrix language used in the projectivization layer.
The square-root identification for the middle factor in the rectangular SVD calculation.
If the middle operator V * (Sᴴ * Iro) * Vᴴ is positive and its square is the
target operator Q, then it is the positive square root of Q. This is the
spectral input which turns the raw SVD calculation into the paper's identity
X† Xhat = sqrt Q.
The mixed rectangular SVD identity with the left square factor represented
as a unitary group element and the target square root supplied as an external
operator Q.
The rectangular SVD data determine a candidate Xhat and its two primitive
identities, with the square factors represented as unitary group elements.
Assemble QXPLayerData from a rank-reduction witness and the SVD
identities for Xhat.
The rank-reduction witness supplies the projectivity of each Q_a and the
identity ∑_a Q_a = Q. The remaining hypotheses are exactly the local
matrix-decomposition data for Q_a = X† T_a X and the two SVD-derived
identities for the chosen Xhat. Thus this constructor removes the
rank-reduction fields from the caller's obligations. The rectangular
SVD/polar decomposition that provides xHat is supplied by the
sigma-range / rectangular polar-decomposition route, which provides the
unitary and coisometry factors from the positive spectral subspace of Q.
The end-to-end chain through the rounding-to-projectors, rank-reduction,
and orthogonalization lemmas remains to be closed upstream.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Assemble QXPLayerData from rank-reduction data and rectangular SVD data
whose square factors are represented as Mathlib unitary-group elements.
The left and right unitarity laws are carried by the type of U and V; the
only remaining rectangular law is the coisometry of Iro.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Assemble QXPLayerData from unitary-group rectangular SVD data whose
middle factor is characterized as the positive square root of Q.
The unitarity of the square factors is represented by
Matrix.unitaryGroup, while the square-root identification is supplied by
positivity and the square equation for the middle factor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Assemble the canonical sigma-space Q/X/Xhat/P layer from rectangular SVD
data whose square factors are Matrix.unitaryGroup elements.
The unitarity hypotheses for U and V are carried by their types.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Assemble the canonical sigma-space Q/X/Xhat/P layer from unitary-group
rectangular SVD data whose middle factor is characterized as a positive square
root.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Rank-reduction existence form for the canonical sigma-space QXP layer from unitary-group rectangular SVD data.
Rank-reduction existence form for the canonical sigma-space QXP layer from unitary-group rectangular SVD data whose middle factor is characterized as a positive square root.