OAI/Probability/UnimodularPercolation/Escape/CollisionTails.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Collision Tails for bond percolation.

  1. theorem OAI.Percolation.raw_position_integral line 19
  2. theorem OAI.Percolation.raw_position_probability line 41
  3. theorem OAI.Percolation.raw_two_time_collision line 65
  4. theorem OAI.Percolation.matrixCoeff_norm_le line 92
  5. theorem OAI.Percolation.matrixCoeff_power_le line 97
  6. theorem OAI.Percolation.reachBall_exists_short_walk line 118
  7. theorem OAI.Percolation.dist_le_of_mem_reachBall line 142
  8. theorem OAI.Percolation.walkPower_zero_of_lt_dist line 147
  9. theorem OAI.Percolation.raw_two_time_collision_bound line 158
  10. theorem OAI.Percolation.finite_nonnegative_event_union line 181
  11. theorem OAI.Percolation.raw_intersection_probability_bound line 200
  12. theorem OAI.Percolation.geometric_cutoff_summable line 247
  13. theorem OAI.Percolation.geometric_cutoff_tsum line 253
  14. theorem OAI.Percolation.finite_geometric_cutoff_bound line 266
  15. theorem OAI.Percolation.finite_double_geometric_cutoff_bound line 275
  16. theorem OAI.Percolation.raw_intersection_uniform_bound line 325
  17. theorem OAI.Percolation.exists_uniform_raw_collision_separation line 337
  18. def OAI.Percolation.HoldingWalk.fromPositions line 366
  19. theorem OAI.Percolation.HoldingWalk.mass_fromPositions line 372
  20. theorem OAI.Percolation.HoldingWalk.position_fromPositions line 383
  21. theorem OAI.Percolation.HoldingWalk.position_append_left line 406
  22. theorem OAI.Percolation.HoldingWalk.position_append_right line 420
  23. theorem OAI.Percolation.HoldingWalk.ext_positions line 430
  24. def OAI.Percolation.segmentCenter line 468
  25. def OAI.Percolation.segmentPositivePositions line 470
  26. def OAI.Percolation.positiveStem line 473
  27. theorem OAI.Percolation.positiveStem_mass line 478
  28. theorem OAI.Percolation.orbitSegment_consecutive line 484
  29. def OAI.Percolation.escapeLabelRaw line 492
  30. theorem OAI.Percolation.escapeLabelRaw_mass line 501
  31. theorem OAI.Percolation.escapeLabelRaw_middle_position line 511
  32. theorem OAI.Percolation.RawFrom.ext_positions line 528
  33. theorem OAI.Percolation.RawFrom.pairwise_disjoint_position_indicators line 536
  34. theorem OAI.Percolation.finite_single_fiber_weight_bound line 546
  35. def OAI.Percolation.rootedEscapeLabelRaw line 572
  36. theorem OAI.Percolation.rootedEscapeLabelRaw_mass line 580
  37. theorem OAI.Percolation.rootedEscapeLabelRaw_middle_position line 590
  38. theorem OAI.Percolation.rootedEscapeLabelRaw_fiber_middle_mass line 599
  39. theorem OAI.Percolation.rootedEscapeLabelRaw_fiber_middle_positions line 609
  40. theorem OAI.Percolation.finite_auxiliary_event_bound line 628
  41. theorem OAI.Percolation.finite_nested_unique_fiber_bound line 639
  42. theorem OAI.Percolation.labelFromCode_middle_position line 684
  43. theorem OAI.Percolation.labelFromCode_middle_mass line 695
  44. theorem OAI.Percolation.rooted_code_single_anchor_fiber_bound line 716
  45. theorem OAI.Percolation.rooted_label_raw_fiber_mass_bound line 798
  46. theorem OAI.Percolation.tsum_indicator_div line 840
  47. theorem OAI.Percolation.rooted_label_raw_projection_bound line 847
  48. theorem OAI.Percolation.operator_pow_norm_le line 884
  49. theorem OAI.Percolation.positive_rows_collision_hasSum line 892
  50. theorem OAI.Percolation.positive_rows_collision_bound line 899
  51. theorem OAI.Percolation.walk_suffix_collision_operator_bound line 907
  52. theorem OAI.Percolation.raw_anchored_position_expectation line 931
  53. theorem OAI.Percolation.raw_tail_anchored_collision_bound line 947
  54. theorem OAI.Percolation.raw_tail_anchored_collision_uniform line 977
  55. theorem OAI.Percolation.anchoredPositionKernel_global_denominator line 1010
  56. theorem OAI.Percolation.finite_geometric_sum_bound line 1027
  57. theorem OAI.Percolation.raw_tail_anchor_collision_identity line 1044
  58. theorem OAI.Percolation.finite_threefold_event_union line 1082
  59. theorem OAI.Percolation.raw_tail_whole_suffix_collision_bound line 1107
  60. theorem OAI.Percolation.raw_anchor_position_identity line 1167
  61. theorem OAI.Percolation.raw_anchor_point_collision_bound line 1183