OAI/Probability/GammaPassage/CrossingLocalized.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.GammaFPP.CrossingBridge.PathIn line 9
  2. abbrev OAI.GammaFPP.CrossingBridge.DependsOnEdges line 10
  3. theorem OAI.GammaFPP.CrossingBridge.pathIn_iff_interval line 12
  4. theorem OAI.GammaFPP.CrossingBridge.depends_iff_grid line 14
  5. def OAI.GammaFPP.CrossingBridge.edgeEnd line 17
  6. def OAI.GammaFPP.CrossingBridge.internalEdges line 19
  7. theorem OAI.GammaFPP.CrossingBridge.mem_internalEdges line 22
  8. theorem OAI.GammaFPP.CrossingBridge.internalEdges_card_le line 26
  9. theorem OAI.GammaFPP.CrossingBridge.step_mem_internalEdges line 30
  10. theorem OAI.GammaFPP.CrossingBridge.internalEdges_disjoint line 36
  11. def OAI.GammaFPP.CrossingBridge.pathEdges line 43
  12. theorem OAI.GammaFPP.CrossingBridge.pathIn_cons_iff line 47
  13. theorem OAI.GammaFPP.CrossingBridge.pathIn_endpoint line 62
  14. theorem OAI.GammaFPP.CrossingBridge.pathEdges_subset_internalEdges line 66
  15. theorem OAI.GammaFPP.CrossingBridge.pathCost_eq_of_agree line 79
  16. def OAI.GammaFPP.CrossingBridge.strictLocalizedEvent line 88
  17. def OAI.GammaFPP.CrossingBridge.boundedLocalizedEvent line 92
  18. theorem OAI.GammaFPP.CrossingBridge.measurableSet_strictLocalizedEvent line 96
  19. theorem OAI.GammaFPP.CrossingBridge.measurableSet_boundedLocalizedEvent line 103
  20. theorem OAI.GammaFPP.CrossingBridge.strictLocalizedEvent_depends line 110
  21. theorem OAI.GammaFPP.CrossingBridge.boundedLocalizedEvent_depends line 122
  22. theorem OAI.GammaFPP.CrossingBridge.strip_vertices_disjoint line 134