OAI/Probability/FirstPassage/BKDyadicPaths.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PlanarFPP.StrictPathWitness line 11
  2. def OAI.PlanarFPP.StrictPathWitness.edges line 18
  3. def OAI.PlanarFPP.StrictPathWitness.bits line 20
  4. def OAI.PlanarFPP.dyadicSurvival line 24
  5. lemma OAI.PlanarFPP.dyadicSurvival_nonneg line 27
  6. lemma OAI.PlanarFPP.dyadicSurvival_mono line 33
  7. lemma OAI.PlanarFPP.dyadicSurvival_eq line 42
  8. lemma OAI.PlanarFPP.pathCost_le_of_edges line 49
  9. def OAI.PlanarFPP.DyadicPathGood line 57
  10. lemma OAI.PlanarFPP.DyadicPathGood.mono line 61
  11. lemma OAI.PlanarFPP.DyadicPathGood.of_agree line 70
  12. def OAI.PlanarFPP.dyadicPathFamily line 86
  13. lemma OAI.PlanarFPP.mem_dyadicPathFamily line 92
  14. lemma OAI.PlanarFPP.upward_dyadicPathFamily line 99
  15. lemma OAI.PlanarFPP.dyadic_path_forces line 107
  16. lemma OAI.PlanarFPP.StrictPathWitness.disjoint_bits line 114
  17. def OAI.PlanarFPP.dyadicDisjointPathFamily line 120
  18. theorem OAI.PlanarFPP.dyadic_strict_path_BK line 128