OAI/Probability/Ballisticity/Estimates/UniformRiemannMesh.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.realMesh line 14
  2. lemma OAI.DirectionalTransience.realMesh_zero line 16
  3. lemma OAI.DirectionalTransience.realMesh_last line 17
  4. lemma OAI.DirectionalTransience.realMesh_sub line 21
  5. lemma OAI.DirectionalTransience.realMesh_mono line 24
  6. lemma OAI.DirectionalTransience.riemann_error_le line 29
  7. lemma OAI.DirectionalTransience.tendsto_riemann_mesh line 63
  8. def OAI.DirectionalTransience.unitMesh line 91
  9. lemma OAI.DirectionalTransience.realMesh_between line 94
  10. lemma OAI.DirectionalTransience.unitMesh_coe line 100
  11. lemma OAI.DirectionalTransience.unitMesh_between line 106
  12. lemma OAI.DirectionalTransience.unitMesh_zero line 112
  13. lemma OAI.DirectionalTransience.unitMesh_last line 115
  14. lemma OAI.DirectionalTransience.unitMesh_sub line 118
  15. lemma OAI.DirectionalTransience.unitMesh_step_lt line 122
  16. lemma OAI.DirectionalTransience.contraction_recurrence_error line 140
  17. lemma OAI.DirectionalTransience.realEulerCoefficient_norm line 157
  18. lemma OAI.DirectionalTransience.scaled_exp_tendsto_zero line 163
  19. lemma OAI.DirectionalTransience.scaled_sqrt_cube_tendsto_zero line 177