OAI/Probability/SKGap/Localization/DriftSquare.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.GaussianHistory.driftSquare line 13
2. lemma OAI.SKGap.GaussianHistory.driftSquare_nonneg line 16
3. lemma OAI.SKGap.GaussianHistory.driftSquare_le line 19
4. lemma OAI.SKGap.GaussianHistory.continuous_driftSquare line 22
5. lemma OAI.SKGap.GaussianHistory.integrable_driftSquare_weight line 29
6. lemma OAI.SKGap.GaussianHistory.integrable_entropy_increment line 38
7. lemma OAI.SKGap.GaussianHistory.entropy_step_history_bound line 62
8. lemma OAI.SKGap.GaussianHistory.drift_integral_bound line 79
9. theorem OAI.SKGap.GaussianHistory.entropy_good_step line 131