OAI/Probability/SKRatio/Matrices/DiagonalSqrt.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatioGaussian.diagonalSqrt line 55
2. lemma OAI.SKRatioGaussian.diagonalSqrt_norm_sq line 58
3. lemma OAI.SKRatioGaussian.diagonalSqrt_norm_sq_le line 66
4. lemma OAI.SKRatioGaussian.diagonalSqrt_norm_le_sqrt line 72
5. lemma OAI.SKRatioGaussian.continuous_diagonalSqrt line 84
6. lemma OAI.SKRatioGaussian.diagonal_sum_mul_le_norm line 88
7. lemma OAI.SKRatioGaussian.quadraticCoeff_norm line 99
8. lemma OAI.SKRatioGaussian.quadratic_margin line 118