OAI/Probability/SKRatio/Matrices/Imaginary.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatioGaussian.ComplexMatrix.lin_csmul line 41
2. lemma OAI.SKRatioGaussian.ComplexMatrix.opNorm_csmul line 44
3. def OAI.SKRatioGaussian.ComplexMatrix.imaginary line 47
4. lemma OAI.SKRatioGaussian.ComplexMatrix.imaginary_skew line 51
5. lemma OAI.SKRatioGaussian.ComplexMatrix.imaginary_norm line 55
6. lemma OAI.SKRatioGaussian.ComplexMatrix.imaginary_opNorm line 58
7. lemma OAI.SKRatioGaussian.ComplexMatrix.imaginary_sub line 62
8. lemma OAI.SKRatioGaussian.ComplexMatrix.imaginary_exp_unitary line 65
9. lemma OAI.SKRatioGaussian.ComplexMatrix.imaginary_exp_norm line 69
10. lemma OAI.SKRatioGaussian.ComplexMatrix.imaginary_exp_opNorm_le line 73
11. def OAI.SKRatioGaussian.ComplexMatrix.kernelMatrix line 80
12. lemma OAI.SKRatioGaussian.ComplexMatrix.kernel_integrable line 83
13. lemma OAI.SKRatioGaussian.ComplexMatrix.kernelMatrix_lipschitz line 91
14. lemma OAI.SKRatioGaussian.ComplexMatrix.kernelMatrix_four_point line 108