OAI/Computability/QuantumFactoring/ParallelPreparation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.leftRegister line 16
  2. lemma OAI.ExactQuantumFactoring.append_leftRegister line 17
  3. lemma OAI.ExactQuantumFactoring.append_replace_left line 21
  4. def OAI.ExactQuantumFactoring.leftProgram line 36
  5. lemma OAI.ExactQuantumFactoring.leftProgram_basis line 38
  6. def OAI.ExactQuantumFactoring.appendEquiv line 46
  7. lemma OAI.ExactQuantumFactoring.appendEquiv_apply line 48
  8. def OAI.ExactQuantumFactoring.independentState line 51
  9. lemma OAI.ExactQuantumFactoring.encode_independent line 54
  10. def OAI.ExactQuantumFactoring.parallelProgram line 67
  11. lemma OAI.ExactQuantumFactoring.parallelProgram_length line 69
  12. lemma OAI.ExactQuantumFactoring.parallelProgram_basis line 73
  13. lemma OAI.ExactQuantumFactoring.independent_mass line 83
  14. lemma OAI.ExactQuantumFactoring.independent_mass_left line 89
  15. lemma OAI.ExactQuantumFactoring.independent_mass_right line 100
  16. lemma OAI.ExactQuantumFactoring.fair_normalized line 111
  17. lemma OAI.ExactQuantumFactoring.basis_preparation_normalized line 114