OAI/Computability/QuantumFactoring/TensorPreparation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactQuantumFactoring.tensorWidth line 19
  2. lemma OAI.ExactQuantumFactoring.tensorWidth_eq line 23
  3. def OAI.ExactQuantumFactoring.tensorLayout line 28
  4. lemma OAI.ExactQuantumFactoring.tensorLayout_succ line 33
  5. def OAI.ExactQuantumFactoring.tensorProgram line 36
  6. lemma OAI.ExactQuantumFactoring.tensorProgram_length line 40
  7. lemma OAI.ExactQuantumFactoring.tensorProgram_entry line 46
  8. lemma OAI.ExactQuantumFactoring.tensorProgram_state line 60

    Source documentation

    A literal repeated finite-gate program, not just a tensor-state idealization.

    lemma tensorProgram_state {q : ℕ} (ops : List (Instruction q)) (K : ℕ) (x : Basis q) :
    (programMatrix (tensorProgram ops K)).mulVec (basisVector (tensorLayout q K (fun _ => x)))=
      encodeState (tensorLayout q K) (tensorState ((programMatrix ops).mulVec (basisVector x)) K) := by
…

    Mentions: OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.tensorProgram, OAI.ExactQuantumFactoring.basisVector, OAI.ExactQuantumFactoring.tensorLayout, OAI.ExactQuantumFactoring.encodeState

  9. lemma OAI.ExactQuantumFactoring.tensorProgram_event line 68