OAI/Probability/UnimodularPercolation/Criticality/Susceptibility.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Susceptibility for bond percolation.

  1. theorem OAI.Percolation.sprinkleParameter_ge_left line 18
  2. theorem OAI.Percolation.susceptibility_sprinkling_gain line 24
  3. theorem OAI.Percolation.rootSusceptibility_sprinkling_gain line 49
  4. def OAI.Percolation.orientedPivotalEvent line 77
  5. theorem OAI.Percolation.measurableSet_orientedPivotalEvent line 80
  6. theorem OAI.Percolation.orientedPivotalEvent_disjoint line 84
  7. theorem OAI.Percolation.closedPivotal_conn line 90
  8. theorem OAI.Percolation.closedPivotal_conn_probability line 113
  9. theorem OAI.Percolation.orientedPivotalEvent_subset_disjoint line 123
  10. theorem OAI.Percolation.distinctClusterMass_eq_pivotal line 151
  11. theorem OAI.Percolation.lintegral_distinctClusterMass line 166
  12. theorem OAI.Percolation.ennreal_distinctClusterMoment line 183
  13. theorem OAI.Percolation.summable_orientedPivotal_pairs line 206
  14. theorem OAI.Percolation.distinctClusterMoment_eq_pivotal line 214
  15. theorem OAI.Percolation.orientedPivotal_probability_covariant line 238
  16. def OAI.Percolation.pivotalTransportMass line 251
  17. theorem OAI.Percolation.pivotalTransportMass_nonneg line 255
  18. theorem OAI.Percolation.pivotalTransportMass_covariant line 259
  19. theorem OAI.Percolation.pivotalTransportMass_incoming_summable line 269
  20. theorem OAI.Percolation.pivotalTransportMass_incoming line 277
  21. theorem OAI.Percolation.pivotalTransportMass_outgoing_summable line 297
  22. theorem OAI.Percolation.rootPivotalMass_eq_neighborMoment line 324
  23. theorem OAI.Percolation.orientedPivotal_probability_le_closed line 353
  24. theorem OAI.Percolation.finite_neighbor_pivotal_le_incident line 362
  25. theorem OAI.Percolation.finite_incident_sum_le_twice line 394
  26. theorem OAI.Percolation.finite_oriented_pivotal_sum_le line 420
  27. theorem OAI.Percolation.eventually_cluster_eq_at_finite line 438
  28. theorem OAI.Percolation.label_cluster_finite_ae_subcritical line 459
  29. theorem OAI.Percolation.susceptibility_eq_label_integral line 467
  30. theorem OAI.Percolation.continuousAt_susceptibility_subcritical line 481
  31. theorem OAI.Percolation.continuousAt_rootSusceptibility_subcritical line 507
  32. theorem OAI.Percolation.summable_orientedPivotal_targets line 526
  33. def OAI.Percolation.finiteRootPivotalMass line 535
  34. theorem OAI.Percolation.finiteRootPivotalMass_nonneg line 540
  35. theorem OAI.Percolation.exists_finiteRootPivotalMass_gt line 549
  36. def OAI.Percolation.vanishingSprinkle line 606
  37. theorem OAI.Percolation.vanishingSprinkle_pos line 614
  38. theorem OAI.Percolation.tendsto_vanishingSprinkle line 618
  39. theorem OAI.Percolation.sprinkle_sequence_gt line 622
  40. theorem OAI.Percolation.tendsto_sprinkle_sequence line 627
  41. theorem OAI.Percolation.tendsto_sprinkle_sequence_right line 633
  42. theorem OAI.Percolation.rootSusceptibility_sequence_slope_lower line 641
  43. theorem OAI.Percolation.frequently_rpow_slope_le_of_sequence line 692
  44. def OAI.Percolation.realRootSusceptibility line 728
  45. theorem OAI.Percolation.realRootSusceptibility_coe line 732
  46. theorem OAI.Percolation.rootSusceptibility_one_le line 737
  47. theorem OAI.Percolation.continuousAt_realRootSusceptibility line 747
  48. theorem OAI.Percolation.rootSusceptibility_power_right_slope line 758
  49. theorem OAI.Percolation.interval_decrease_of_right_slope line 803
  50. theorem OAI.Percolation.right_slope_distance_bound line 820
  51. theorem OAI.Percolation.susceptibility_bound_of_neighborMoment line 859
  52. theorem OAI.Percolation.eventually_upper_interval_unit line 921
  53. theorem OAI.Percolation.susceptibility_growth_of_divergent_moment line 938
  54. theorem OAI.Percolation.exponential_transfer_of_deriv_bound line 982
  55. theorem OAI.Percolation.markedConnection_transfer line 1006
  56. theorem OAI.Percolation.markedConnection_component_polynomial line 1055
  57. theorem OAI.Percolation.one_sub_pow_one_sub_le line 1088
  58. theorem OAI.Percolation.markedConnection_integral line 1111
  59. theorem OAI.Percolation.markedConnection_le_susceptibility line 1123
  60. theorem OAI.Percolation.one_sub_pow_one_sub_ge_half line 1139
  61. theorem OAI.Percolation.clusterWindow_le_markedConnection line 1159