OAI/Probability/FirstPassage/Paths.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PlanarFPP.Vertex line 11

    Also declared: ComparatorChallenges/GammaPassage.lean:17 (same declaration text), ComparatorChallenges/PlanarFirstPassage.lean:18 (same declaration text).

  2. abbrev OAI.PlanarFPP.Edge line 13

    Also declared: ComparatorChallenges/GammaPassage.lean:19 (same declaration text), ComparatorChallenges/PlanarFirstPassage.lean:20 (same declaration text).

  3. inductive OAI.PlanarFPP.Step line 15

    Also declared: ComparatorChallenges/GammaPassage.lean:21 (same declaration text), ComparatorChallenges/PlanarFirstPassage.lean:22 (same declaration text).

  4. def OAI.PlanarFPP.Step.delta line 19

    Also declared: ComparatorChallenges/GammaPassage.lean:25 (same declaration text), ComparatorChallenges/PlanarFirstPassage.lean:26 (same declaration text).

  5. def OAI.PlanarFPP.Step.reverse line 25
  6. def OAI.PlanarFPP.Step.edge line 31

    Also declared: ComparatorChallenges/GammaPassage.lean:31 (same declaration text), ComparatorChallenges/PlanarFirstPassage.lean:32 (same declaration text).

  7. theorem OAI.PlanarFPP.Step.delta_reverse line 37
  8. theorem OAI.PlanarFPP.Step.edge_reverse line 40
  9. def OAI.PlanarFPP.displacement line 44

    Also declared: ComparatorChallenges/GammaPassage.lean:37 (same declaration text), ComparatorChallenges/PlanarFirstPassage.lean:38 (same declaration text).

  10. def OAI.PlanarFPP.pathCost line 46

    Also declared: ComparatorChallenges/GammaPassage.lean:39 (same declaration text), ComparatorChallenges/PlanarFirstPassage.lean:40 (same declaration text).

  11. theorem OAI.PlanarFPP.displacement_nil line 50
  12. theorem OAI.PlanarFPP.displacement_cons line 51
  13. theorem OAI.PlanarFPP.displacement_append line 53
  14. theorem OAI.PlanarFPP.pathCost_append line 57
  15. theorem OAI.PlanarFPP.pathCost_nonneg line 64
  16. def OAI.PlanarFPP.transverse line 70
  17. def OAI.PlanarFPP.support line 71
  18. def OAI.PlanarFPP.defect line 72
  19. theorem OAI.PlanarFPP.transverse_add line 75
  20. theorem OAI.PlanarFPP.support_add line 78
  21. theorem OAI.PlanarFPP.defect_append line 82
  22. theorem OAI.PlanarFPP.minimum_defect line 87
  23. theorem OAI.PlanarFPP.transverse_chunk_witness line 102