OAI/Probability/FirstPassage/CoordinateTails.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFPP.straightEdge line 10
  2. theorem OAI.PlanarFPP.straightEdge_injective line 13
  3. theorem OAI.PlanarFPP.straightEdge_succ line 18
  4. theorem OAI.PlanarFPP.pathCost_replicate line 24
  5. theorem OAI.PlanarFPP.pathCost_replicate_edgeSet line 33
  6. theorem OAI.PlanarFPP.costly_straight_probability line 41
  7. theorem OAI.PlanarFPP.costly_straight_probability_real line 49
  8. theorem OAI.PlanarFPP.costly_straight_excess_probability_real line 63
  9. def OAI.PlanarFPP.coordinatePath line 80
  10. def OAI.PlanarFPP.latticeDistance line 83
  11. theorem OAI.PlanarFPP.coordinatePath_endpoint line 86
  12. theorem OAI.PlanarFPP.costly_horizontal_excess_probability_real line 89
  13. theorem OAI.PlanarFPP.costly_vertical_excess_probability_real line 101
  14. theorem OAI.PlanarFPP.costly_coordinatePath_probability_real line 113