OAI/Probability/SKGap/Localization/TAPVectorTaylor.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.varianceAverage line 13
2. def OAI.SKGap.varianceLinear line 15
3. def OAI.SKGap.magnetizationRemainder line 18
4. lemma OAI.SKGap.varianceAverage_eq_average line 21
5. lemma OAI.SKGap.varianceAverage_bounds line 28
6. lemma OAI.SKGap.magnetization_norm_bound line 33
7. lemma OAI.SKGap.vectorNorm_le_of_sq_sum line 41
8. lemma OAI.SKGap.magnetization_difference_norm line 46
9. lemma OAI.SKGap.magnetization_remainder_norm line 57
10. lemma OAI.SKGap.varianceAverage_remainder line 68
11. lemma OAI.SKGap.varianceAverage_difference line 92
12. lemma OAI.SKGap.tap_remainder_identity line 113
13. theorem OAI.SKGap.tap_remainder_norm line 147