OAI/Probability/FirstPassage/UniformShape.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.rescaledPassage line 9
2. theorem OAI.PlanarFPP.passageTime_origin_difference_le line 12
3. theorem OAI.PlanarFPP.rescaledPassage_modulus line 19
4. theorem OAI.PlanarFPP.ae_rescaledPassage_modulus line 52
5. theorem OAI.PlanarFPP.ae_uniform_rescaledPassage line 66
6. theorem OAI.PlanarFPP.rescaledPassage_lattice_error line 82
7. theorem OAI.PlanarFPP.uniform_rescaled_ball_bound line 94
8. def OAI.PlanarFPP.UniformShape line 125
9. theorem OAI.PlanarFPP.uniformShape_of_uniform_rescaled line 129
10. theorem OAI.PlanarFPP.exponential_uniform_shape line 166