OAI/Computability/QuantumFactoring/ControlledHadamard.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ExactQuantumFactoring.controlledHadamardAt line 20

   Source documentation

   One of the literal fixed alphabet gates; the extra control is the first wire and is never modified.

   abbrev controlledHadamardAt {q : ℕ} (c t : Fin q) (h : c≠t) : Instruction q :=
   …

   Mentions: OAI.ExactQuantumFactoring.Instruction

2. lemma OAI.ExactQuantumFactoring.controlledHadamardAt_matrix line 26
3. lemma OAI.ExactQuantumFactoring.controlledHadamardAt_basis line 71
4. lemma OAI.ExactQuantumFactoring.controlledHadamardAt_target line 80
5. lemma OAI.ExactQuantumFactoring.controlledHadamardAt_sector line 85

   Source documentation

   On a sector with a fixed control, controlled H is H or the identity on an arbitrary coherent state, including all old retained work.

   lemma controlledHadamardAt_sector {q : ℕ} (c t : Fin q) (h : c≠t) (b : Bool)
       (ψ : State q) (hs : Supported (fun x => x c=b) ψ) :
       (controlledHadamardAt c t h).matrix.mulVec ψ=
         if b then (hadamardAt t).matrix.mulVec ψ else ψ := by
   …

   Mentions: OAI.ExactQuantumFactoring.State, OAI.ExactQuantumFactoring.Supported, OAI.ExactQuantumFactoring.controlledHadamardAt, OAI.ExactQuantumFactoring.hadamardAt