OAI/Probability/SKRatio/Matrices/Vectorize.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatioGaussian.ComplexMatrix.vectorize line 39
2. lemma OAI.SKRatioGaussian.ComplexMatrix.vectorize_norm line 44
3. instance OAI.SKRatioGaussian.ComplexMatrix.frobeniusInnerProduct line 51
4. def OAI.SKRatioGaussian.ComplexMatrix.hermitianBall line 60
5. lemma OAI.SKRatioGaussian.ComplexMatrix.hermitianBall_closed line 63
6. lemma OAI.SKRatioGaussian.ComplexMatrix.hermitianBall_convex line 68
7. lemma OAI.SKRatioGaussian.ComplexMatrix.hermitianBall_good line 83
8. def OAI.SKRatioGaussian.ComplexMatrix.matrixProject line 88
9. lemma OAI.SKRatioGaussian.ComplexMatrix.matrixProject_lipschitz line 91
10. lemma OAI.SKRatioGaussian.ComplexMatrix.matrixProject_bound line 95
11. lemma OAI.SKRatioGaussian.ComplexMatrix.matrixProject_eq_self line 99