OAI/Probability/Ballisticity/Geometry/CoordinateStrip.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.integrable_log_sum line 12
  2. lemma OAI.DirectionalTransience.stationary_tail_growth_obstruction line 35
  3. lemma OAI.DirectionalTransience.wordWeight_lower line 92
  4. lemma OAI.DirectionalTransience.wordPath_replicate line 102
  5. lemma OAI.DirectionalTransience.stayUntil_split line 110
  6. lemma OAI.DirectionalTransience.quenched_stayUntil_add line 122
  7. lemma OAI.DirectionalTransience.quenched_stayUntil_block_bound line 139
  8. def OAI.DirectionalTransience.CoordinateStrip line 155
  9. lemma OAI.DirectionalTransience.wordCylinder_up_disjoint_stay line 158
  10. lemma OAI.DirectionalTransience.quenched_strip_block line 174
  11. lemma OAI.DirectionalTransience.quenched_strip_geometric line 194
  12. def OAI.DirectionalTransience.HitThrough line 201
  13. lemma OAI.DirectionalTransience.measurableSet_hitThrough line 204
  14. lemma OAI.DirectionalTransience.hitThrough_subset_hit line 208
  15. lemma OAI.DirectionalTransience.hit_subset_hitThrough_union_stayUntil line 214
  16. lemma OAI.DirectionalTransience.quenched_hit_truncation line 222
  17. lemma OAI.DirectionalTransience.quenched_strip_hit_truncation line 229
  18. def OAI.DirectionalTransience.LatticeBall line 238
  19. lemma OAI.DirectionalTransience.latticeBall_finite line 241
  20. lemma OAI.DirectionalTransience.abs_step_le_one line 256
  21. def OAI.DirectionalTransience.NearestNeighborPrefix line 261
  22. lemma OAI.DirectionalTransience.nearestNeighborPrefix_bound line 264
  23. lemma OAI.DirectionalTransience.edgeWeight_eq_zero_of_not_neighbor line 281
  24. lemma OAI.DirectionalTransience.quenched_pathCylinder_locality line 288
  25. lemma OAI.DirectionalTransience.quenched_prefix_locality line 317
  26. lemma OAI.DirectionalTransience.quenched_hitThrough_locality line 332
  27. lemma OAI.DirectionalTransience.quenched_strip_compare line 350
  28. lemma OAI.DirectionalTransience.quenched_strip_uniform_locality line 361
  29. lemma OAI.DirectionalTransience.measurable_of_row_locality line 378
  30. lemma OAI.DirectionalTransience.measurable_hitThrough_ball line 397
  31. def OAI.DirectionalTransience.noDropFinite line 407
  32. lemma OAI.DirectionalTransience.noDropFinite_measurable line 411