OAI/Probability/UnimodularPercolation/Exploration/TailBounds.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

Tail Bounds for bond percolation.

  1. theorem OAI.Percolation.finiteClusterTail_derivative_bound line 18
  2. theorem OAI.Percolation.exponential_transfer_of_deriv_lower line 43
  3. theorem OAI.Percolation.cluster_finite_ae_mono line 74
  4. theorem OAI.Percolation.finiteClusterTail_le_markedConnection line 89
  5. theorem OAI.Percolation.finiteClusterTail_stretched line 108
  6. theorem OAI.Percolation.exists_exp_neg_le_rpow line 153
  7. theorem OAI.Percolation.exp_stretched_power_bound line 189
  8. theorem OAI.Percolation.finiteClusterTail_polynomial_large line 208
  9. theorem OAI.Percolation.finiteClusterTail_le_one line 246
  10. theorem OAI.Percolation.finiteClusterTail_polynomial line 256
  11. theorem OAI.Percolation.natCast_eq_sum_tail line 305
  12. theorem OAI.Percolation.finiteClusterSize_eq_sum_tail line 315
  13. theorem OAI.Percolation.summable_shifted_rpow line 324
  14. theorem OAI.Percolation.finiteClusterSize_bound_of_tail line 329
  15. theorem OAI.Percolation.finite_connection_row_le_size line 350
  16. theorem OAI.Percolation.susceptibility_bound_of_finite_size line 367
  17. theorem OAI.Percolation.susceptibility_power_of_uniform_moment line 399
  18. theorem OAI.Percolation.almost_linear_susceptibility_of_moments line 426
  19. theorem OAI.Percolation.cluster_finite_ae_covariant line 464
  20. theorem OAI.Percolation.almost_linear_susceptibility line 478
  21. def OAI.Percolation.EdgeQueryTree.forget line 517
  22. def OAI.Percolation.EdgeQueryTree.leaf line 521
  23. theorem OAI.Percolation.EdgeQueryTree.leaf_congr line 525
  24. theorem OAI.Percolation.EdgeQueryTree.leaf_insert line 535
  25. theorem OAI.Percolation.EdgeQueryTree.leaf_expectation line 542
  26. def OAI.Percolation.EdgeQueryTree.score line 569
  27. def OAI.Percolation.EdgeQueryTree.queryCount line 572
  28. theorem OAI.Percolation.EdgeQueryTree.score_mgf line 576
  29. theorem OAI.Percolation.EdgeQueryTree.capped_score_mgf line 599
  30. theorem OAI.Percolation.EdgeQueryTree.capped_score_chernoff line 616
  31. theorem OAI.Percolation.EdgeQueryTree.capped_neg_score_chernoff line 635
  32. theorem OAI.Percolation.EdgeQueryTree.capped_score_tail line 656
  33. def OAI.Percolation.EdgeQueryTree.readSet line 698
  34. theorem OAI.Percolation.EdgeQueryTree.mem_readSet line 701
  35. theorem OAI.Percolation.EdgeQueryTree.readSet_query line 704
  36. theorem OAI.Percolation.EdgeQueryTree.score_query line 715
  37. theorem OAI.Percolation.EdgeQueryTree.queryCount_query line 722
  38. theorem OAI.Percolation.EdgeQueryTree.queryCount_eq_card line 727
  39. theorem OAI.Percolation.EdgeQueryTree.score_eq_sum line 745
  40. def OAI.Percolation.IncidencePending line 776
  41. def OAI.Percolation.incidencePick line 779
  42. theorem OAI.Percolation.incidencePick_spec line 782
  43. def OAI.Percolation.incidenceSearch line 788
  44. theorem OAI.Percolation.incidenceSearch_valid line 798
  45. theorem OAI.Percolation.incidenceSearch_cap line 808
  46. structure OAI.Percolation.IncidenceInvariant line 821
  47. theorem OAI.Percolation.incidentBonds_erase line 826
  48. theorem OAI.Percolation.incidencePending_of_mem line 832
  49. theorem OAI.Percolation.IncidenceInvariant.closed_step line 850
  50. theorem OAI.Percolation.IncidenceInvariant.open_step line 857
  51. theorem OAI.Percolation.IncidenceInvariant.no_pending line 875
  52. theorem OAI.Percolation.incidenceSearch_readSet line 907
  53. theorem OAI.Percolation.incidenceInvariant_root line 935
  54. theorem OAI.Percolation.incidenceSearch_completed_score line 955
  55. theorem OAI.Percolation.incidenceSearch_score_tail line 963
  56. theorem OAI.Percolation.cluster_exterior_expectation_bound line 982
  57. def OAI.Percolation.exteriorSearchScore line 1022
  58. theorem OAI.Percolation.exteriorSearchScore_tail line 1028
  59. def OAI.Percolation.contactBonds line 1054
  60. theorem OAI.Percolation.incident_exterior_subset line 1057
  61. theorem OAI.Percolation.incident_exterior_difference line 1065
  62. theorem OAI.Percolation.finiteRootComponent_disjoint line 1086
  63. theorem OAI.Percolation.distinct_contact_closed line 1099
  64. theorem OAI.Percolation.finiteRootComponent_exterior line 1112
  65. theorem OAI.Percolation.incidence_exterior_score_difference line 1133
  66. theorem OAI.Percolation.contactBonds_comm line 1190
  67. theorem OAI.Percolation.ordered_cluster_contact_tail line 1200