OAI/Probability/Ballisticity/Crossings/Hit.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.HitAt line 12
  2. def OAI.DirectionalTransience.Hit line 15
  3. lemma OAI.DirectionalTransience.measurableSet_hitAt line 17
  4. lemma OAI.DirectionalTransience.measurableSet_hit line 25
  5. lemma OAI.DirectionalTransience.hitAt_pairwise_disjoint line 28
  6. def OAI.DirectionalTransience.hitKernel line 37
  7. lemma OAI.DirectionalTransience.hitKernel_apply line 40
  8. lemma OAI.DirectionalTransience.hitKernel_total line 52
  9. lemma OAI.DirectionalTransience.hitKernel_total_le_one line 57
  10. lemma OAI.DirectionalTransience.quenched_hitAt_future line 62
  11. lemma OAI.DirectionalTransience.hitKernel_future line 78
  12. lemma OAI.DirectionalTransience.hitKernel_noDrop_le line 93
  13. def OAI.DirectionalTransience.Cross line 112
  14. def OAI.DirectionalTransience.Strip line 116
  15. def OAI.DirectionalTransience.Upper line 120
  16. lemma OAI.DirectionalTransience.disjoint_strip_upper line 123
  17. lemma OAI.DirectionalTransience.cross_eq_hit line 129
  18. lemma OAI.DirectionalTransience.measurableSet_cross line 145
  19. lemma OAI.DirectionalTransience.cross_antitone line 150
  20. lemma OAI.DirectionalTransience.iInter_cross_subset_noDrop line 155
  21. lemma OAI.DirectionalTransience.noDrop_subset_cross_of_tendsto line 174
  22. def OAI.DirectionalTransience.TransientPaths line 180

    Also declared: ComparatorChallenges/VelocityHemisphere.lean:79 (same declaration text).

  23. lemma OAI.DirectionalTransience.measurableSet_transientPaths line 183
  24. lemma OAI.DirectionalTransience.transientPaths_translation line 190
  25. lemma OAI.DirectionalTransience.quenched_directionallyTransient_ae line 207
  26. def OAI.DirectionalTransience.crossingQuenched line 234
  27. lemma OAI.DirectionalTransience.crossingQuenched_antitone line 237
  28. lemma OAI.DirectionalTransience.crossingQuenched_tendsto_ae line 242
  29. lemma OAI.DirectionalTransience.quenched_hitAt_congr line 263
  30. lemma OAI.DirectionalTransience.hitKernel_congr line 294
  31. lemma OAI.DirectionalTransience.measurable_hitKernel_rows line 302
  32. lemma OAI.DirectionalTransience.crossingQuenched_eq_hitKernel line 321
  33. lemma OAI.DirectionalTransience.measurable_crossingQuenched_rows line 326
  34. lemma OAI.DirectionalTransience.crossingQuenched_zero line 334
  35. lemma OAI.DirectionalTransience.crossingQuenched_lower_step line 344
  36. lemma OAI.DirectionalTransience.mass_of_small_mean line 376
  37. def OAI.DirectionalTransience.endpointLaw line 400
  38. lemma OAI.DirectionalTransience.crossingQuenched_le_one line 404
  39. lemma OAI.DirectionalTransience.crossingQuenched_ne_top line 407
  40. lemma OAI.DirectionalTransience.endpointLaw_total line 410
  41. lemma OAI.DirectionalTransience.endpointLaw_total_le_one line 415
  42. lemma OAI.DirectionalTransience.endpointLaw_mean_le line 422