OAI/Probability/UnimodularPercolation/Kernel/Connections.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Connections for bond percolation.

  1. def OAI.Percolation.ClusterWindow line 18
  2. theorem OAI.Percolation.clusterWindow_local line 21
  3. theorem OAI.Percolation.measurableSet_clusterWindow line 38
  4. def OAI.Percolation.clusterWindowProbability line 48
  5. theorem OAI.Percolation.finiteClusterWindowMass_eq line 51
  6. theorem OAI.Percolation.clusterWindowProbability_nonneg line 72
  7. theorem OAI.Percolation.clusterWindowProbability_mono line 75
  8. theorem OAI.Percolation.LocalEndpointRule.finiteClusterWindowMass_amplification line 86
  9. def OAI.Percolation.amplificationMomentFactor line 106
  10. theorem OAI.Percolation.amplificationMomentFactor_pos line 109
  11. theorem OAI.Percolation.LocalEndpointRule.amplificationLoad_moment_factor line 117
  12. theorem OAI.Percolation.LocalEndpointRule.quantitative_amplification_step line 194
  13. def OAI.Percolation.cappedConnectionMass line 267
  14. theorem OAI.Percolation.cappedConnectionMass_nonneg line 271
  15. theorem OAI.Percolation.cappedConnectionMass_support line 279
  16. theorem OAI.Percolation.cappedConnectionMass_le line 291
  17. theorem OAI.Percolation.cappedConnectionMass_local line 303
  18. theorem OAI.Percolation.cappedConnectionMass_covariant line 324
  19. def OAI.Percolation.connectionAdjustedRule line 332
  20. theorem OAI.Percolation.integral_cappedConnectionMass line 374
  21. theorem OAI.Percolation.integral_cappedConnectionMass_bounds line 383
  22. theorem OAI.Percolation.connectionAdjustedRule_success_lower line 427
  23. theorem OAI.Percolation.connectionAdjustedRule_operator line 462
  24. theorem OAI.Percolation.clusterLarge_probability_tendsto_zero line 518
  25. theorem OAI.Percolation.cappedGoodness_failure_le line 530
  26. theorem OAI.Percolation.cappedGoodness_failure_eventually_small line 551
  27. theorem OAI.Percolation.walkKernel_zero_of_not_step line 580
  28. theorem OAI.Percolation.walkKernel_hasSum line 584
  29. theorem OAI.Percolation.walkPower_support line 592
  30. theorem OAI.Percolation.walkPower_hasSum line 616
  31. theorem OAI.Percolation.neighbors_aut_card line 653
  32. theorem OAI.Percolation.walkKernel_covariant line 667
  33. theorem OAI.Percolation.twoPoint_reachBall_lower line 674
  34. lemma OAI.Percolation.finiteKernel_summable_mul line 704
  35. theorem OAI.Percolation.orbit_two_step_return_lower line 714
  36. theorem OAI.Percolation.matrixCoeff_real_symm line 802
  37. theorem OAI.Percolation.finite_positive_square_row line 807
  38. theorem OAI.Percolation.walkPower_finite_support line 827
  39. theorem OAI.Percolation.walkPower_invariant line 836
  40. theorem OAI.Percolation.walkPower_even_orbit_return line 847
  41. theorem OAI.Percolation.starting_endpoint_rule_of_walk line 884
  42. theorem OAI.Percolation.nonamenable_starting_endpoint_rule line 976
  43. theorem OAI.Percolation.finite_partition_square_bound line 1016
  44. theorem OAI.Percolation.vertexOrbit_eq_of_mem line 1042
  45. theorem OAI.Percolation.finite_sameOrbit_pairs_lower line 1054
  46. def OAI.Percolation.binSizeMass line 1084
  47. def OAI.Percolation.binOrbitRowMass line 1087
  48. theorem OAI.Percolation.binMass_eq_of_window line 1090
  49. theorem OAI.Percolation.binMass_zero_of_not_window line 1096
  50. theorem OAI.Percolation.binSizeMass_eq line 1101
  51. theorem OAI.Percolation.binOrbitRowMass_eq line 1113
  52. theorem OAI.Percolation.binOrbitRowMass_nonneg line 1124
  53. theorem OAI.Percolation.binOrbitRowMass_local line 1132
  54. theorem OAI.Percolation.binSizeMass_local line 1141
  55. theorem OAI.Percolation.binOrbitRowMass_covariant line 1150
  56. theorem OAI.Percolation.binSizeMass_covariant line 1158
  57. def OAI.Percolation.binOrbitTransportMass line 1176
  58. theorem OAI.Percolation.binOrbitRowMass_zero line 1179
  59. theorem OAI.Percolation.binOrbitTransportMass_nonneg line 1183
  60. theorem OAI.Percolation.binOrbitTransportMass_column line 1188
  61. theorem OAI.Percolation.binOrbitTransportMass_row line 1217