OAI/Probability/UnimodularPercolation/Clusters/LargeContacts.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

Large Contacts for bond percolation.

  1. theorem OAI.Percolation.cluster_contact_tail line 19
  2. theorem OAI.Percolation.cluster_exterior_weighted_bound line 72
  3. theorem OAI.Percolation.finiteClusterTail_domain_mono line 86
  4. theorem OAI.Percolation.two_large_clusters_tail line 96
  5. theorem OAI.Percolation.finiteClusterTail_of_endpoint_moment line 143
  6. theorem OAI.Percolation.two_large_clusters_of_endpoint_moment line 170
  7. theorem OAI.Percolation.contactBonds_card_le line 203
  8. def OAI.Percolation.clusterContactBin line 215
  9. theorem OAI.Percolation.clusterContactBin_bound line 224
  10. theorem OAI.Percolation.exists_stretched_exp_volume_bound line 275
  11. theorem OAI.Percolation.contact_tail_exponent line 297
  12. theorem OAI.Percolation.clusterContactBin_power_bound line 319
  13. def OAI.Percolation.closedContactSet line 389
  14. def OAI.Percolation.clusterContactCount line 392
  15. def OAI.Percolation.fullContactBin line 395
  16. theorem OAI.Percolation.contactSet_subset_incident line 400
  17. theorem OAI.Percolation.coe_contactBonds_eq line 405
  18. theorem OAI.Percolation.contactSet_ncard_le line 414
  19. theorem OAI.Percolation.fullContactBin_nonneg line 431
  20. theorem OAI.Percolation.fullContactBin_le line 434
  21. theorem OAI.Percolation.measurable_clusterContactCount line 455
  22. theorem OAI.Percolation.measurable_fullContactBin line 476
  23. theorem OAI.Percolation.coe_domainBits line 485
  24. theorem OAI.Percolation.domainBits_local line 488
  25. theorem OAI.Percolation.domainBits_of_subset line 494
  26. theorem OAI.Percolation.integral_domainBits line 499
  27. theorem OAI.Percolation.fullContactBin_eq_finite line 517
  28. theorem OAI.Percolation.clusterContactBin_norm_le line 544
  29. theorem OAI.Percolation.fullContactBin_integral_le_of_finite line 553
  30. theorem OAI.Percolation.fullContactBin_power_bound line 600
  31. theorem OAI.Percolation.integrable_fullContactBin line 624
  32. theorem OAI.Percolation.integral_le_tsum_majorants line 643
  33. theorem OAI.Percolation.dyadic_rpow_identity line 661
  34. theorem OAI.Percolation.dyadic_rpow_summable line 666
  35. theorem OAI.Percolation.dyadic_rpow_sum line 672
  36. def OAI.Percolation.fullLargeContact line 688
  37. theorem OAI.Percolation.fullLargeContact_nonneg line 692
  38. theorem OAI.Percolation.measurable_fullLargeContact line 695
  39. theorem OAI.Percolation.fullLargeContact_le_dyadic line 703
  40. theorem OAI.Percolation.fullLargeContact_bound_of_bins line 728
  41. theorem OAI.Percolation.incident_ncard_le_degree line 763
  42. theorem OAI.Percolation.fullLargeContact_power_bound line 770
  43. theorem OAI.Percolation.critical_large_contact_bound line 790
  44. theorem OAI.Percolation.enn_sum_iSup_nat line 831
  45. theorem OAI.Percolation.enn_tsum_iSup_nat line 841
  46. theorem OAI.Percolation.RootTransport.ennreal line 849
  47. def OAI.Percolation.clusterAveragingKernel line 940
  48. theorem OAI.Percolation.measurable_clusterAveragingKernel line 943
  49. theorem OAI.Percolation.clusterAveragingKernel_symm line 949
  50. theorem OAI.Percolation.cluster_ncard_pos line 956
  51. theorem OAI.Percolation.clusterAveragingKernel_row line 960
  52. theorem OAI.Percolation.clusterAveragingKernel_column line 972
  53. theorem OAI.Percolation.clusterAveragingKernel_aut line 977
  54. theorem OAI.Percolation.root_cluster_average line 984
  55. def OAI.Percolation.clusterPairKernel line 1031
  56. def OAI.Percolation.clusterPairDensity line 1037
  57. def OAI.Percolation.clusterPairFunctional line 1042
  58. theorem OAI.Percolation.cluster_weighted_resum line 1047
  59. theorem OAI.Percolation.clusterPairDensity_reroot_pointwise line 1063
  60. theorem OAI.Percolation.clusterPairFunctional_reroot line 1120
  61. def OAI.Percolation.clusterPairMass line 1171
  62. theorem OAI.Percolation.clusterPairDensity_eq_tsum line 1176
  63. theorem OAI.Percolation.clusterPairMass_swap line 1181
  64. theorem OAI.Percolation.measurable_clusterPairMass line 1187
  65. theorem OAI.Percolation.clusterPairFunctional_swap line 1195