OAI/Probability/FirstPassage/GridTrials.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarFPP.crossingEvent_eq_rareFastEvent line 8
2. lemma OAI.PlanarFPP.crossingEvent_translate line 20
3. def OAI.PlanarFPP.gridTrialTranslate line 26
4. lemma OAI.PlanarFPP.gridTrialTranslate_center line 29
5. lemma OAI.PlanarFPP.gridTrialTranslate_separation line 35
6. lemma OAI.PlanarFPP.gridTrials_disjoint line 51
7. lemma OAI.PlanarFPP.crossingEvent_probability_translate line 75
8. theorem OAI.PlanarFPP.gridTrials_failure_bound line 82