OAI/Probability/FirstPassage/CrossingTrialGeometry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFPP.trialSpacing line 8
  2. def OAI.PlanarFPP.trialWindow line 10
  3. def OAI.PlanarFPP.trialOffset line 12
  4. def OAI.PlanarFPP.trialTranslate line 15
  5. theorem OAI.PlanarFPP.nearest_integer_error line 19
  6. theorem OAI.PlanarFPP.trialTranslate_error line 25
  7. theorem OAI.PlanarFPP.trialSpacing_bounds line 34
  8. theorem OAI.PlanarFPP.trialOffset_bound line 43
  9. theorem OAI.PlanarFPP.trial_strip_in_window line 56
  10. theorem OAI.PlanarFPP.trial_centers_separated line 76