OAI/Probability/CriticalPercolation/Exploration/Visits.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.QueryTree.visits line 21
  2. lemma OAI.CriticalPercolation.QueryTree.response_run line 24
  3. lemma OAI.CriticalPercolation.QueryTree.bit_not_mem line 45
  4. lemma OAI.CriticalPercolation.QueryTree.nodeMass_push line 56
  5. lemma OAI.CriticalPercolation.QueryTree.nodeTrueMass_push line 63
  6. lemma OAI.CriticalPercolation.QueryTree.quadratic_charge_eq_sum line 74
  7. inductive OAI.CriticalPercolation.MarkedTree line 89
  8. def OAI.CriticalPercolation.MarkedTree.bare line 96
  9. def OAI.CriticalPercolation.MarkedTree.nodeLabel line 100
  10. def OAI.CriticalPercolation.MarkedTree.trace line 106
  11. def OAI.CriticalPercolation.MarkedTree.map line 110
  12. lemma OAI.CriticalPercolation.MarkedTree.trace_map line 114
  13. lemma OAI.CriticalPercolation.MarkedTree.trace_bits line 120
  14. def OAI.CriticalPercolation.MarkedTree.append line 126
  15. lemma OAI.CriticalPercolation.MarkedTree.trace_append line 130
  16. def OAI.CriticalPercolation.MarkedTree.sequence line 136
  17. lemma OAI.CriticalPercolation.MarkedTree.trace_sequence line 140
  18. abbrev OAI.CriticalPercolation.MarkedTree.Cache line 148
  19. def OAI.CriticalPercolation.MarkedTree.Compatible line 150
  20. lemma OAI.CriticalPercolation.MarkedTree.compatible_update line 153
  21. def OAI.CriticalPercolation.MarkedTree.cached line 161
  22. def OAI.CriticalPercolation.MarkedTree.fresh line 171
  23. lemma OAI.CriticalPercolation.MarkedTree.update_compatible_value line 177
  24. lemma OAI.CriticalPercolation.MarkedTree.trace_cached line 184
  25. def OAI.CriticalPercolation.MarkedTree.domain line 206
  26. lemma OAI.CriticalPercolation.MarkedTree.mem_domain line 210
  27. lemma OAI.CriticalPercolation.MarkedTree.domain_update line 213
  28. lemma OAI.CriticalPercolation.MarkedTree.cached_valid line 220
  29. lemma OAI.CriticalPercolation.MarkedTree.cached_empty_valid line 237