OAI/Probability/UnimodularPercolation/Escape/PositiveEscapes.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Positive Escapes for bond percolation.

  1. theorem OAI.Percolation.finite_dependent_event_union line 15
  2. theorem OAI.Percolation.raw_anchor_finite_collision_bound line 40
  3. theorem OAI.Percolation.raw_hits_distant_set_bound line 91
  4. def OAI.Percolation.earlyCollisionCost line 142
  5. theorem OAI.Percolation.earlyCollisionCost_tendsto line 145
  6. theorem OAI.Percolation.exists_earlyCollisionCutoff line 159
  7. theorem OAI.Percolation.finite_weighted_event_or line 171
  8. theorem OAI.Percolation.raw_early_collision_bound line 193
  9. theorem OAI.Percolation.raw_anchor_event_le_unconditioned line 273
  10. theorem OAI.Percolation.raw_anchor_early_collision_bound line 324
  11. theorem OAI.Percolation.raw_tail_integrate_anchor_event line 349
  12. theorem OAI.Percolation.finite_threefold_event_or line 382
  13. def OAI.Percolation.firstEscapeCollision line 414
  14. def OAI.Percolation.suffixCollisionCost line 423
  15. theorem OAI.Percolation.raw_first_escape_collision_bound line 428
  16. theorem OAI.Percolation.conditional_first_escape_collision_bound line 513
  17. theorem OAI.Percolation.exists_first_escape_uniform_cutoffs line 563
  18. theorem OAI.Percolation.raw_tail_anchor_total_mass line 598
  19. theorem OAI.Percolation.raw_tail_anchor_conditional_mass line 625
  20. theorem OAI.Percolation.graph_dist_aut line 649
  21. theorem OAI.Percolation.geodesic_anchor_early_separations line 666
  22. theorem OAI.Percolation.exists_positive_first_escape line 706
  23. theorem OAI.Percolation.finite_event_fiber_sum line 775
  24. theorem OAI.Percolation.rooted_label_raw_event_bound line 800
  25. def OAI.Percolation.labelFirstEscapeCollision line 840
  26. theorem OAI.Percolation.labelFromCode_first_collision line 847
  27. theorem OAI.Percolation.raw_rooted_first_collision_marginal line 864
  28. theorem OAI.Percolation.rooted_first_collision_probability_marginal line 931
  29. theorem OAI.Percolation.rooted_first_collision_probability_bound line 965
  30. theorem OAI.Percolation.HoldingWalk.map_position line 1023
  31. theorem OAI.Percolation.list_common_vertex_map_iff line 1031
  32. theorem OAI.Percolation.labelFirstEscapeCollision_aut line 1045
  33. theorem OAI.Percolation.rootOrbitWeight_pos line 1074
  34. theorem OAI.Percolation.rooted_escape_collision_reversal line 1092
  35. theorem OAI.Percolation.rooted_both_collision_probability_bound line 1123
  36. theorem OAI.Percolation.exists_positive_two_escape_label line 1174