OAI/Probability/FirstPassage/GridMeshes.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFPP.gridMeshExponent line 9
  2. def OAI.PlanarFPP.gridLastLevel line 10
  3. def OAI.PlanarFPP.gridMesh line 11
  4. def OAI.PlanarFPP.gridWidth line 12
  5. lemma OAI.PlanarFPP.gridMesh_pos line 14
  6. lemma OAI.PlanarFPP.gridWidth_pos line 15
  7. lemma OAI.PlanarFPP.gridLastLevel_unit line 16
  8. lemma OAI.PlanarFPP.gridMesh_antitone line 22
  9. lemma OAI.PlanarFPP.gridMesh_ratio_le line 28
  10. lemma OAI.PlanarFPP.gridMesh_divides line 33
  11. lemma OAI.PlanarFPP.gridMesh_level_bound line 38
  12. lemma OAI.PlanarFPP.gridMesh_count_ratio line 43
  13. lemma OAI.PlanarFPP.gridWidth_ratio line 52
  14. lemma OAI.PlanarFPP.gridMesh_below_record_length line 59
  15. theorem OAI.PlanarFPP.actual_grid_trial_probabilities line 82