OAI/Probability/UnimodularPercolation/Clusters/ExteriorMoments.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

Exterior Moments for bond percolation.

  1. def OAI.Percolation.binDiagonalKernel line 18
  2. theorem OAI.Percolation.binDiagonalKernel_covariant line 22
  3. theorem OAI.Percolation.binDiagonalKernel_row_integral line 33
  4. theorem OAI.Percolation.binDiagonalKernel_column_integral line 44
  5. theorem OAI.Percolation.integral_binDiagonalLoss line 53
  6. theorem OAI.Percolation.integral_binDiagonalLoss_le line 85
  7. def OAI.Percolation.fullOrbitClass line 122
  8. def OAI.Percolation.diagonalLossMass line 125
  9. theorem OAI.Percolation.binSizeMass_zero line 129
  10. theorem OAI.Percolation.binOrbitClass_eq_full line 133
  11. theorem OAI.Percolation.dyadic_window_iff line 138
  12. theorem OAI.Percolation.dyadic_binSizeMass_sq line 152
  13. theorem OAI.Percolation.dyadic_binDiagonalMass line 167
  14. theorem OAI.Percolation.diagonalLossMass_nonneg line 185
  15. theorem OAI.Percolation.diagonalLossMass_le line 189
  16. theorem OAI.Percolation.integral_le_of_discrete_strata line 206
  17. theorem OAI.Percolation.integral_diagonalLoss_le line 266
  18. theorem OAI.Percolation.subcritical_diagonalLoss_le line 303
  19. theorem OAI.Percolation.second_moment_le_rootSusceptibility_cube line 334
  20. theorem OAI.Percolation.diagonalLoss_le_rootSusceptibility_cube line 362
  21. def OAI.Percolation.diagonalLossTerm line 393
  22. theorem OAI.Percolation.diagonalLossTerm_nonneg line 397
  23. theorem OAI.Percolation.diagonalLossTerm_le line 405
  24. theorem OAI.Percolation.diagonalLossMass_eq_tsum line 413
  25. theorem OAI.Percolation.integrable_diagonalLossTerm line 433
  26. theorem OAI.Percolation.integral_diagonalLoss_eq_series line 450
  27. theorem OAI.Percolation.exists_rootSusceptibility_lower line 497
  28. theorem OAI.Percolation.association_finiteWitness_ennreal line 548
  29. theorem OAI.Percolation.clusterMass_mul line 557
  30. theorem OAI.Percolation.lintegral_clusterMass_mul line 568
  31. theorem OAI.Percolation.clusterMass_association line 585
  32. theorem OAI.Percolation.subcritical_cluster_association line 601
  33. theorem OAI.Percolation.integral_mul_finite_local line 646
  34. theorem OAI.Percolation.complement_incidentSupport line 687
  35. theorem OAI.Percolation.cluster_restrict_incident_eq_iff line 700
  36. theorem OAI.Percolation.measurableSet_cluster_eq line 710
  37. theorem OAI.Percolation.cluster_cell_finite_exterior_independence line 724
  38. theorem OAI.Percolation.measurableSet_restrictedConn line 755
  39. theorem OAI.Percolation.integral_event_indicator line 761
  40. theorem OAI.Percolation.cluster_cell_exterior_connection_independent line 767
  41. theorem OAI.Percolation.conn_exterior_of_cluster_eq line 828
  42. theorem OAI.Percolation.cluster_size_eq_tsum_real line 843
  43. theorem OAI.Percolation.integral_cluster_size_event line 854
  44. theorem OAI.Percolation.cluster_cell_exterior_susceptibility line 902
  45. theorem OAI.Percolation.restrictedSusceptibility_le_susceptibility line 945
  46. theorem OAI.Percolation.inducedSusceptibility_le_susceptibility line 953
  47. theorem OAI.Percolation.tsum_cluster_cells line 973
  48. theorem OAI.Percolation.integral_cluster_finite_partition line 982
  49. def OAI.Percolation.freshExteriorMoment line 1032
  50. theorem OAI.Percolation.freshExteriorMoment_eq_tsum line 1036
  51. theorem OAI.Percolation.measurable_freshExteriorMoment line 1048
  52. theorem OAI.Percolation.freshExteriorMoment_nonneg line 1056
  53. theorem OAI.Percolation.integrable_freshExteriorMoment line 1060
  54. theorem OAI.Percolation.integrable_distinct_cluster_product line 1070
  55. theorem OAI.Percolation.integral_freshExteriorMoment line 1087
  56. def OAI.Percolation.distinctClusterMoment line 1130
  57. theorem OAI.Percolation.distinctClusterMoment_nonneg line 1133
  58. theorem OAI.Percolation.cluster_ncard_covariant line 1140
  59. theorem OAI.Percolation.distinctClusterMoment_covariant line 1145
  60. def OAI.Percolation.neighborClusterMoment line 1158
  61. theorem OAI.Percolation.neighborClusterMoment_nonneg line 1162
  62. theorem OAI.Percolation.neighbors_covariant line 1166
  63. theorem OAI.Percolation.neighborClusterMoment_covariant line 1178
  64. def OAI.Percolation.rootNeighborMoment line 1185
  65. theorem OAI.Percolation.neighborMoment_le_rootMoment line 1189