OAI/Probability/FirstPassage/LocalizedEvents.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFPP.edgeEnd line 9
  2. def OAI.PlanarFPP.internalEdges line 11
  3. theorem OAI.PlanarFPP.mem_internalEdges line 14
  4. theorem OAI.PlanarFPP.internalEdges_card_le line 18
  5. theorem OAI.PlanarFPP.step_mem_internalEdges line 22
  6. theorem OAI.PlanarFPP.internalEdges_disjoint line 28
  7. def OAI.PlanarFPP.pathEdges line 35
  8. theorem OAI.PlanarFPP.pathIn_cons_iff line 39
  9. theorem OAI.PlanarFPP.pathIn_endpoint line 54
  10. theorem OAI.PlanarFPP.pathEdges_subset_internalEdges line 58
  11. theorem OAI.PlanarFPP.pathCost_eq_of_agree line 71
  12. def OAI.PlanarFPP.strictLocalizedEvent line 80
  13. def OAI.PlanarFPP.boundedLocalizedEvent line 84
  14. theorem OAI.PlanarFPP.measurableSet_strictLocalizedEvent line 88
  15. theorem OAI.PlanarFPP.measurableSet_boundedLocalizedEvent line 95
  16. theorem OAI.PlanarFPP.strictLocalizedEvent_depends line 102
  17. theorem OAI.PlanarFPP.boundedLocalizedEvent_depends line 114
  18. theorem OAI.PlanarFPP.strip_vertices_disjoint line 126
  19. theorem OAI.PlanarFPP.localized_path_events_iIndepSet line 140