OAI/Computability/QuantumFactoring/CoherentSampling.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.packed_eq_iff line 14
2. lemma OAI.ExactQuantumFactoring.encoded_packed_coordinate line 24
3. def OAI.ExactQuantumFactoring.sampleProgram line 36

   Source documentation

   Retain the modular value register while interfering the exponent register; no copy of the exponent or hidden measurement is inserted.

   def sampleProgram {n m r : ℕ} (c : BooleanNetwork n m) (hr : c.net.count ≤ r)
       (ops : List (Instruction n)) : List (Instruction (n+m+r)) :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.Instruction

4. lemma OAI.ExactQuantumFactoring.sampleProgram_length line 40
5. lemma OAI.ExactQuantumFactoring.sampleProgram_amplitude line 47
6. lemma OAI.ExactQuantumFactoring.sampleProgram_encoded_amplitude line 69

   Source documentation

   Coherent sampling on an explicitly encoded logical subspace. Inactive quantum registers stay present; normalization need not be inferred by analogy with a stochastic oracle.

   lemma sampleProgram_encoded_amplitude {α : Type*} [Fintype α]
       {n m r : ℕ} (e : α → Basis n) (c : BooleanNetwork n m)
       (hr : c.net.count ≤ r) (ops : List (Instruction n)) (ψ : α → ℂ)
       (z : Basis n) (u : Basis m) :
       (programMatrix (sampleProgram c hr ops)).mulVec
         (encodeState (fun x => packed r (e x) (fun _ => false)) ψ) (packed r z u) =
         ∑ x, if c.eval (e x)=u then programMatrix ops z (e x) * ψ x else 0 := by
   …

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.sampleProgram, OAI.ExactQuantumFactoring.encodeState