OAI/Probability/SKRatio/Matrices/LinSub.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatioGaussian.ComplexMatrix.lin_sub line 37
2. lemma OAI.SKRatioGaussian.ComplexMatrix.lin_neg line 38
3. lemma OAI.SKRatioGaussian.ComplexMatrix.opNorm_smul line 39
4. lemma OAI.SKRatioGaussian.ComplexMatrix.unitary_exp_smul line 45
5. lemma OAI.SKRatioGaussian.ComplexMatrix.opNorm_exp_sub line 51
6. lemma OAI.SKRatioGaussian.ComplexMatrix.frobenius_exp_sub line 62
7. lemma OAI.SKRatioGaussian.ComplexMatrix.exp_four_point line 73