OAI/Probability/UnimodularPercolation/Exploration/FractionalMoments.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

Fractional Moments for bond percolation.

  1. theorem OAI.Percolation.sqrt_log_power_bound line 20
  2. theorem OAI.Percolation.markedConnection_power_transfer line 49
  3. def OAI.Percolation.dyadicGhost line 87
  4. theorem OAI.Percolation.dyadicGhost_pos line 90
  5. theorem OAI.Percolation.dyadicGhost_volume line 92
  6. theorem OAI.Percolation.tendsto_dyadicGhost line 96
  7. theorem OAI.Percolation.dyadicGhost_rpow line 99
  8. theorem OAI.Percolation.eventually_dyadic_backstep line 110
  9. theorem OAI.Percolation.critical_dyadic_bound_of_susceptibility line 141
  10. theorem OAI.Percolation.critical_power_integrable_of_dyadic_bound line 184
  11. theorem OAI.Percolation.critical_moment_of_susceptibility_growth line 222
  12. theorem OAI.Percolation.critical_root_power_integrable line 263
  13. theorem OAI.Percolation.measurable_cluster_power line 320
  14. theorem OAI.Percolation.integrable_cluster_power_covariant line 324
  15. theorem OAI.Percolation.integral_cluster_power_covariant line 341
  16. theorem OAI.Percolation.uniform_cluster_power_of_root line 352
  17. theorem OAI.Percolation.cluster_power_mono_integral line 386
  18. def OAI.Percolation.finiteCovariance line 434
  19. def OAI.Percolation.coordinateAverage line 437
  20. def OAI.Percolation.coordinateVariation line 440
  21. theorem OAI.Percolation.bernoulliPolynomial_abs line 443
  22. theorem OAI.Percolation.coordinateVariation_nonneg line 455
  23. theorem OAI.Percolation.finiteCovariance_first_coordinate line 460
  24. theorem OAI.Percolation.coordinateVariation_average_le line 509
  25. theorem OAI.Percolation.finiteCovariance_first_bound line 532
  26. inductive OAI.Percolation.EdgeQueryTree line 576
  27. def OAI.Percolation.EdgeQueryTree.Valid line 582
  28. def OAI.Percolation.EdgeQueryTree.eval line 586
  29. def OAI.Percolation.EdgeQueryTree.value line 590
  30. def OAI.Percolation.EdgeQueryTree.reads line 592
  31. def OAI.Percolation.EdgeQueryTree.revealment line 596
  32. theorem OAI.Percolation.EdgeQueryTree.value_mem line 600
  33. theorem OAI.Percolation.EdgeQueryTree.revealment_nonneg line 604
  34. theorem OAI.Percolation.EdgeQueryTree.eval_congr line 613
  35. theorem OAI.Percolation.EdgeQueryTree.eval_insert line 623
  36. theorem OAI.Percolation.EdgeQueryTree.value_insert line 629
  37. theorem OAI.Percolation.EdgeQueryTree.reads_congr line 633
  38. theorem OAI.Percolation.EdgeQueryTree.reads_mem line 643
  39. theorem OAI.Percolation.finiteCovariance_congr_right line 665
  40. theorem OAI.Percolation.EdgeQueryTree.covariance_bound line 676
  41. theorem OAI.Percolation.EdgeQueryTree.reads_insert line 757
  42. theorem OAI.Percolation.EdgeQueryTree.revealment_eq_probability line 764
  43. def OAI.Percolation.seededEdgeSearch line 802
  44. theorem OAI.Percolation.seededEdgeSearch_valid line 812
  45. theorem OAI.Percolation.seedMarked_singleton_of_no_crossing line 822
  46. theorem OAI.Percolation.seededEdgeSearch_correct line 833
  47. theorem OAI.Percolation.seededEdgeSearch_reads line 860
  48. theorem OAI.Percolation.finiteCovariance_average_right line 891
  49. theorem OAI.Percolation.EdgeQueryTree.randomized_covariance_bound line 908
  50. def OAI.Percolation.finiteSeedProbability line 924
  51. theorem OAI.Percolation.seededEdgeSearch_value line 928
  52. theorem OAI.Percolation.finiteSeedProbability_tree line 939
  53. theorem OAI.Percolation.seededEdgeSearch_reads_endpoints line 957
  54. theorem OAI.Percolation.seededEdgeSearch_mean_revealment_le line 967
  55. theorem OAI.Percolation.finiteSeedProbability_component line 992
  56. theorem OAI.Percolation.one_sub_pow_one_sub_le_power line 1032
  57. theorem OAI.Percolation.markedConnection_le_cluster_power line 1041
  58. theorem OAI.Percolation.finiteSeedProbability_expectation line 1056
  59. theorem OAI.Percolation.finiteSeedProbability_le_cluster_power line 1065
  60. theorem OAI.Percolation.sum_coordinateVariation_eq_deriv line 1086
  61. theorem OAI.Percolation.EdgeQueryTree.randomized_covariance_le_deriv line 1096
  62. theorem OAI.Percolation.seededEdgeSearch_revealment_of_moments line 1113
  63. theorem OAI.Percolation.finiteSeed_covariance_upper line 1134
  64. def OAI.Percolation.finiteClusterTailIndicator line 1161
  65. def OAI.Percolation.finiteClusterTail line 1164
  66. theorem OAI.Percolation.finiteClusterTailIndicator_mono line 1167
  67. theorem OAI.Percolation.finiteClusterTail_nonneg line 1175
  68. theorem OAI.Percolation.finiteClusterTail_deriv_nonneg line 1182
  69. theorem OAI.Percolation.finiteSeed_covariance_lower line 1190