OAI/Probability/UnimodularPercolation/Graph/Paths.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Bond paths, degree bounds and positivity of the critical parameter.

  1. inductive OAI.Percolation.Along line 19
  2. theorem OAI.Percolation.Along.conn line 24
  3. def OAI.Percolation.openSimpleGraph line 32

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:99 (same declaration text).

  4. theorem OAI.Percolation.conn_iff_reachable line 39
  5. theorem OAI.Percolation.walk_lift_bonds line 56
  6. theorem OAI.Percolation.conn_exists_bond_trail line 72
  7. theorem OAI.Percolation.Along.append line 82
  8. def OAI.Percolation.Step line 93
  9. theorem OAI.Percolation.finite_steps line 95
  10. def OAI.Percolation.stepEquiv line 102
  11. def OAI.Percolation.degree line 110
  12. theorem OAI.Percolation.degree_aut line 112
  13. theorem OAI.Percolation.exists_degree_bound line 116
  14. def OAI.Percolation.TrailLength line 130
  15. theorem OAI.Percolation.trailLength_upper line 133
  16. theorem OAI.Percolation.finiteWitness_trailLength line 138
  17. theorem OAI.Percolation.finiteWitness_edge line 144
  18. theorem OAI.Percolation.trailLength_succ_subset line 148
  19. theorem OAI.Percolation.trailLength_probability_le line 163
  20. theorem OAI.Percolation.Along.mem_reachBall line 194
  21. theorem OAI.Percolation.Along.take line 215
  22. theorem OAI.Percolation.reachBall_mono line 226
  23. theorem OAI.Percolation.infinite_cluster_subset_trailLength line 231
  24. theorem OAI.Percolation.infinite_cluster_probability_eq_zero_of_small line 243
  25. theorem OAI.Percolation.exists_infinite_cluster_probability_eq_zero_of_small line 254
  26. theorem OAI.Percolation.pc_pos line 265
  27. theorem OAI.Percolation.mainConclusion_of_strict_gap line 295