OAI/Probability/SKGap/Localization/LocalWhitening.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.vectorNorm_sq_dot line 13
2. lemma OAI.SKGap.gram_energy line 17
3. lemma OAI.SKGap.regularizedGram_posDef line 21
4. lemma OAI.SKGap.squareRoot_energy line 28
5. theorem OAI.SKGap.localGaussian_whitening line 36
6. lemma OAI.SKGap.symmetric_row_sq_bound line 65
7. lemma OAI.SKGap.vectorNorm_fourth_le line 93
8. lemma OAI.SKGap.tap_remainder_sq line 101
9. lemma OAI.SKGap.varianceAverage_sq_difference line 126