OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSweepCursor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact sweep cursor around the inserted logical gate.

  1. def OAI.ContinuumCoulomb.qmaStageCursor line 11

    Source documentation

    Three transfer gates per column, with one gate inserted at the previous column.

    def qmaStageCursor (cut t : ℕ) : ℕ :=
…
  2. theorem OAI.ContinuumCoulomb.qmaStageCursor_lt line 14
  3. theorem OAI.ContinuumCoulomb.qmaStageCursor_step line 19
  4. theorem OAI.ContinuumCoulomb.qmaStageCursor_zero line 25
  5. theorem OAI.ContinuumCoulomb.qmaStageCursor_last line 28
  6. def OAI.ContinuumCoulomb.qmaStageCursorFin line 33
  7. theorem OAI.ContinuumCoulomb.qmaSweepOrder_near line 38