OAI/Probability/FirstPassage/BKQuantization.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFPP.roundedSurvival line 11
  2. def OAI.PlanarFPP.roundedEdgeCost line 14
  3. lemma OAI.PlanarFPP.roundedSurvival_nonneg line 17
  4. lemma OAI.PlanarFPP.roundedSurvival_le line 21
  5. lemma OAI.PlanarFPP.roundedSurvival_tendsto line 25
  6. lemma OAI.PlanarFPP.roundedSurvival_eventually_pos line 31
  7. lemma OAI.PlanarFPP.roundedEdgeCost_ge line 35
  8. lemma OAI.PlanarFPP.roundedEdgeCost_tendsto line 42
  9. lemma OAI.PlanarFPP.rounded_pathCost_tendsto line 48
  10. def OAI.PlanarFPP.RoundedPathGood line 55
  11. def OAI.PlanarFPP.StrictPathWitness.Good line 59
  12. lemma OAI.PlanarFPP.RoundedPathGood.original line 62
  13. lemma OAI.PlanarFPP.StrictPathWitness.Good.eventually_rounded line 67
  14. lemma OAI.PlanarFPP.strict_path_list_eventually_rounded line 76
  15. def OAI.PlanarFPP.StrictDisjointPaths line 88
  16. def OAI.PlanarFPP.RoundedDisjointPaths line 93
  17. lemma OAI.PlanarFPP.RoundedDisjointPaths.original line 99
  18. lemma OAI.PlanarFPP.StrictDisjointPaths.eventually_rounded line 105
  19. theorem OAI.PlanarFPP.strict_disjoint_eventual_rounded_iff line 127