OAI/Probability/UnimodularPercolation/Kernel/DistinctMoments.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

Distinct Moments for bond percolation.

  1. def OAI.Percolation.exposedVertexPotential line 18
  2. theorem OAI.Percolation.integrable_exposedVertexPotential line 22
  3. theorem OAI.Percolation.integral_exposedVertexPotential_le line 32
  4. theorem OAI.Percolation.exposedBoundaryPotential_eq line 46
  5. theorem OAI.Percolation.integral_exposedBoundaryPotential_le line 65
  6. theorem OAI.Percolation.reachBall_ncard_covariant line 92
  7. theorem OAI.Percolation.reachBall_card_le_root_sum line 104
  8. theorem OAI.Percolation.rootNeighborMoment_nonneg line 112
  9. theorem OAI.Percolation.integral_exposedBoundaryPotential_uniform line 119
  10. theorem OAI.Percolation.LocalEndpointRule.kernel_distinctMoment_integral line 155
  11. theorem OAI.Percolation.LocalEndpointRule.integrable_kernel_freshMoment line 168
  12. theorem OAI.Percolation.LocalEndpointRule.kernel_distinctMoment_bound line 179
  13. theorem OAI.Percolation.finite_positive_product_support line 233
  14. theorem OAI.Percolation.finite_positive_product_action line 259
  15. theorem OAI.Percolation.finite_positive_pow_support line 281
  16. theorem OAI.Percolation.positive_identity_action line 297
  17. def OAI.Percolation.realAction line 313
  18. theorem OAI.Percolation.realAction_mono line 316
  19. theorem OAI.Percolation.realAction_affine line 322
  20. theorem OAI.Percolation.realAction_pow_succ line 336
  21. theorem OAI.Percolation.realAction_pow_potential_bound line 345
  22. theorem OAI.Percolation.realAction_pow_potential_at_zero line 371
  23. theorem OAI.Percolation.LocalEndpointRule.normalized_operator_positive line 393
  24. theorem OAI.Percolation.LocalEndpointRule.normalized_operator_finite line 401
  25. theorem OAI.Percolation.LocalEndpointRule.normalized_operator_action line 413
  26. theorem OAI.Percolation.LocalEndpointRule.normalized_operator_row_le line 420
  27. theorem OAI.Percolation.LocalEndpointRule.normalized_operator_row_eq line 432
  28. theorem OAI.Percolation.LocalEndpointRule.normalized_operator_invariant line 442
  29. theorem OAI.Percolation.LocalEndpointRule.normalized_operator_end_support line 450
  30. theorem OAI.Percolation.distinctClusterMoment_self line 469
  31. theorem OAI.Percolation.LocalEndpointRule.normalized_power_distinctMoment_upper line 479
  32. theorem OAI.Percolation.realAction_pow_row_le line 528
  33. theorem OAI.Percolation.positive_pow_end_support line 538
  34. theorem OAI.Percolation.realAction_pow_row_eq_on line 549
  35. def OAI.Percolation.connectedClusterMoment line 578
  36. theorem OAI.Percolation.integrable_connected_cluster_square line 581
  37. theorem OAI.Percolation.distinct_add_connected_cluster_moment line 593
  38. theorem OAI.Percolation.distinctClusterMoment_lower line 607
  39. theorem OAI.Percolation.realAction_connectedMoment_eq_diagonalLoss line 617
  40. theorem OAI.Percolation.realAction_distinctMoment_lower line 650
  41. theorem OAI.Percolation.LocalEndpointRule.normalized_power_moment_sandwich line 706
  42. theorem OAI.Percolation.exists_logarithmic_power line 760
  43. theorem OAI.Percolation.moment_sandwich_power_law line 792
  44. theorem OAI.Percolation.EndpointProfile.exp_neg_H line 847
  45. theorem OAI.Percolation.EndpointProfile.exists_nearby_operators line 852
  46. def OAI.Percolation.EndpointProfile.potentialScale line 890
  47. def OAI.Percolation.EndpointProfile.geometricScale line 893
  48. theorem OAI.Percolation.EndpointProfile.potentialScale_pos line 895
  49. theorem OAI.Percolation.EndpointProfile.geometricScale_two_le line 901
  50. theorem OAI.Percolation.EndpointProfile.log_geometricScale_le line 910
  51. theorem OAI.Percolation.EndpointProfile.eventually_potentialScale_le line 928
  52. theorem OAI.Percolation.EndpointProfile.eventually_neighborMoment_lower line 956
  53. theorem OAI.Percolation.neighborMoment_growth_of_divergent_moment line 1032
  54. theorem OAI.Percolation.measurable_set_union_pair line 1101
  55. theorem OAI.Percolation.measurable_set_insert line 1111
  56. theorem OAI.Percolation.measurableSet_closedPivotal line 1116
  57. def OAI.Percolation.singleSprinkle line 1120
  58. theorem OAI.Percolation.measurableSet_singleSprinkle line 1123
  59. theorem OAI.Percolation.singleSprinkle_disjoint line 1127
  60. theorem OAI.Percolation.singleSprinkle_mem line 1136
  61. theorem OAI.Percolation.singleSprinkle_probability line 1141
  62. theorem OAI.Percolation.event_sprinkling_gain line 1154