OAI/Probability/UnimodularPercolation/Encounter/IntrinsicDistance.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Intrinsic distance and closest vertices in percolation clusters.

  1. theorem OAI.Percolation.Along.exists_open_walk_length_le line 18
  2. theorem OAI.Percolation.mem_intrinsicBall_iff line 30
  3. theorem OAI.Percolation.measurableSet_mem_intrinsicBall line 45
  4. def OAI.Percolation.closest line 63
  5. theorem OAI.Percolation.closest_finite line 66
  6. theorem OAI.Percolation.closest_nonempty line 77
  7. theorem OAI.Percolation.mem_closest_iff_balls line 89
  8. theorem OAI.Percolation.measurableSet_mem_closest line 107
  9. def OAI.Percolation.openAutIso line 125
  10. theorem OAI.Percolation.iso_dist line 140
  11. theorem OAI.Percolation.closest_iso line 157
  12. theorem OAI.Percolation.dist_lt_of_cut_separates line 171
  13. theorem OAI.Percolation.closest_eq_singleton_of_branch line 183