OAI/Probability/FirstPassage/BKBitLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.dyadicRankCell line 12
2. lemma OAI.PlanarFPP.measurableSet_dyadicRankCell line 16
3. lemma OAI.PlanarFPP.dyadicRankCell_disjoint line 28
4. lemma OAI.PlanarFPP.ExponentialEnvironment.dyadicRankCell_real line 36
5. theorem OAI.PlanarFPP.ExponentialEnvironment.dyadicRankCells_real line 46
6. theorem OAI.PlanarFPP.ExponentialEnvironment.ae_dyadicRankCell line 62
7. lemma OAI.PlanarFPP.dyadicRankCell_survival line 87
8. lemma OAI.PlanarFPP.dyadicRankCell_path_iff line 93