OAI/Computability/QuantumFactoring/NetworkEmissionBounds.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.NetworkEmission.Node.Bound line 13
  2. lemma OAI.ExactQuantumFactoring.NetworkEmission.Node.Bound.mono line 18
  3. lemma OAI.ExactQuantumFactoring.NetworkEmission.Node.Bound.map line 20
  4. def OAI.ExactQuantumFactoring.NetworkEmission.Data.width line 27
  5. def OAI.ExactQuantumFactoring.NetworkEmission.Data.mass line 28
  6. def OAI.ExactQuantumFactoring.NetworkEmission.Data.Valid line 29
  7. lemma OAI.ExactQuantumFactoring.NetworkEmission.eraseNode_bound line 30
  8. lemma OAI.ExactQuantumFactoring.NetworkEmission.eraseNet_nodes_bound line 32
  9. lemma OAI.ExactQuantumFactoring.NetworkEmission.erase_valid line 41
  10. lemma OAI.ExactQuantumFactoring.NetworkEmission.valid_select line 51
  11. lemma OAI.ExactQuantumFactoring.NetworkEmission.valid_node line 56
  12. lemma OAI.ExactQuantumFactoring.NetworkEmission.pairIndex_bound line 65
  13. lemma OAI.ExactQuantumFactoring.NetworkEmission.pair_valid line 67
  14. lemma OAI.ExactQuantumFactoring.NetworkEmission.headD_drop_bound line 86
  15. lemma OAI.ExactQuantumFactoring.NetworkEmission.attachRawIndex_bound line 93
  16. lemma OAI.ExactQuantumFactoring.NetworkEmission.comp_valid line 99
  17. lemma OAI.ExactQuantumFactoring.NetworkEmission.pair_mass line 117
  18. lemma OAI.ExactQuantumFactoring.NetworkEmission.comp_mass line 119
  19. lemma OAI.ExactQuantumFactoring.NetworkEmission.nat_bits_length_bound line 121
  20. lemma OAI.ExactQuantumFactoring.NetworkEmission.listCode_length_bound line 124
  21. lemma OAI.ExactQuantumFactoring.NetworkEmission.nodeCode_bound line 133
  22. lemma OAI.ExactQuantumFactoring.NetworkEmission.dataCode_bound line 154