OAI/Probability/CriticalPercolation/Exploration/Initial2.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.ExactExposure.initial line 26
  2. def OAI.CriticalPercolation.ExactExposure.search line 27
  3. lemma OAI.CriticalPercolation.ExactExposure.initial_consistent line 31
  4. lemma OAI.CriticalPercolation.ExactExposure.initial_sound line 37
  5. lemma OAI.CriticalPercolation.ExactExposure.search_valid line 42
  6. lemma OAI.CriticalPercolation.ExactExposure.search_reached line 45
  7. lemma OAI.CriticalPercolation.ExactExposure.search_reads line 68
  8. def OAI.CriticalPercolation.ExactExposure.pair line 90
  9. lemma OAI.CriticalPercolation.ExactExposure.pair_reads line 93
  10. def OAI.CriticalPercolation.SearchTree.bare line 104
  11. lemma OAI.CriticalPercolation.SearchTree.bare_reads line 108
  12. lemma OAI.CriticalPercolation.SearchTree.bare_valid line 113
  13. lemma OAI.CriticalPercolation.SearchTree.bare_run_eq line 119