Revision #3489 → #4031 · back to history
modifiedSVD related to polar decomposition27b91965e78b
| Field | From #3489 | To #4031 |
|---|
| note | Polar decomposition of operators/matrices is not present in Mathlib (loogle for "polarDecomposition" returns 0 hits), so its relation to the SVD is not formalized. | Polar decomposition of operators/matrices is not present in Mathlib, so its relation to the SVD is not formalized. |
modifiedHouseholder reflection38e1ad47709f
| Field | From #3489 | To #4031 |
|---|
| note | Householder reflections/transformations are not formalized as a named construction (loogle for "Householder" returns 0 hits). | Householder reflections/transformations are not formalized as a named construction. |
modifiedPauli matricesd78d3095627e
| Field | From #3489 | To #4031 |
|---|
| note | The Pauli matrices are not defined as named constants in Mathlib (loogle for "Pauli" returns 0 hits). | The Pauli matrices are not defined as named constants in Mathlib. |
modifiedPartial isometry504b56193a9b
| Field | From #3489 | To #4031 |
|---|
| note | Partial isometries on Hilbert spaces are not a named concept in Mathlib (loogle for "partialIsometry" returns 0 hits). | Partial isometries on Hilbert spaces are not a named concept in Mathlib. |
addedEigenvalue decomposition12c98bf34281
addedBest low-rank approximation via truncated SVDae6130b77813
addedFrobenius norm equals sum of squared singular values55336e836f74
addedNearest orthogonal via polar decomposition unitary factor715599fe69db
addedSchmidt decomposition853d4288260d
addedRayleigh quotient378f7700e286
addedOrthonormal basis3ab6e03e6f63
addedRank of a matrix23ded3da830f
addedRange of a linear map904bfa42ca71
addedHermitian matrixf8b33abbe0b5
addedUnit sphere35a71612a7f6
addedBounded operator21a5eb2457c0