OAI/Probability/SKGap/Localization/QuadraticCoeff.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.quadraticCoeff line 54
2. def OAI.SKGap.linearCoeff line 58
3. lemma OAI.SKGap.sum_coord_sq line 62
4. lemma OAI.SKGap.sum_outer_sq line 65
5. lemma OAI.SKGap.quadraticCoeff_increment line 75
6. lemma OAI.SKGap.linearCoeff_increment line 91
7. theorem OAI.SKGap.quadratic_linear_increment_difference line 109
8. theorem OAI.SKGap.quadratic_linear_increment_le line 118
9. lemma OAI.SKGap.quadratic_linear_orthogonal line 127
10. lemma OAI.SKGap.continuous_quadraticCoeff line 135
11. lemma OAI.SKGap.continuous_linearCoeff line 144