OAI/Probability/FirstPassage/RealScaleConnections.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarFPP.latticeEmbed_norm_le_of_box line 10
  2. lemma OAI.PlanarFPP.lattice_mem_box_of_norm line 19

    Distinct definitions of this name: OAI/Probability/FirstPassage/EndpointNet.lean:25 (different declaration text). Qualify references as OAI.PlanarFPP.lattice_mem_box_of_norm@path.

  3. theorem OAI.PlanarFPP.real_scale_connections line 26
  4. lemma OAI.PlanarFPP.floor_real_ratio_tendsto line 63
  5. def OAI.PlanarFPP.scaledLatticePoint line 68
  6. lemma OAI.PlanarFPP.scaledLatticePoint_norm line 71
  7. lemma OAI.PlanarFPP.scaledLatticePoint_sub_norm line 76
  8. lemma OAI.PlanarFPP.scaled_floor_error line 82
  9. lemma OAI.PlanarFPP.scaled_floor_tendsto line 92
  10. lemma OAI.PlanarFPP.latticeEmbed_nsmul line 102
  11. lemma OAI.PlanarFPP.scaled_lattice_ray_tendsto line 107
  12. theorem OAI.PlanarFPP.real_scale_connections_normalized line 113