OAI/Probability/SKRatio/Matrices/MatrixCoordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SKRatioGaussian.MatrixCoordinates line 16
2. def OAI.SKRatioGaussian.goeMatrix line 20
3. def OAI.SKRatioGaussian.rawCoordinateMatrix line 25
4. lemma OAI.SKRatioGaussian.rawCoordinateMatrix_norm line 28
5. lemma OAI.SKRatioGaussian.goeMatrix_norm line 38
6. lemma OAI.SKRatioGaussian.goeMatrix_sub line 50
7. lemma OAI.SKRatioGaussian.goeMatrix_L2_lipschitz line 54
8. lemma OAI.SKRatioGaussian.goeMatrix_pi_lipschitz line 61
9. def OAI.SKRatioGaussian.symmetricElementary line 70
10. lemma OAI.SKRatioGaussian.goeMatrix_update line 74
11. lemma OAI.SKRatioGaussian.symmetricElementary_norm_le line 83
12. lemma OAI.SKRatioGaussian.goeMatrix_updated_hasDerivAt line 87