OAI/InformationTheory/QuantumCircuit/Model.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.QAC.Bit line 10

   Also declared: ComparatorChallenges/QACParity.lean:10 (same declaration text), ComparatorChallenges/RegularParity.lean:10 (same declaration text).

2. abbrev OAI.QAC.Word line 11

   Also declared: ComparatorChallenges/QACParity.lean:11 (same declaration text), ComparatorChallenges/RegularParity.lean:11 (same declaration text).

3. abbrev OAI.QAC.Operator line 12

   Also declared: ComparatorChallenges/QACParity.lean:12 (same declaration text), ComparatorChallenges/RegularParity.lean:12 (same declaration text).

4. abbrev OAI.QAC.QubitOperator line 13

   Also declared: ComparatorChallenges/QACParity.lean:13 (same declaration text), ComparatorChallenges/RegularParity.lean:13 (same declaration text).

5. def OAI.QAC.tensorMatrix line 16

   Source documentation

   Tensor product in the computational basis.

   Also declared: ComparatorChallenges/QACParity.lean:16 (same declaration text), ComparatorChallenges/RegularParity.lean:16 (same declaration text).

   def tensorMatrix {N : ℕ} (a : Fin N → QubitOperator) : Operator N :=
   …

   Mentions: OAI.QAC.QubitOperator, OAI.QAC.Operator

6. inductive OAI.QAC.Gate line 20

   Source documentation

   A one-qubit unitary or an unbounded-arity Toffoli gate.

   Also declared: ComparatorChallenges/QACParity.lean:20 (same declaration text), ComparatorChallenges/RegularParity.lean:20 (same declaration text).

   inductive Gate (N : ℕ) where
   …

7. def OAI.QAC.Gate.support line 26

   Also declared: ComparatorChallenges/QACParity.lean:26 (same declaration text), ComparatorChallenges/RegularParity.lean:26 (same declaration text).

8. def OAI.QAC.Gate.toffoliWord line 31

   Source documentation

   A Toffoli flips its target iff all controls are one.

   Also declared: ComparatorChallenges/QACParity.lean:31 (same declaration text), ComparatorChallenges/RegularParity.lean:31 (same declaration text).

   def toffoliWord {N : ℕ} (c : Finset (Fin N)) (t : Fin N) (x : Word N) : Word N :=
   …

   Mentions: OAI.QAC.Word

9. def OAI.QAC.Gate.matrix line 34

   Also declared: ComparatorChallenges/QACParity.lean:34 (same declaration text), ComparatorChallenges/RegularParity.lean:34 (same declaration text).

10. structure OAI.QAC.PhysicalLayer line 40

    Also declared: ComparatorChallenges/QACParity.lean:40 (same declaration text), ComparatorChallenges/RegularParity.lean:40 (same declaration text).

11. def OAI.QAC.physicalLayerMatrix line 44

    Also declared: ComparatorChallenges/QACParity.lean:44 (same declaration text), ComparatorChallenges/RegularParity.lean:44 (same declaration text).

12. def OAI.QAC.physicalCircuitMatrix line 48

    Source documentation

    Chronological order: the rightmost matrix acts first.

    Also declared: ComparatorChallenges/QACParity.lean:48 (same declaration text), ComparatorChallenges/RegularParity.lean:48 (same declaration text).

    def physicalCircuitMatrix {N : ℕ} (layers : List (PhysicalLayer N)) : Operator N :=
    …

    Mentions: OAI.QAC.PhysicalLayer, OAI.QAC.Operator

13. def OAI.QAC.inputWord line 52

    Source documentation

    The computational-basis input with the remaining qubits initialized to zero.

    Also declared: ComparatorChallenges/QACParity.lean:52 (same declaration text), ComparatorChallenges/RegularParity.lean:52 (same declaration text).

    def inputWord {n N : ℕ} (x : Word n) : Word N :=
    …

    Mentions: OAI.QAC.Word

14. def OAI.QAC.parity line 55

    Also declared: ComparatorChallenges/QACParity.lean:55 (same declaration text), ComparatorChallenges/RegularParity.lean:55 (same declaration text).

15. def OAI.QAC.successProbability line 58

    Source documentation

    Born probability, summing all final garbage with no cleanliness assumption.

    Also declared: ComparatorChallenges/QACParity.lean:58 (same declaration text), ComparatorChallenges/RegularParity.lean:58 (same declaration text).

    def successProbability {n N : ℕ} (W : Operator N) (out : Fin N) (x : Word n) : ℝ :=
    …

    Mentions: OAI.QAC.Operator, OAI.QAC.Word

16. def OAI.QAC.ParityStatement line 62

    Source documentation

    The literal measured-output, polynomial-total-qubit parity lower bound.

    Also declared: ComparatorChallenges/QACParity.lean:62 (same declaration text).

    def ParityStatement : Prop :=
    …