OAI/Probability/Ballisticity/Walk/PathCompact.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.floor_scaled_close line 12
  2. lemma OAI.DirectionalTransience.scaledPolygon_oscillation_subset line 21
  3. theorem OAI.DirectionalTransience.gaussian_continuous_modulus line 62
  4. lemma OAI.DirectionalTransience.linearPolygon_abs_le_max line 87
  5. lemma OAI.DirectionalTransience.norm_scaledPolygon_le_max line 109
  6. lemma OAI.DirectionalTransience.gaussian_max_horizon_eventually line 120
  7. lemma OAI.DirectionalTransience.gaussian_continuous_norm_bound line 139
  8. lemma OAI.DirectionalTransience.continuousOscillation_mono line 178
  9. lemma OAI.DirectionalTransience.continuousOscillation_iInter_empty line 183
  10. lemma OAI.DirectionalTransience.tendsto_measure_continuousOscillation line 194
  11. lemma OAI.DirectionalTransience.continuous_modulus_uniform_of_eventual line 207
  12. lemma OAI.DirectionalTransience.continuous_norm_uniform_of_eventual line 230
  13. def OAI.DirectionalTransience.pathCompact line 255
  14. lemma OAI.DirectionalTransience.isClosed_pathCompact line 258
  15. lemma OAI.DirectionalTransience.isCompact_pathCompact line 262
  16. lemma OAI.DirectionalTransience.isTightMeasureSet_of_continuous_modulus line 290
  17. theorem OAI.DirectionalTransience.gaussian_iid_path_tight line 325
  18. lemma OAI.DirectionalTransience.tendstoInMeasure_pi line 352
  19. lemma OAI.DirectionalTransience.tendstoInMeasure_of_abs_le line 371
  20. lemma OAI.DirectionalTransience.selected_iid_div_tendstoInMeasure line 384
  21. lemma OAI.DirectionalTransience.polygon_eval_error_tendstoInMeasure line 405