OAI/Probability/UnimodularPercolation/Clusters/KernelMoments.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

Kernel Moments for bond percolation.

  1. theorem OAI.Percolation.inducedSusceptibility_nonneg line 18
  2. def OAI.Percolation.deletedBoundaryPotential line 25
  3. theorem OAI.Percolation.deletedBoundaryPotential_nonneg line 30
  4. theorem OAI.Percolation.le_deletedBoundaryPotential line 35
  5. def OAI.Percolation.deletedLocalPotential line 44
  6. theorem OAI.Percolation.deletedLocalPotential_nonneg line 48
  7. theorem OAI.Percolation.short_path_deleted_potential_bound line 59
  8. theorem OAI.Percolation.LocalEndpointRule.summable_mass_action line 102
  9. theorem OAI.Percolation.LocalEndpointRule.summable_kernel_action line 108
  10. theorem OAI.Percolation.LocalEndpointRule.integrable_mass_action line 114
  11. theorem OAI.Percolation.LocalEndpointRule.kernel_action_integral line 121
  12. theorem OAI.Percolation.LocalEndpointRule.mass_action_le line 138
  13. theorem OAI.Percolation.integrable_deletedLocalPotential line 164
  14. theorem OAI.Percolation.integral_deletedLocalPotential_le line 174
  15. theorem OAI.Percolation.LocalEndpointRule.kernel_deleted_potential_bound line 190
  16. theorem OAI.Percolation.orbit_kernel_column_eq_row line 232
  17. theorem OAI.Percolation.operator_norm_le_absolute_sums line 287
  18. def OAI.Percolation.LocalEndpointRule.kernelDifference line 313
  19. def OAI.Percolation.LocalEndpointRule.differenceRow line 315
  20. theorem OAI.Percolation.LocalEndpointRule.kernelDifference_nonneg line 317
  21. theorem OAI.Percolation.LocalEndpointRule.kernelDifference_covariant line 320
  22. theorem OAI.Percolation.LocalEndpointRule.kernelDifference_outside line 325
  23. theorem OAI.Percolation.LocalEndpointRule.kernelDifference_reverse_outside line 330
  24. theorem OAI.Percolation.LocalEndpointRule.kernelDifference_start line 335
  25. theorem OAI.Percolation.LocalEndpointRule.kernelDifference_end line 340
  26. theorem OAI.Percolation.LocalEndpointRule.summable_kernelDifference line 345
  27. theorem OAI.Percolation.LocalEndpointRule.summable_kernelDifference_column line 351
  28. theorem OAI.Percolation.LocalEndpointRule.differenceRow_nonneg line 357
  29. theorem OAI.Percolation.LocalEndpointRule.differenceRow_finite line 360
  30. theorem OAI.Percolation.LocalEndpointRule.kernelDifference_row_le line 366
  31. theorem OAI.Percolation.LocalEndpointRule.norm_sub_le_differenceRow line 376
  32. theorem OAI.Percolation.LocalEndpointRule.exists_normalized_operator_all line 423
  33. theorem OAI.Percolation.LocalEndpointRule.continuousAt_differenceRow line 440
  34. theorem OAI.Percolation.LocalEndpointRule.exists_continuous_normalized_operators line 452
  35. theorem OAI.Percolation.Along.first_entrance line 486
  36. theorem OAI.Percolation.conn_three_disjoint_arms line 508
  37. theorem OAI.Percolation.bk_ennreal line 570
  38. theorem OAI.Percolation.three_arm_bound line 580
  39. theorem OAI.Percolation.three_arm_double_sum_bound line 606
  40. def OAI.Percolation.clusterMass line 642
  41. theorem OAI.Percolation.measurable_clusterMass line 645
  42. theorem OAI.Percolation.clusterMass_eq_ncard line 651
  43. theorem OAI.Percolation.lintegral_clusterMass line 664
  44. theorem OAI.Percolation.clusterMass_sq line 673
  45. theorem OAI.Percolation.lintegral_clusterMass_sq line 684
  46. theorem OAI.Percolation.cluster_second_moment_bound line 702
  47. theorem OAI.Percolation.subcritical_cluster_finite_ae line 722
  48. theorem OAI.Percolation.subcritical_ennreal_row_bound line 733
  49. theorem OAI.Percolation.subcritical_second_moment line 750
  50. def OAI.Percolation.susceptibility line 789

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:115 (same declaration text).

  51. def OAI.Percolation.rootSusceptibility line 792
  52. theorem OAI.Percolation.susceptibility_nonneg line 796
  53. theorem OAI.Percolation.summable_twoPoint_subcritical line 799
  54. theorem OAI.Percolation.ennreal_susceptibility line 805
  55. theorem OAI.Percolation.susceptibility_aut line 815
  56. theorem OAI.Percolation.susceptibility_one_le line 822
  57. theorem OAI.Percolation.rootSusceptibility_nonneg line 831
  58. theorem OAI.Percolation.susceptibility_le_rootSusceptibility line 836
  59. theorem OAI.Percolation.susceptibility_eq_integral line 852
  60. theorem OAI.Percolation.kernel_sum_le_norm_card line 879
  61. theorem OAI.Percolation.kernel_average_le_norm line 902
  62. def OAI.Percolation.binClusterSlice line 919
  63. theorem OAI.Percolation.mem_binClusterSlice line 923
  64. theorem OAI.Percolation.binClusterSlice_eq_of_conn line 930
  65. theorem OAI.Percolation.binClusterSlice_nonempty line 941
  66. theorem OAI.Percolation.binOrbitRowMass_eq_slice line 946
  67. theorem OAI.Percolation.binSizeMass_eq_of_conn line 957
  68. theorem OAI.Percolation.mem_binClusterSlice_iff_mass line 969
  69. theorem OAI.Percolation.binClusterSlice_local line 987
  70. def OAI.Percolation.finiteClassTransport line 1007
  71. theorem OAI.Percolation.finiteClassTransport_nonneg line 1011
  72. theorem OAI.Percolation.finiteClassTransport_row line 1019
  73. theorem OAI.Percolation.finiteClassTransport_column line 1035
  74. theorem OAI.Percolation.finiteClassTransport_column_le line 1050
  75. def OAI.Percolation.binOrbitClass line 1076
  76. theorem OAI.Percolation.mem_binOrbitClass line 1080
  77. theorem OAI.Percolation.binOrbitClass_symm line 1088
  78. theorem OAI.Percolation.binOrbitClass_eq line 1099
  79. theorem OAI.Percolation.binOrbitClass_mass_eq line 1105
  80. theorem OAI.Percolation.binOrbitClass_local line 1109
  81. theorem OAI.Percolation.binOrbitClass_mem_covariant line 1117
  82. theorem OAI.Percolation.binOrbitClass_covariant line 1128
  83. theorem OAI.Percolation.binOrbitClass_reach line 1141
  84. def OAI.Percolation.binDiagonalMass line 1157
  85. theorem OAI.Percolation.binDiagonalMass_nonneg line 1161
  86. theorem OAI.Percolation.binDiagonalMass_local line 1166
  87. theorem OAI.Percolation.binDiagonalMass_integrable line 1174
  88. theorem OAI.Percolation.binDiagonalMass_outside line 1179
  89. theorem OAI.Percolation.binDiagonalMass_outside_column line 1184
  90. theorem OAI.Percolation.binDiagonalMass_row_zero line 1189
  91. theorem OAI.Percolation.binDiagonalMass_column_zero line 1194
  92. theorem OAI.Percolation.binDiagonalMass_covariant line 1199
  93. theorem OAI.Percolation.binDiagonalMass_row line 1213
  94. theorem OAI.Percolation.binDiagonalMass_column line 1219
  95. theorem OAI.Percolation.binDiagonalMass_column_le line 1228