OAI/Probability/UnimodularPercolation/Clusters/Resampling.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

Resampling for bond percolation.

  1. theorem OAI.Percolation.exists_efficient_of_contracting_successor line 19
  2. theorem OAI.Percolation.efficient_endpoint_profiles_of_divergent_moment line 65
  3. def OAI.Percolation.ShortClosedBoundary line 141
  4. theorem OAI.Percolation.bridgeIndex_le_short_trail line 145
  5. theorem OAI.Percolation.ShortClosedBoundary.open_pivotal line 170
  6. theorem OAI.Percolation.ShortClosedBoundary.bridgeIndex_le line 189
  7. def OAI.Percolation.firstOpenBridgeCount line 210
  8. def OAI.Percolation.shortClosedBoundaryCount line 214
  9. theorem OAI.Percolation.firstOpenBridgeCount_le line 218
  10. theorem OAI.Percolation.bernoulliPolynomial_bit_balance line 244
  11. theorem OAI.Percolation.bernoulliPolynomial_closed_count_balance line 287
  12. theorem OAI.Percolation.shortClosedBoundary_erase_first line 314
  13. theorem OAI.Percolation.shortRecoveredBoundaryCount_le line 323
  14. theorem OAI.Percolation.finite_short_boundary_expectation line 335
  15. theorem OAI.Percolation.bernoulliPolynomial_commute line 371
  16. theorem OAI.Percolation.exteriorBonds_union_blocks line 383
  17. theorem OAI.Percolation.cluster_cell_exterior_factor line 398
  18. theorem OAI.Percolation.cluster_cell_incident_probability line 422
  19. def OAI.Percolation.resampleClusterAt line 430
  20. theorem OAI.Percolation.cluster_resample_cell_independent line 436
  21. theorem OAI.Percolation.resampleClusterAt_subset line 468
  22. theorem OAI.Percolation.resampleClusterAt_external line 476
  23. theorem OAI.Percolation.resampled_path_boundary line 487
  24. def OAI.Percolation.resampleRootCluster line 520
  25. theorem OAI.Percolation.resampled_hit_le_boundaryCount line 525
  26. theorem OAI.Percolation.rootCluster_resampling_law line 557
  27. def OAI.Percolation.finiteSusceptibility line 607
  28. theorem OAI.Percolation.finiteSusceptibility_nonneg line 611
  29. theorem OAI.Percolation.rootCluster_resampled_selector line 618
  30. theorem OAI.Percolation.finite_selector_connection_bound line 633
  31. theorem OAI.Percolation.finite_selected_susceptibility_bound line 666
  32. theorem OAI.Percolation.tendsto_bernoulliPolynomial line 699
  33. theorem OAI.Percolation.conn_finite_exhaustion line 708
  34. theorem OAI.Percolation.finite_connection_polynomial_tendsto line 723
  35. def OAI.Percolation.restrictedBondExhaustion line 745
  36. theorem OAI.Percolation.restrictedBondExhaustion_mono line 748
  37. theorem OAI.Percolation.restrictedBondExhaustion_cover line 753
  38. theorem OAI.Percolation.restrictedBondExhaustion_subset line 758
  39. theorem OAI.Percolation.restricted_selector_connection_bound line 778
  40. def OAI.Percolation.restrictedSusceptibility line 807
  41. theorem OAI.Percolation.restrictedTwoPoint_le line 811
  42. theorem OAI.Percolation.summable_restrictedTwoPoint line 816
  43. theorem OAI.Percolation.summable_bernoulliPolynomial line 836
  44. theorem OAI.Percolation.bernoulliPolynomial_tsum line 844
  45. theorem OAI.Percolation.restrictedTwoPoint_symm line 855
  46. theorem OAI.Percolation.restricted_selected_susceptibility_bound line 865
  47. theorem OAI.Percolation.subcritical_selected_susceptibility_bound line 883
  48. def OAI.Percolation.intrinsicBall line 907
  49. theorem OAI.Percolation.mem_intrinsicBall_self line 910
  50. theorem OAI.Percolation.intrinsicBall_subset_reachBall line 913
  51. theorem OAI.Percolation.intrinsicBall_mono line 918
  52. theorem OAI.Percolation.Along.bonds_in_incidentBall line 923
  53. theorem OAI.Percolation.intrinsicBall_restrict line 937
  54. theorem OAI.Percolation.integral_eq_bernoulliPolynomial line 945
  55. theorem OAI.Percolation.intrinsicBall_exists_max line 968
  56. def OAI.Percolation.intrinsicMaximizer line 974
  57. theorem OAI.Percolation.intrinsicMaximizer_spec line 978
  58. def OAI.Percolation.intrinsicPotentialMax line 984
  59. theorem OAI.Percolation.intrinsicPotentialMax_eq line 987
  60. theorem OAI.Percolation.le_intrinsicPotentialMax line 994
  61. def OAI.Percolation.intrinsicBondSupport line 1000
  62. theorem OAI.Percolation.intrinsicBondSupport_coe line 1004
  63. theorem OAI.Percolation.intrinsicBall_domain_restrict line 1011
  64. theorem OAI.Percolation.intrinsicPotentialMax_domain_local line 1021
  65. theorem OAI.Percolation.maximal_restricted_susceptibility_bound line 1044
  66. def OAI.Percolation.inducedSusceptibility line 1071
  67. theorem OAI.Percolation.intrinsicBall_internal_subset line 1075
  68. theorem OAI.Percolation.inducedSusceptibility_max_eq line 1081
  69. theorem OAI.Percolation.maximal_induced_susceptibility_bound line 1093
  70. theorem OAI.Percolation.restrictedTwoPoint_adj_lower line 1115
  71. theorem OAI.Percolation.restrictedTwoPoint_path_lower line 1130
  72. theorem OAI.Percolation.restrictedSusceptibility_nonneg line 1142
  73. theorem OAI.Percolation.restrictedSusceptibility_path_lower line 1146
  74. theorem OAI.Percolation.restrictedSusceptibility_short_path_bound line 1157
  75. theorem OAI.Percolation.conn_short_of_cluster_cap line 1181
  76. theorem OAI.Percolation.Along.last_entrance line 1203