OAI/Probability/UnimodularPercolation/Escape/SelectionBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Selection Bounds for bond percolation.

  1. theorem OAI.Percolation.exists_both_escape_uniform_cutoffs line 16
  2. theorem OAI.Percolation.rooted_label_event_of_tail_bound line 38
  3. theorem OAI.Percolation.rooted_label_probability_of_tail_bound line 107
  4. def OAI.Percolation.labelPotentialFailure line 160
  5. theorem OAI.Percolation.labelFromCode_potential_failure line 167
  6. theorem OAI.Percolation.rooted_label_potential_failure_bound line 189
  7. theorem OAI.Percolation.rooted_label_collision_potential_failure_bound line 231
  8. theorem OAI.Percolation.finite_weighted_success_lower line 287
  9. theorem OAI.Percolation.rooted_label_collision_potential_success_lower line 300
  10. theorem OAI.Percolation.exists_joint_collision_potential_cutoffs line 345
  11. theorem OAI.Percolation.labelFromCode_anchor_event line 378
  12. theorem OAI.Percolation.rooted_label_anchor_event_marginal line 396
  13. theorem OAI.Percolation.rooted_label_endpoint_marginal line 441
  14. theorem OAI.Percolation.rooted_label_endpoint_hit_bound line 470
  15. theorem OAI.Percolation.rooted_label_endpoint_ball_bound line 526