OAI/Probability/UnimodularPercolation/Deformation/ClusterProducts.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

Cluster Products for bond percolation.

  1. theorem OAI.Percolation.exists_deformedOperator_small_change line 20
  2. def OAI.Percolation.closedBondNeighborhood line 89
  3. def OAI.Percolation.SimpleVisit line 92
  4. theorem OAI.Percolation.SimpleVisit.mono line 95
  5. theorem OAI.Percolation.walk_conn_restrict_vertices line 104
  6. theorem OAI.Percolation.conn_restrict_of_no_simpleVisit line 114
  7. theorem OAI.Percolation.RawCorridor.counted_support_subset_walk line 124
  8. theorem OAI.Percolation.simplePath_disjoint_at line 140
  9. theorem OAI.Percolation.conn_delete_of_no_visit line 168
  10. theorem OAI.Percolation.RawCorridor.counted_before_deletion_of_no_visit line 183
  11. theorem OAI.Percolation.deformedConnection_no_visit line 232
  12. theorem OAI.Percolation.deformedConnection_deletion_pointwise line 260
  13. theorem OAI.Percolation.deformedKernel_deletion_bound line 289
  14. def OAI.Percolation.deformedSusceptibility line 339
  15. theorem OAI.Percolation.deformedKernel_le_twoPoint line 343
  16. theorem OAI.Percolation.summable_deformedKernel line 355
  17. theorem OAI.Percolation.deformedSusceptibility_le line 364
  18. theorem OAI.Percolation.summable_twoPoint_restricted_pair line 384
  19. theorem OAI.Percolation.twoPoint_double_restricted_bound line 391
  20. theorem OAI.Percolation.deformedSusceptibility_deletion line 413
  21. theorem OAI.Percolation.conn_of_open_incident line 442
  22. theorem OAI.Percolation.conn_restrict_away_from_cluster line 456
  23. theorem OAI.Percolation.conn_delete_cluster line 465
  24. theorem OAI.Percolation.RawCorridor.counted_delete_other_cluster line 478
  25. theorem OAI.Percolation.corridorPenalty_delete_other_cluster line 533
  26. theorem OAI.Percolation.deformedConnection_delete_other_cluster line 545
  27. def OAI.Percolation.deformedClusterMass line 566
  28. theorem OAI.Percolation.deformedClusterMass_delete_other_cluster line 570
  29. theorem OAI.Percolation.deformedConnection_le_conn line 577
  30. theorem OAI.Percolation.measurable_deformedClusterMass line 586
  31. theorem OAI.Percolation.deformedConnection_finite_support line 602
  32. theorem OAI.Percolation.deformedClusterMass_nonneg line 612
  33. theorem OAI.Percolation.deformedClusterMass_le_ncard line 617
  34. theorem OAI.Percolation.integrable_deformedClusterMass line 630
  35. theorem OAI.Percolation.deformedSusceptibility_eq_integral line 643
  36. def OAI.Percolation.OpenClosed line 665
  37. theorem OAI.Percolation.openClosed_cluster line 668
  38. theorem OAI.Percolation.conn_restrict_openClosed line 673
  39. theorem OAI.Percolation.RawCorridor.counted_restrict_openClosed line 690
  40. theorem OAI.Percolation.corridorPenalty_restrict_openClosed line 736
  41. theorem OAI.Percolation.deformedConnection_restrict_openClosed line 745
  42. theorem OAI.Percolation.deformedClusterMass_restrict_openClosed line 761
  43. theorem OAI.Percolation.deformedClusterMass_restrict_config line 768
  44. theorem OAI.Percolation.restriction_functions_independent line 794
  45. theorem OAI.Percolation.integral_mul_disjoint_coordinates line 808
  46. theorem OAI.Percolation.induced_cluster_restrict_incident_iff line 826
  47. theorem OAI.Percolation.weighted_cluster_cell_local line 833
  48. theorem OAI.Percolation.weighted_cluster_cell_exposure line 858
  49. theorem OAI.Percolation.integral_induced_cluster_finite_partition line 894
  50. theorem OAI.Percolation.deformedClusterMass_eq_zero_of_not_mem line 945
  51. theorem OAI.Percolation.deformed_distinct_product_eq_exterior line 950
  52. theorem OAI.Percolation.integrable_deformed_product line 961
  53. theorem OAI.Percolation.integrable_distinct_deformed_product line 978
  54. def OAI.Percolation.deformedFreshExteriorMoment line 1005
  55. theorem OAI.Percolation.deformedSusceptibility_nonneg line 1010
  56. theorem OAI.Percolation.deformedFreshExteriorMoment_eq_tsum line 1015
  57. theorem OAI.Percolation.integrable_deformedFreshExteriorMoment line 1028
  58. theorem OAI.Percolation.integral_deformedFreshExteriorMoment line 1067
  59. theorem OAI.Percolation.summable_three_arm_pair line 1111
  60. theorem OAI.Percolation.three_arm_real_bound line 1121
  61. theorem OAI.Percolation.integral_size_membership_le line 1141
  62. theorem OAI.Percolation.finset_sum_union_le line 1180
  63. theorem OAI.Percolation.finset_sum_biUnion_le line 1186
  64. theorem OAI.Percolation.closedBondNeighborhood_finset line 1195
  65. theorem OAI.Percolation.neighborhood_mass_le line 1211