OAI/Probability/Ballisticity/Crossings/CrossingGap.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.CrossingGap line 15
  2. lemma OAI.DirectionalTransience.measurableSet_crossingGap line 18
  3. lemma OAI.DirectionalTransience.signedHeight_zero line 21
  4. lemma OAI.DirectionalTransience.confined_crossingGap_split line 24
  5. lemma OAI.DirectionalTransience.quenched_crossingGap_confined line 104
  6. def OAI.DirectionalTransience.latticeBox line 136
  7. lemma OAI.DirectionalTransience.mem_latticeBox line 139
  8. lemma OAI.DirectionalTransience.card_latticeBox line 143
  9. lemma OAI.DirectionalTransience.latticeBox_of_signed_bound line 147
  10. def OAI.DirectionalTransience.badBoxEvent line 161
  11. lemma OAI.DirectionalTransience.measurableSet_badBoxEvent line 165
  12. lemma OAI.DirectionalTransience.badBox_bound line 170
  13. lemma OAI.DirectionalTransience.good_box_crossing line 188
  14. lemma OAI.DirectionalTransience.annealed_bound_bad_environment line 197
  15. lemma OAI.DirectionalTransience.annealed_crossingGap_bound line 211