OAI/Probability/FirstPassage/LatticeGeometry.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFPP.latticeEmbed line 11
  2. theorem OAI.PlanarFPP.latticeEmbed_zero line 14
  3. theorem OAI.PlanarFPP.latticeFloor_embed line 15
  4. theorem OAI.PlanarFPP.latticeEmbed_sub line 18
  5. theorem OAI.PlanarFPP.plane_coordinate_le_norm line 23
  6. theorem OAI.PlanarFPP.plane_norm_le_coordinates line 26
  7. theorem OAI.PlanarFPP.latticeDistance_le_norm line 39
  8. theorem OAI.PlanarFPP.latticeFloor_error line 49
  9. theorem OAI.PlanarFPP.latticeFloor_mem_box line 59
  10. theorem OAI.PlanarFPP.latticeDistance_floor_le line 77
  11. theorem OAI.PlanarFPP.timeConstantNorm_lipschitz_bound line 98