OAI/Probability/Ballisticity/Estimates/FirstBelow.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.endpointLaw_small_ratio line 12
  2. lemma OAI.DirectionalTransience.measurable_endpointLaw_rows line 26
  3. lemma OAI.DirectionalTransience.endpointLaw_supported line 34
  4. lemma OAI.DirectionalTransience.noDropQuenched_small_translation line 49
  5. lemma OAI.DirectionalTransience.endpointLaw_badmass line 63
  6. lemma OAI.DirectionalTransience.stopped_layer_small_ratio line 135
  7. def OAI.DirectionalTransience.FirstBelow line 169
  8. lemma OAI.DirectionalTransience.firstBelow_iff_exists line 172
  9. lemma OAI.DirectionalTransience.firstBelow_unique line 180
  10. lemma OAI.DirectionalTransience.firstBelow_pairwise_disjoint line 187
  11. lemma OAI.DirectionalTransience.crossingQuenched_mesh_tendsto line 195
  12. lemma OAI.DirectionalTransience.measurableSet_firstBelow_crossing line 220
  13. lemma OAI.DirectionalTransience.noDrop_small_recursive line 246
  14. lemma OAI.DirectionalTransience.positive_random_small_set line 327
  15. lemma OAI.DirectionalTransience.noDrop_geometric_tail line 365
  16. lemma OAI.DirectionalTransience.exists_inverse_geometric_ratio line 405
  17. lemma OAI.DirectionalTransience.inverse_power_le_series line 426