OAI/Probability/Ballisticity/Estimates/GridOscillation.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.shifted_iid_identDistrib line 12
  2. lemma OAI.DirectionalTransience.measureReal_shifted_max line 19
  3. lemma OAI.DirectionalTransience.measureReal_max_scaled_fourth_le line 29
  4. lemma OAI.DirectionalTransience.gaussian_max_block_eventually line 55
  5. lemma OAI.DirectionalTransience.realPartialSum_add line 78
  6. lemma OAI.DirectionalTransience.grid_oscillation_block line 82
  7. def OAI.DirectionalTransience.GridOscillation line 112
  8. lemma OAI.DirectionalTransience.measureReal_gridOscillation_le line 116
  9. lemma OAI.DirectionalTransience.eventually_floor_horizon_covered line 137
  10. lemma OAI.DirectionalTransience.gaussian_gridOscillation_eventually line 153
  11. theorem OAI.DirectionalTransience.gaussian_grid_modulus line 187
  12. theorem OAI.DirectionalTransience.transverse_common_gaussian_grid_modulus line 238
  13. def OAI.DirectionalTransience.unitRamp line 265
  14. lemma OAI.DirectionalTransience.unitRamp_zero line 267
  15. lemma OAI.DirectionalTransience.unitRamp_one line 269
  16. lemma OAI.DirectionalTransience.unitRamp_self line 271
  17. lemma OAI.DirectionalTransience.continuous_unitRamp line 273
  18. def OAI.DirectionalTransience.linearPolygon line 275
  19. lemma OAI.DirectionalTransience.linearPolygon_formula line 278
  20. instance OAI.DirectionalTransience.continuousPathMeasurableSpace line 302
  21. instance OAI.DirectionalTransience.continuousPathBorelSpace line 304
  22. def OAI.DirectionalTransience.polygonPath line 306
  23. lemma OAI.DirectionalTransience.polygonPath_apply line 310
  24. lemma OAI.DirectionalTransience.measurable_polygonPath line 318
  25. lemma OAI.DirectionalTransience.linearPolygon_near_partialSum line 324
  26. lemma OAI.DirectionalTransience.realPartialSum_step line 336
  27. lemma OAI.DirectionalTransience.not_gridOscillation_bound line 340
  28. lemma OAI.DirectionalTransience.linearPolygon_oscillation_le line 349
  29. def OAI.DirectionalTransience.scaledPolygon line 376
  30. lemma OAI.DirectionalTransience.scaledPolygon_apply line 379
  31. lemma OAI.DirectionalTransience.measurable_scaledPolygon line 383
  32. lemma OAI.DirectionalTransience.scaledPolygon_zero line 388
  33. def OAI.DirectionalTransience.ContinuousOscillation line 399
  34. lemma OAI.DirectionalTransience.isOpen_continuousOscillation line 402