OAI/Computability/QuantumFactoring/TreeTableEmission.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactQuantumFactoring.NetworkEmission.Emission.rowCode line 12
  2. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.compRow line 13
  3. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.compRowP line 14
  4. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emission.compRow_erase line 20
  5. def OAI.ExactQuantumFactoring.PhysicalTreeEmission.packedLog line 27
  6. lemma OAI.ExactQuantumFactoring.PhysicalTreeEmission.logCode_bound line 29
  7. lemma OAI.ExactQuantumFactoring.PhysicalTreeEmission.logCode_poly line 57
  8. lemma OAI.ExactQuantumFactoring.PhysicalTreeEmission.logNets line 69