OAI/Probability/DirectionalWalk/ContactEvents.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.visits line 12
  2. lemma OAI.DirectionalZeroOne.measurableSet_visits line 14
  3. def OAI.DirectionalZeroOne.contactAvoid line 18
  4. lemma OAI.DirectionalZeroOne.measurableSet_contactAvoid line 21
  5. lemma OAI.DirectionalZeroOne.contactAvoid_iff_firstHit line 24
  6. def OAI.DirectionalZeroOne.contactRectangle line 34
  7. lemma OAI.DirectionalZeroOne.measurableSet_contactRectangle line 37
  8. lemma OAI.DirectionalZeroOne.contactRectangles_disjoint line 40
  9. lemma OAI.DirectionalZeroOne.annealed_contactRectangle_transfer line 51
  10. lemma OAI.DirectionalZeroOne.weighted_contact_transfer line 66
  11. lemma OAI.DirectionalZeroOne.hits_eq_firstHitWords line 89
  12. lemma OAI.DirectionalZeroOne.negative_visit_firstWord_subset line 108
  13. lemma OAI.DirectionalZeroOne.quenched_negative_visit_bound line 119
  14. def OAI.DirectionalZeroOne.lateVisits line 142
  15. lemma OAI.DirectionalZeroOne.measurableSet_lateVisits line 145
  16. lemma OAI.DirectionalZeroOne.annealed_avoidsUpper_lateLower line 153
  17. lemma OAI.DirectionalZeroOne.quenched_negative_bins line 173
  18. lemma OAI.DirectionalZeroOne.weighted_disjoint_measure_bound line 195
  19. lemma OAI.DirectionalZeroOne.weighted_contact_bin_bound line 210