OAI/Probability/CriticalPercolation/Exploration/ClosedFresh.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalPercolation.LazyDFS.exhaustive_mapTarget line 20
  2. lemma OAI.CriticalPercolation.LazyDFS.mapState_initial line 32
  3. theorem OAI.CriticalPercolation.LazyDFS.search_reads_targetWiring line 38
  4. theorem OAI.CriticalPercolation.LazyDFS.search_target_pivotal_moments line 68
  5. def OAI.CriticalPercolation.SearchTree.ClosedFresh line 96
  6. lemma OAI.CriticalPercolation.SearchTree.closedFresh_pin line 101
  7. def OAI.CriticalPercolation.SearchTree.contactScore line 110
  8. def OAI.CriticalPercolation.SearchTree.terminalProbability line 118
  9. lemma OAI.CriticalPercolation.SearchTree.contact_mean_step line 126
  10. lemma OAI.CriticalPercolation.SearchTree.terminal_mean_step line 140
  11. theorem OAI.CriticalPercolation.SearchTree.contact_mean_terminal line 147
  12. lemma OAI.CriticalPercolation.SearchTree.terminalProbability_nonneg line 175
  13. theorem OAI.CriticalPercolation.SearchTree.contact_mean_le_prob line 186
  14. lemma OAI.CriticalPercolation.SearchTree.expect_square_add_const line 197
  15. theorem OAI.CriticalPercolation.SearchTree.contact_second_le_three_mean line 204