OAI/Probability/FirstPassage/EndpointNet.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PlanarFPP.finite_ball_net line 9
2. theorem OAI.PlanarFPP.lattice_mem_box_of_norm line 25

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

3. theorem OAI.PlanarFPP.scaled_net_norm line 35
4. theorem OAI.PlanarFPP.scaled_net_approximates line 44