OAI/Probability/UnimodularPercolation/Exploration/Marked.lean

GitHub source file

107 declarations, 0 contain sorry, 0 declared as axioms

Marked decision trees, graph searches and pivotal geometry.

  1. theorem OAI.Percolation.centered_bernoulli_mgf_le line 18
  2. inductive OAI.Percolation.ProbeTree line 38
  3. def OAI.Percolation.ProbeTree.Leaf line 45
  4. instance OAI.Percolation.ProbeTree.leafFintype line 50
  5. def OAI.Percolation.ProbeTree.weight line 55
  6. def OAI.Percolation.ProbeTree.score line 62
  7. def OAI.Percolation.ProbeTree.queries line 69
  8. def OAI.Percolation.ProbeTree.outcome line 76
  9. lemma OAI.Percolation.ProbeTree.weight_nonneg line 83
  10. lemma OAI.Percolation.ProbeTree.sum_weight line 96
  11. theorem OAI.Percolation.ProbeTree.score_mgf line 109
  12. def OAI.Percolation.ProbeTree.successWeight line 154
  13. def OAI.Percolation.ProbeTree.successMass line 157
  14. def OAI.Percolation.ProbeTree.successScore line 160
  15. def OAI.Percolation.ProbeTree.successQueries line 163
  16. lemma OAI.Percolation.ProbeTree.successWeight_nonneg line 166
  17. lemma OAI.Percolation.ProbeTree.successWeight_le line 171
  18. lemma OAI.Percolation.ProbeTree.successMass_nonneg line 178
  19. lemma OAI.Percolation.ProbeTree.successMass_le_one line 181
  20. lemma OAI.Percolation.ProbeTree.successQueries_nonneg line 185
  21. theorem OAI.Percolation.ProbeTree.conditional_score_bound line 189
  22. def OAI.Percolation.ProbeTree.dweight line 223
  23. lemma OAI.Percolation.ProbeTree.hasDerivAt_weight line 230
  24. lemma OAI.Percolation.ProbeTree.score_eq_derivative line 245
  25. theorem OAI.Percolation.ProbeTree.successScore_eq_deriv line 259
  26. inductive OAI.Percolation.ProbeTree.IsMarkSearch line 277
  27. def OAI.Percolation.ProbeTree.marks line 282
  28. def OAI.Percolation.ProbeTree.successMarks line 289
  29. lemma OAI.Percolation.ProbeTree.successMass_edge line 292
  30. lemma OAI.Percolation.ProbeTree.successMass_mark line 297
  31. lemma OAI.Percolation.ProbeTree.successMass_done line 302
  32. lemma OAI.Percolation.ProbeTree.successMarks_edge line 306
  33. lemma OAI.Percolation.ProbeTree.successMarks_mark line 311
  34. lemma OAI.Percolation.ProbeTree.successMarks_done line 319
  35. theorem OAI.Percolation.ProbeTree.marks_times_parameter_le line 323
  36. theorem OAI.Percolation.ProbeTree.successQueries_times_parameter_le line 338
  37. theorem OAI.Percolation.ProbeTree.marked_score_bound line 356
  38. inductive OAI.Percolation.LabelledTree line 382
  39. def OAI.Percolation.LabelledTree.forget line 389
  40. def OAI.Percolation.LabelledTree.eval line 394
  41. def OAI.Percolation.LabelledTree.Valid line 399
  42. theorem OAI.Percolation.LabelledTree.eval_congr line 404
  43. lemma OAI.Percolation.LabelledTree.eval_insert_edge line 423
  44. lemma OAI.Percolation.LabelledTree.eval_insert_mark line 431
  45. theorem OAI.Percolation.bernoulliPolynomial_affine line 441
  46. theorem OAI.Percolation.LabelledTree.expectation_eq line 450
  47. def OAI.Percolation.SearchCrossing line 512
  48. def OAI.Percolation.searchCrossing line 515
  49. theorem OAI.Percolation.searchCrossing_spec line 518
  50. def OAI.Percolation.SearchAvailable line 526
  51. def OAI.Percolation.clusterSearch line 529
  52. lemma OAI.Percolation.searchAvailable_erase line 538
  53. lemma OAI.Percolation.searchAvailable_discover line 542
  54. theorem OAI.Percolation.clusterSearch_valid line 552
  55. theorem OAI.Percolation.clusterSearch_markSearch line 565
  56. def OAI.Percolation.SeedMarked line 576
  57. theorem OAI.Percolation.seedMarked_insert_edge line 579
  58. theorem OAI.Percolation.seedMarked_false_of_no_crossing line 595
  59. theorem OAI.Percolation.clusterSearch_correct line 610
  60. def OAI.Percolation.ProbeTree.Budget line 655
  61. lemma OAI.Percolation.ProbeTree.budget_done line 657
  62. lemma OAI.Percolation.ProbeTree.budget_mono line 661
  63. lemma OAI.Percolation.ProbeTree.budget_edge line 664
  64. lemma OAI.Percolation.ProbeTree.budget_mark line 671
  65. def OAI.Percolation.queryPotential line 682
  66. lemma OAI.Percolation.queryPotential_erase line 685
  67. lemma OAI.Percolation.queryPotential_insert line 690
  68. lemma OAI.Percolation.filtered_degree_erase line 695
  69. lemma OAI.Percolation.queryPotential_discover_card line 704
  70. theorem OAI.Percolation.clusterSearch_budget line 713
  71. def OAI.Percolation.searchVertices line 739
  72. lemma OAI.Percolation.mem_searchVertices line 742
  73. def OAI.Percolation.markedClusterTree line 746
  74. lemma OAI.Percolation.markedClusterTree_available line 749
  75. theorem OAI.Percolation.markedClusterTree_valid line 756
  76. theorem OAI.Percolation.markedClusterTree_budget line 760
  77. theorem OAI.Percolation.markedClusterTree_correct line 767
  78. theorem OAI.Percolation.quadratic_test_bound line 785
  79. def OAI.Percolation.markedConnectionPolynomial line 799
  80. theorem OAI.Percolation.markedConnectionPolynomial_eq_tree line 804
  81. theorem OAI.Percolation.markedConnectionPolynomial_ge_mark line 815
  82. theorem OAI.Percolation.markedConnection_derivative_bound line 824
  83. theorem OAI.Percolation.bernoulliPolynomial_open_difference line 861
  84. def OAI.Percolation.markedOpenPivotals line 881
  85. def OAI.Percolation.markedPivotalMomentOne line 887
  86. theorem OAI.Percolation.marked_pivotal_russo line 892
  87. theorem OAI.Percolation.marked_pivotal_first_moment line 926
  88. def OAI.Percolation.MarkedEvent line 941
  89. def OAI.Percolation.OpenMarkedPivotal line 945
  90. theorem OAI.Percolation.markedEvent_mono line 949
  91. theorem OAI.Percolation.edge_cluster_sides line 954
  92. theorem OAI.Percolation.conn_restrict_cluster_compl line 961
  93. theorem OAI.Percolation.conn_restrict_cluster line 972
  94. theorem OAI.Percolation.openMarkedPivotal_oriented line 984
  95. theorem OAI.Percolation.pivotal_rootSide_disjoint_marks line 1005
  96. theorem OAI.Percolation.conn_delete_internal_of_outside line 1012
  97. theorem OAI.Percolation.pivotal_other_sides line 1028
  98. theorem OAI.Percolation.conn_delete_exterior_of_inside line 1043
  99. theorem OAI.Percolation.pivotal_rootSide_ssubset line 1057
  100. theorem OAI.Percolation.pivotal_rootSides_nested line 1073
  101. theorem OAI.Percolation.conn_restrict_cluster_compl_of_subset line 1091
  102. theorem OAI.Percolation.markedEvent_after_pivotal line 1104
  103. theorem OAI.Percolation.openMarkedPivotal_exterior_iff line 1140
  104. theorem OAI.Percolation.cluster_finite_of_finite_edges line 1163
  105. def OAI.Percolation.pivotalRank line 1177
  106. theorem OAI.Percolation.pivotalRank_injective line 1180
  107. theorem OAI.Percolation.pivotalRank_lt_iff line 1191