OAI/Probability/UnimodularPercolation/Exploration/Goodness.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

Pruning, finite and infinite goodness events and uniform bounds.

  1. def OAI.Percolation.pairOpenPivotals line 19
  2. def OAI.Percolation.CappedRadiusEvent line 24
  3. def OAI.Percolation.finiteCappedRadiusTail line 29
  4. theorem OAI.Percolation.sole_root_mark line 34
  5. theorem OAI.Percolation.bernoulliPolynomial_exact_indicator line 60
  6. theorem OAI.Percolation.bernoulliPolynomial_sole_root_mark line 70
  7. theorem OAI.Percolation.cappedRadius_mark_comparison line 84
  8. theorem OAI.Percolation.finiteMarkedMoment_zero_le_one line 118
  9. theorem OAI.Percolation.finiteCappedRadiusTail_exponential line 131
  10. theorem OAI.Percolation.pairOpenPivotals_symm line 161
  11. theorem OAI.Percolation.pairOpenPivotals_triangle_subset line 172
  12. theorem OAI.Percolation.pairOpenPivotals_triangle line 182
  13. theorem OAI.Percolation.conn_no_crossing_internal line 190
  14. theorem OAI.Percolation.conn_one_attachment_internal line 203
  15. def OAI.Percolation.internalBonds line 223
  16. theorem OAI.Percolation.coe_internalBonds line 226
  17. theorem OAI.Percolation.pairOpenPivotals_one_attachment line 231
  18. theorem OAI.Percolation.conn_first_entry line 256
  19. def OAI.Percolation.pruneContacts line 279
  20. theorem OAI.Percolation.internal_not_cut line 282
  21. theorem OAI.Percolation.exterior_not_cut line 287
  22. theorem OAI.Percolation.internal_pruneContacts line 292
  23. theorem OAI.Percolation.pruneContacts_only_attachment line 300
  24. theorem OAI.Percolation.exists_pruneContacts_root line 306
  25. theorem OAI.Percolation.mem_pairOpenPivotals line 335
  26. theorem OAI.Percolation.pairOpenPivotals_card_le line 342
  27. theorem OAI.Percolation.finiteRootComponent_mono line 371
  28. def OAI.Percolation.openContacts line 381
  29. def OAI.Percolation.BadPieceEvent line 385
  30. theorem OAI.Percolation.badPieceEvent_contact_bound line 394
  31. def OAI.Percolation.incidentBonds line 418
  32. theorem OAI.Percolation.mem_incidentBonds line 421
  33. theorem OAI.Percolation.incidentBonds_card_le line 426
  34. theorem OAI.Percolation.badPieceEvent_pruning line 436
  35. def OAI.Percolation.bernoulliWeight line 498
  36. theorem OAI.Percolation.bernoulliWeight_nonneg line 501
  37. theorem OAI.Percolation.bernoulliWeight_closure_ratio line 505
  38. theorem OAI.Percolation.bernoulliWeight_closure_le line 522
  39. theorem OAI.Percolation.card_small_subsets_le line 533
  40. theorem OAI.Percolation.closure_fiber_card_le line 553
  41. theorem OAI.Percolation.finite_closure_comparison line 577
  42. def OAI.Percolation.finiteBadPieceProbability line 613
  43. theorem OAI.Percolation.bernoulliPolynomial_indicator_weight line 617
  44. theorem OAI.Percolation.finiteBadPieceProbability_le_radius line 627
  45. theorem OAI.Percolation.finiteBadPieceProbability_exponential line 656
  46. def OAI.Percolation.FiniteGoodForScale line 686
  47. def OAI.Percolation.CappedBadGoodnessEvent line 694
  48. def OAI.Percolation.finiteBadGoodnessProbability line 698
  49. theorem OAI.Percolation.cappedBadGoodness_iff line 703
  50. theorem OAI.Percolation.finiteBadGoodnessProbability_le_sum line 728
  51. theorem OAI.Percolation.finiteBadGoodnessProbability_geometric line 747
  52. theorem OAI.Percolation.inverse_mark_cost_le line 796
  53. theorem OAI.Percolation.ghost_scale_estimates line 812
  54. theorem OAI.Percolation.eventually_ghost_scale line 922
  55. theorem OAI.Percolation.ghost_ratio_le_one line 958
  56. theorem OAI.Percolation.finite_bad_goodness_stretched_exp line 984
  57. theorem OAI.Percolation.reachBall_le_step line 1032
  58. theorem OAI.Percolation.reachBall_mono_local line 1035
  59. theorem OAI.Percolation.walk_mem_reachBall line 1038
  60. theorem OAI.Percolation.finite_cluster_subset_reachBall line 1053
  61. theorem OAI.Percolation.cluster_restrict_incident_eq line 1073
  62. theorem OAI.Percolation.cluster_restrict_incident_of_full line 1088
  63. theorem OAI.Percolation.capped_cluster_local line 1095
  64. def OAI.Percolation.pivotalDistance line 1124
  65. def OAI.Percolation.contactSet line 1128
  66. def OAI.Percolation.GoodForScale line 1132
  67. def OAI.Percolation.CappedBadGoodness line 1141
  68. theorem OAI.Percolation.pivotalDistance_finset line 1144
  69. theorem OAI.Percolation.contactSet_finset line 1153
  70. theorem OAI.Percolation.finiteGoodForScale_iff line 1158
  71. theorem OAI.Percolation.cappedBadGoodness_finset_iff line 1169
  72. theorem OAI.Percolation.internal_config_eq_of_incident line 1177
  73. theorem OAI.Percolation.contacts_eq_of_incident line 1187
  74. theorem OAI.Percolation.goodForScale_congr line 1198
  75. theorem OAI.Percolation.goodForScale_restrict_incident line 1210
  76. theorem OAI.Percolation.cappedBadGoodness_local line 1221
  77. theorem OAI.Percolation.measurableSet_finite_restriction line 1248
  78. theorem OAI.Percolation.measurableSet_cappedBadGoodness line 1258
  79. theorem OAI.Percolation.bad_goodness_law_eq_finite line 1269
  80. theorem OAI.Percolation.incident_filter_card_le_degree line 1286
  81. theorem OAI.Percolation.bad_goodness_stretched_exp line 1300