OAI/Probability/FirstPassage/VerticalIntervals.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.verticalIntervalEdges line 10
2. lemma OAI.PlanarFPP.verticalIntervalEdges_card line 13
3. lemma OAI.PlanarFPP.vertical_straight_subset line 20
4. lemma OAI.PlanarFPP.vertical_straight_in line 39
5. theorem OAI.PlanarFPP.vertical_interval_all_pairs line 53
6. lemma OAI.PlanarFPP.costly_edge_set_probability_real line 92
7. theorem OAI.PlanarFPP.grid_vertical_cost_tail line 104