OAI/Computability/QuantumFactoring/HadamardAction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.hadamardAt_symmetric line 14
2. lemma OAI.ExactQuantumFactoring.hadamardAt_apply_direct_sum line 21
3. def OAI.ExactQuantumFactoring.localHadamard line 36
4. lemma OAI.ExactQuantumFactoring.localHadamard_apply line 41
5. lemma OAI.ExactQuantumFactoring.localHadamard_basis line 54
6. lemma OAI.ExactQuantumFactoring.encoded_hadamard line 72

   Source documentation

   Logical H on data is physically H on the corresponding encoded wire, provided the embedding preserves that bit and its two updates.

   lemma encoded_hadamard {A : Type*} [Fintype A] [DecidableEq A] {b q : ℕ}
       (e : Basis b × A → Basis q) (j : Fin b) (t : Fin q)
       (hbit : ∀ u, e u t = u.1 j)
       (hupdate : ∀ u c, Function.update (e u) t c = e (Function.update u.1 j c,u.2))
       (ψ : Basis b × A → ℂ) :
       (hadamardAt t).matrix.mulVec (encodeState e ψ) =
         encodeState e ((localHadamard (A:=A) j).mulVec ψ) := by
   …

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.hadamardAt, OAI.ExactQuantumFactoring.encodeState, OAI.ExactQuantumFactoring.localHadamard