OAI/Probability/GammaPassage/RealDirectionGeometry.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GammaFPP.RealDirectionBridge.latticeEmbed line 14
  2. theorem OAI.GammaFPP.RealDirectionBridge.latticeEmbed_zero line 17
  3. theorem OAI.GammaFPP.RealDirectionBridge.latticeFloor_embed line 18
  4. theorem OAI.GammaFPP.RealDirectionBridge.latticeEmbed_sub line 21
  5. theorem OAI.GammaFPP.RealDirectionBridge.plane_coordinate_le_norm line 26
  6. theorem OAI.GammaFPP.RealDirectionBridge.plane_norm_le_coordinates line 29
  7. theorem OAI.GammaFPP.RealDirectionBridge.latticeDistance_le_norm line 42
  8. theorem OAI.GammaFPP.RealDirectionBridge.latticeFloor_error line 52
  9. theorem OAI.GammaFPP.RealDirectionBridge.timeConstantNorm_lipschitz_bound line 62
  10. theorem OAI.GammaFPP.RealDirectionBridge.passageTime_origin_difference_le line 88
  11. lemma OAI.GammaFPP.RealDirectionBridge.lattice_mem_box_of_norm line 95
  12. lemma OAI.GammaFPP.RealDirectionBridge.floor_real_ratio_tendsto line 102
  13. def OAI.GammaFPP.RealDirectionBridge.scaledLatticePoint line 107
  14. lemma OAI.GammaFPP.RealDirectionBridge.scaledLatticePoint_norm line 110
  15. lemma OAI.GammaFPP.RealDirectionBridge.scaledLatticePoint_sub_norm line 115
  16. lemma OAI.GammaFPP.RealDirectionBridge.scaled_floor_error line 121
  17. lemma OAI.GammaFPP.RealDirectionBridge.scaled_floor_tendsto line 131
  18. lemma OAI.GammaFPP.RealDirectionBridge.latticeEmbed_nsmul line 141
  19. lemma OAI.GammaFPP.RealDirectionBridge.scaled_lattice_ray_tendsto line 146
  20. lemma OAI.GammaFPP.RealDirectionBridge.passageTime_real_lattice_ray_tendsto line 152