OAI/Probability/SKGap/Matrix/MatrixWhitening.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SKGap.positive_sqrt_dataline 14 - theorem
OAI.SKGap.positive_whitening_gramline 24 - theorem
OAI.SKGap.positive_unwhiteningline 36