OAI/Probability/SKGap/Localization/CondSubConst.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.GaussianStep.cond_sub_const line 11
2. lemma OAI.SKGap.GaussianStep.energy_sub_const line 17
3. lemma OAI.SKGap.GaussianStep.var_center line 22
4. lemma OAI.SKGap.GaussianHistory.localization_scalar line 38
5. def OAI.SKGap.GaussianHistory.localizationLoss line 54
6. def OAI.SKGap.GaussianHistory.localizationCost line 57
7. lemma OAI.SKGap.GaussianHistory.centered_localization_bound line 60
8. theorem OAI.SKGap.GaussianHistory.poincare_of_history_estimates line 92
9. lemma OAI.SKGap.GaussianHistory.eventProbability_lift line 141
10. lemma OAI.SKGap.GaussianHistory.eventProbability_union_le line 157
11. def OAI.SKGap.GaussianHistory.goodPrefix line 166
12. lemma OAI.SKGap.GaussianHistory.measurable_goodPrefix line 170
13. lemma OAI.SKGap.GaussianHistory.goodPrefix_not_bad line 175
14. lemma OAI.SKGap.GaussianHistory.goodPrefix_previous line 180
15. lemma OAI.SKGap.GaussianHistory.goodPrefix_failure_bound line 183
16. lemma OAI.SKGap.GaussianHistory.eventProbability_mono line 202
17. lemma OAI.SKGap.GaussianHistory.bad_term_le_sum line 207