OAI/Probability/UnimodularPercolation/Criticality/Sharpness.lean

GitHub source file

123 declarations, 0 contain sorry, 0 declared as axioms

Finite Russo formulae, exterior exposure and subcritical sharpness.

  1. def OAI.Percolation.bernoulliPolynomial line 20
  2. theorem OAI.Percolation.bernoulliPolynomial_empty line 23
  3. theorem OAI.Percolation.bernoulliPolynomial_congr line 26
  4. theorem OAI.Percolation.bernoulliPolynomial_sub line 33
  5. theorem OAI.Percolation.bernoulliPolynomial_insert line 38
  6. theorem OAI.Percolation.hasDerivAt_bernoulliPolynomial line 69
  7. theorem OAI.Percolation.bernoulliPolynomial_zero line 106
  8. theorem OAI.Percolation.bernoulliPolynomial_const line 109
  9. theorem OAI.Percolation.bernoulliPolynomial_nonneg line 115
  10. theorem OAI.Percolation.bernoulliPolynomial_mono line 123
  11. theorem OAI.Percolation.bernoulliPolynomial_union line 133
  12. theorem OAI.Percolation.bernoulliPolynomial_closed_difference line 153
  13. theorem OAI.Percolation.closed_difference_russo line 169
  14. def OAI.Percolation.finiteEventPolynomial line 179
  15. theorem OAI.Percolation.finiteEventPolynomial_eq line 182
  16. def OAI.Percolation.closedPivotal line 190
  17. theorem OAI.Percolation.closedPivotal_difference line 193
  18. theorem OAI.Percolation.finite_russo_closed line 207
  19. theorem OAI.Percolation.finite_russo_closed_law line 223
  20. theorem OAI.Percolation.conn_insert_iff line 236
  21. def OAI.Percolation.internalEdges line 271
  22. theorem OAI.Percolation.mem_internalEdges_of_ends line 274
  23. def OAI.Percolation.unexposed line 280
  24. theorem OAI.Percolation.unexposed_subset line 283
  25. theorem OAI.Percolation.mem_unexposed_of_conn line 286
  26. theorem OAI.Percolation.conn_restrict_unexposed line 293
  27. theorem OAI.Percolation.unexposed_boundary_closed line 305
  28. theorem OAI.Percolation.unexposed_insert_crossing line 313
  29. theorem OAI.Percolation.not_mem_unexposed_of_conn line 334
  30. theorem OAI.Percolation.conn_sdiff_internal_unexposed line 341
  31. theorem OAI.Percolation.unexposed_sdiff_internal line 352
  32. theorem OAI.Percolation.unexposed_union_internal line 365
  33. theorem OAI.Percolation.unexposed_union_eq_iff line 383
  34. def OAI.Percolation.escapeEvent line 401
  35. theorem OAI.Percolation.escapeEvent_isUpperSet line 404
  36. theorem OAI.Percolation.escape_closed_pivotal_iff line 412
  37. theorem OAI.Percolation.bernoulliPolynomial_add line 438
  38. theorem OAI.Percolation.bernoulliPolynomial_mul_const line 443
  39. theorem OAI.Percolation.bernoulliPolynomial_const_mul line 450
  40. theorem OAI.Percolation.bernoulliPolynomial_sum line 454
  41. theorem OAI.Percolation.bernoulliPolynomial_blocks line 463
  42. theorem OAI.Percolation.bernoulliPolynomial_exposure line 485
  43. def OAI.Percolation.unexposedRegion line 516
  44. theorem OAI.Percolation.coe_unexposedRegion line 519
  45. theorem OAI.Percolation.unexposedRegion_subset line 523
  46. theorem OAI.Percolation.bernoulliPolynomial_partition_region line 530
  47. def OAI.Percolation.internalSupport line 552
  48. theorem OAI.Percolation.internalSupport_subset line 555
  49. theorem OAI.Percolation.internalSupport_union_sdiff line 558
  50. theorem OAI.Percolation.coe_inter_internalSupport line 562
  51. def OAI.Percolation.regionProbability line 570
  52. theorem OAI.Percolation.regionProbability_nonneg line 574
  53. theorem OAI.Percolation.bernoulliPolynomial_exposure_factor line 582
  54. def OAI.Percolation.crossingReach line 607
  55. def OAI.Percolation.crossingCount line 610
  56. def OAI.Percolation.boundaryExpectation line 615
  57. def OAI.Percolation.closedEscapeCount line 620
  58. theorem OAI.Percolation.finite_escape_russo line 624
  59. theorem OAI.Percolation.closedEscapeCount_expectation line 639
  60. theorem OAI.Percolation.finite_escape_complement line 681
  61. theorem OAI.Percolation.finite_escape_differential_lower line 709
  62. theorem OAI.Percolation.bernoulliPolynomial_monotoneOn line 728
  63. theorem OAI.Percolation.crossingCount_mono line 743
  64. theorem OAI.Percolation.boundaryExpectation_nonneg line 756
  65. theorem OAI.Percolation.boundaryExpectation_monotoneOn line 765
  66. theorem OAI.Percolation.boundaryCost_monotoneOn line 771
  67. theorem OAI.Percolation.finiteEventPolynomial_mem_Icc line 778
  68. theorem OAI.Percolation.differential_escape_growth line 794
  69. theorem OAI.Percolation.finite_escape_probability_lower line 834
  70. theorem OAI.Percolation.bernoulliPolynomial_map line 859
  71. theorem OAI.Percolation.finiteEventPolynomial_restrict line 870
  72. theorem OAI.Percolation.bernoulliPolynomial_restrict line 899
  73. def OAI.Percolation.incidentSupport line 916
  74. theorem OAI.Percolation.mem_incidentSupport line 919
  75. theorem OAI.Percolation.incidentSupport_mono line 923
  76. theorem OAI.Percolation.escapeEvent_restrict_incident line 930
  77. theorem OAI.Percolation.finite_escape_eq_law line 953
  78. theorem OAI.Percolation.internal_edge_mem_incident line 962
  79. theorem OAI.Percolation.internalSupport_eq_of_incident_subset line 969
  80. theorem OAI.Percolation.crossingCount_eq_of_incident_subset line 977
  81. theorem OAI.Percolation.boundaryExpectation_eq_of_incident_subset line 988
  82. def OAI.Percolation.boundaryCost line 999
  83. theorem OAI.Percolation.measurableSet_escapeEvent line 1003
  84. theorem OAI.Percolation.escapeEvent_antitone_domain line 1018
  85. def OAI.Percolation.vertexExhaustion line 1025
  86. theorem OAI.Percolation.vertexExhaustion_mono line 1028
  87. theorem OAI.Percolation.subset_vertexExhaustion line 1034
  88. theorem OAI.Percolation.infinite_cluster_eq_iInter_escape line 1041
  89. theorem OAI.Percolation.infinite_cluster_probability_ge_of_escape line 1056
  90. theorem OAI.Percolation.infinite_cluster_probability_pos_of_bad_cost line 1073
  91. theorem OAI.Percolation.pc_le_of_infinite_cluster_probability_pos line 1090
  92. theorem OAI.Percolation.exists_subcritical_testSet line 1101
  93. theorem OAI.Percolation.internalEdges_aut_iff line 1113
  94. theorem OAI.Percolation.crossingReach_aut_iff line 1125
  95. theorem OAI.Percolation.internalSupport_aut line 1143
  96. theorem OAI.Percolation.crossingCount_aut line 1151
  97. theorem OAI.Percolation.boundaryExpectation_aut line 1157
  98. theorem OAI.Percolation.incidentSupport_aut line 1168
  99. theorem OAI.Percolation.boundaryCost_aut line 1185
  100. theorem OAI.Percolation.exists_uniform_subcritical_testSets line 1194
  101. def OAI.Percolation.domainTwoPoint line 1225
  102. theorem OAI.Percolation.conn_internal_endpoint line 1228
  103. def OAI.Percolation.CutExists line 1236
  104. def OAI.Percolation.cutInside line 1239
  105. def OAI.Percolation.cutOutside line 1242
  106. theorem OAI.Percolation.cut_spec line 1245
  107. theorem OAI.Percolation.cut_unique line 1251
  108. theorem OAI.Percolation.crossingReach_cut line 1260
  109. theorem OAI.Percolation.crossingReach_upper line 1270
  110. theorem OAI.Percolation.finiteWitness_crossingReach line 1275
  111. theorem OAI.Percolation.conn_first_exit line 1283
  112. theorem OAI.Percolation.boundaryExpectation_eq_sum line 1317
  113. theorem OAI.Percolation.domainTwoPoint_first_exit line 1337
  114. theorem OAI.Percolation.conn_internal_eq_or_mem line 1387
  115. theorem OAI.Percolation.domainTwoPoint_zero_of_outside line 1397
  116. theorem OAI.Percolation.domainRow_le_boundaryCost line 1407
  117. theorem OAI.Percolation.domainRow_uniform_bound line 1440
  118. theorem OAI.Percolation.internalEdges_mono line 1467
  119. theorem OAI.Percolation.exists_internal_vertexExhaustion line 1470
  120. theorem OAI.Percolation.conn_domain_exhaustion line 1478
  121. theorem OAI.Percolation.tendsto_domainTwoPoint line 1494
  122. theorem OAI.Percolation.subcritical_row_bound line 1513
  123. theorem OAI.Percolation.operatorBounded_of_lt_pc line 1529