OAI/LinearAlgebra/MatrixState/HilbertSchmidt.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RowColumn.MatrixState.hsVector line 11
2. lemma OAI.RowColumn.MatrixState.hsVector_inner line 16
3. lemma OAI.RowColumn.MatrixState.hsVector_norm_sq line 24
4. lemma OAI.RowColumn.MatrixState.trace_mH_mul_le line 29
5. lemma OAI.RowColumn.MatrixState.trace_mul_psd_nonneg line 38
6. lemma OAI.RowColumn.MatrixState.trace_mul_mono line 50
7. lemma OAI.RowColumn.MatrixState.trace_sqrt_conjugate_le_one line 56
8. lemma OAI.RowColumn.MatrixState.toEuclideanCLM_positive_iff line 95
9. lemma OAI.RowColumn.MatrixState.trace_toEuclideanCLM line 100
10. lemma OAI.RowColumn.MatrixState.hsVector_injective line 106
11. lemma OAI.RowColumn.MatrixState.hsVector_norm_sq_sum line 112
12. lemma OAI.RowColumn.MatrixState.finite_sum_embedding_le line 117
13. lemma OAI.RowColumn.MatrixState.hsVector_submatrix_norm_sq_le line 124
14. lemma OAI.RowColumn.MatrixState.hsVector_sandwich_sq line 135

    Source documentation

    The exact Hilbert--Schmidt trace formula used in the two PSD majorizations.

    lemma hsVector_sandwich_sq (A B X : Matrix I I ℂ)
        (hA : A.IsHermitian) (hB : B.IsHermitian) :
        ‖hsVector (A * X * B)‖^2 = (A^2 * X * B^2 * X.conjTranspose).trace.re := by
    …

    Mentions: OAI.RowColumn.MatrixState.hsVector

15. def OAI.RowColumn.MatrixState.matrixAlgebraCore line 149

    Source documentation

    A concrete finite-algebra Hilbert--Schmidt core, not the operator norm.

    def matrixAlgebraCore (A : StarSubalgebra ℂ (Matrix I I ℂ)) : InnerProductSpace.Core ℂ A where
    …

16. def OAI.RowColumn.MatrixState.matrixAlgebraTrace line 161
17. lemma OAI.RowColumn.MatrixState.matrixAlgebraCore_inner line 164
18. instance OAI.RowColumn.MatrixState.matrixAlgebraIsClosed line 168