OAI/Computability/QuantumFactoring/EncodedStates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.encodeState line 14

   Source documentation

   Embed a logical finite state in concrete basis words, including clean work.

   noncomputable def encodeState {α : Type*} [Fintype α] {q : ℕ}
       (e : α → Basis q) (ψ : α → ℂ) : State q := by
   …

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.State

2. lemma OAI.ExactQuantumFactoring.encodeState_apply line 19
3. lemma OAI.ExactQuantumFactoring.encodeState_at line 28
4. lemma OAI.ExactQuantumFactoring.encodeState_outside line 35
5. lemma OAI.ExactQuantumFactoring.encodeState_basis line 46
6. lemma OAI.ExactQuantumFactoring.encodeState_add line 51
7. lemma OAI.ExactQuantumFactoring.encodeState_smul line 57
8. lemma OAI.ExactQuantumFactoring.encodeState_sum line 63
9. lemma OAI.ExactQuantumFactoring.matrix_encodeState line 71

   Source documentation

   A basis-level implementation law extends to every coherent superposition.

   lemma matrix_encodeState {α β : Type*} [Fintype α] [Fintype β] {p q : ℕ}
       (e : α → Basis p) (f : β → Basis q) (U : Matrix (Basis q) (Basis p) ℂ)
       (V : Matrix β α ℂ)
       (h : ∀ a, U.mulVec (basisVector (e a)) = encodeState f (fun b => V b a))
       (ψ : α → ℂ) : U.mulVec (encodeState e ψ) = encodeState f (V.mulVec ψ) := by
   …

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

10. lemma OAI.ExactQuantumFactoring.matrix_encode_permutation line 89