OAI/Probability/UnimodularPercolation/Exploration/Moments.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Recursive marked moments and exponential estimates.

  1. theorem OAI.Percolation.sum_choose_rank_suffix line 19
  2. theorem OAI.Percolation.cluster_union_external line 73
  3. theorem OAI.Percolation.cluster_union_external_eq_iff line 88
  4. theorem OAI.Percolation.markedEvent_internal_marks line 99
  5. theorem OAI.Percolation.openMarkedPivotal_internal_marks line 109
  6. theorem OAI.Percolation.openMarkedPivotal_insert_cut line 116
  7. theorem OAI.Percolation.mem_markedOpenPivotals line 146
  8. def OAI.Percolation.markedMomentValue line 153
  9. theorem OAI.Percolation.markedMomentValue_succ line 158
  10. theorem OAI.Percolation.conn_mem_searchSupport line 191
  11. theorem OAI.Percolation.markedEvent_searchSupport line 200
  12. theorem OAI.Percolation.markedOpenPivotals_searchSupport line 209
  13. theorem OAI.Percolation.markedMomentValue_searchSupport line 219
  14. theorem OAI.Percolation.markedMomentValue_zero line 228
  15. theorem OAI.Percolation.markedMomentValue_one line 233
  16. def OAI.Percolation.finiteMarkedMoment line 245
  17. theorem OAI.Percolation.finiteMarkedMoment_support line 249
  18. theorem OAI.Percolation.finiteMarkedMoment_first_bound line 261
  19. def OAI.Percolation.exteriorBonds line 274
  20. def OAI.Percolation.exteriorMarks line 277
  21. theorem OAI.Percolation.coe_exteriorBonds line 280
  22. theorem OAI.Percolation.coe_exteriorMarks line 284
  23. theorem OAI.Percolation.markedOpenPivotals_exterior line 289
  24. theorem OAI.Percolation.markedMomentValue_exterior line 315
  25. theorem OAI.Percolation.markedMomentValue_succ_exterior line 337
  26. def OAI.Percolation.cutMomentValue line 365
  27. theorem OAI.Percolation.cut_not_exterior line 375
  28. theorem OAI.Percolation.exteriorBonds_subset_erase line 382
  29. theorem OAI.Percolation.cutMomentValue_blocks line 389
  30. theorem OAI.Percolation.bernoulliPolynomial_empty_indicator line 437
  31. theorem OAI.Percolation.cutMoment_factor line 447
  32. def OAI.Percolation.pivotalSuffixValue line 500
  33. theorem OAI.Percolation.pivotalSuffixValue_insert line 509
  34. def OAI.Percolation.finiteRootComponent line 551
  35. theorem OAI.Percolation.coe_finiteRootComponent line 556
  36. theorem OAI.Percolation.finiteRootComponent_subset line 560
  37. theorem OAI.Percolation.sum_component_partition line 571
  38. theorem OAI.Percolation.pivotalSuffixValue_component_sum line 589
  39. theorem OAI.Percolation.bernoulliPolynomial_open_gate line 611
  40. def OAI.Percolation.cutCoefficient line 632
  41. theorem OAI.Percolation.finiteMarkedMoment_recursion line 638
  42. theorem OAI.Percolation.cutCoefficient_nonneg line 679
  43. theorem OAI.Percolation.finiteMarkedMoment_nonneg line 686
  44. theorem OAI.Percolation.exterior_mark_support line 696
  45. theorem OAI.Percolation.exterior_degree_bound line 714
  46. theorem OAI.Percolation.finiteMarkedMoment_geometric line 724
  47. theorem OAI.Percolation.choose_generating_sum line 778
  48. theorem OAI.Percolation.markedMomentValue_generating line 788
  49. def OAI.Percolation.finiteMarkedGenerating line 797
  50. def OAI.Percolation.finiteMarkedTail line 802
  51. theorem OAI.Percolation.finiteMarkedTail_nonneg line 807
  52. theorem OAI.Percolation.finiteMarkedGenerating_eq line 815
  53. theorem OAI.Percolation.half_geometric_sum_le line 823
  54. theorem OAI.Percolation.finiteMarkedGenerating_le line 834
  55. theorem OAI.Percolation.finiteMarkedTail_markov line 863
  56. theorem OAI.Percolation.log_one_add_half_inv_ge line 882
  57. theorem OAI.Percolation.finiteMarkedTail_exponential line 897