OAI/Computability/QuantumFactoring/PackedEncoding.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.BooleanNetwork.packed_injective line 13
2. lemma OAI.ExactQuantumFactoring.BooleanNetwork.packed_update_input line 24
3. lemma OAI.ExactQuantumFactoring.BooleanNetwork.packed_update_target line 39
4. lemma OAI.ExactQuantumFactoring.BooleanNetwork.append_update_left line 57
5. lemma OAI.ExactQuantumFactoring.BooleanNetwork.encoded_adjoint_test line 70

   Source documentation

   Taking an adjoint and reading a basis outcome implements exactly the correlation with the prepared state, without an idealized projection gate.

   lemma encoded_adjoint_test {α : Type*} [Fintype α] {q : ℕ}
       (e : α → Basis q) (he : Function.Injective e)
       (U : Matrix (Basis q) (Basis q) ℂ) (v : Basis q) (χ ψ : α → ℂ)
       (h : U.mulVec (basisVector v) = encodeState e χ) :
       U.conjTranspose.mulVec (encodeState e ψ) v = ∑ a, star (χ a)*ψ a := by
   …

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.basisVector, OAI.ExactQuantumFactoring.encodeState