OAI/Probability/CriticalPercolation/Exploration/QueryTree.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.CriticalPercolation.QueryTree line 21
  2. def OAI.CriticalPercolation.QueryTree.Leaf line 28
  3. instance OAI.CriticalPercolation.QueryTree.leafFintype line 32
  4. def OAI.CriticalPercolation.QueryTree.run line 36
  5. def OAI.CriticalPercolation.QueryTree.reads line 40
  6. def OAI.CriticalPercolation.QueryTree.Valid line 44
  7. def OAI.CriticalPercolation.QueryTree.reference line 48
  8. lemma OAI.CriticalPercolation.QueryTree.reference_pos line 53
  9. lemma OAI.CriticalPercolation.QueryTree.reference_sum line 64
  10. def OAI.CriticalPercolation.QueryTree.charge line 73
  11. lemma OAI.CriticalPercolation.QueryTree.charge_mono line 81
  12. lemma OAI.CriticalPercolation.QueryTree.charge_const_mul line 102
  13. theorem OAI.CriticalPercolation.QueryTree.divergence_reference_eq_charge line 108
  14. theorem OAI.CriticalPercolation.QueryTree.divergence_reference_bounds line 134
  15. lemma OAI.CriticalPercolation.QueryTree.valid_mono line 148
  16. lemma OAI.CriticalPercolation.QueryTree.run_dependsOn line 156
  17. lemma OAI.CriticalPercolation.QueryTree.reads_disjoint line 171
  18. lemma OAI.CriticalPercolation.QueryTree.reads_nodup line 184