OAI/Probability/CriticalPercolation/Exploration/Node.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalPercolation.QueryTree.bitWeight_pos line 22
  2. theorem OAI.CriticalPercolation.QueryTree.transcript_divergence_le line 26
  3. theorem OAI.CriticalPercolation.QueryTree.quadratic_bias_budget line 34
  4. theorem OAI.CriticalPercolation.QueryTree.transcript_divergence_upper line 42
  5. def OAI.CriticalPercolation.QueryTree.Node line 55
  6. instance OAI.CriticalPercolation.QueryTree.nodeFintype line 59
  7. def OAI.CriticalPercolation.QueryTree.bit line 64
  8. def OAI.CriticalPercolation.QueryTree.response line 70
  9. def OAI.CriticalPercolation.QueryTree.nodeMass line 79
  10. def OAI.CriticalPercolation.QueryTree.nodeTrueMass line 82
  11. lemma OAI.CriticalPercolation.QueryTree.nodeMass_root line 85
  12. lemma OAI.CriticalPercolation.QueryTree.nodeTrueMass_root line 90
  13. lemma OAI.CriticalPercolation.QueryTree.nodeMass_left line 94
  14. lemma OAI.CriticalPercolation.QueryTree.nodeTrueMass_left line 101
  15. lemma OAI.CriticalPercolation.QueryTree.nodeMass_right line 108
  16. lemma OAI.CriticalPercolation.QueryTree.nodeTrueMass_right line 115
  17. lemma OAI.CriticalPercolation.QueryTree.charge_eq_sum line 122