OAI/Probability/SKGap/Localization/DiagonalSqrt.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.diagonalSqrt line 54
2. lemma OAI.SKGap.diagonalSqrt_norm_sq line 57
3. lemma OAI.SKGap.diagonalSqrt_norm_sq_le line 65
4. lemma OAI.SKGap.diagonalSqrt_norm_le_sqrt line 71
5. lemma OAI.SKGap.continuous_diagonalSqrt line 83
6. lemma OAI.SKGap.diagonal_sum_mul_le_norm line 87
7. lemma OAI.SKGap.quadraticCoeff_norm line 98
8. lemma OAI.SKGap.quadratic_margin line 117