OAI/Probability/FirstPassage/EndpointMesh.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFPP.meshFloor line 7
  2. lemma OAI.PlanarFPP.meshFloor_bounds line 9
  3. lemma OAI.PlanarFPP.meshFloor_dvd line 17
  4. lemma OAI.PlanarFPP.meshFloor_of_dvd line 20
  5. lemma OAI.PlanarFPP.meshFloor_greatest line 23
  6. lemma OAI.PlanarFPP.meshFloor_refinement line 29
  7. theorem OAI.PlanarFPP.meshFloor_refinement_count line 35
  8. def OAI.PlanarFPP.endpointColumn line 48
  9. lemma OAI.PlanarFPP.endpointColumn_last line 50
  10. lemma OAI.PlanarFPP.endpointColumn_step line 54
  11. lemma OAI.PlanarFPP.gridMesh_dvd_of_le line 60
  12. lemma OAI.PlanarFPP.endpointColumn_mono line 65
  13. def OAI.PlanarFPP.entranceColumn line 71
  14. def OAI.PlanarFPP.exitColumn line 73
  15. lemma OAI.PlanarFPP.entranceColumn_span line 75
  16. lemma OAI.PlanarFPP.exitColumn_span line 82
  17. lemma OAI.PlanarFPP.entranceColumn_dvd line 89
  18. lemma OAI.PlanarFPP.exitColumn_dvd line 92