OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRowInsertion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A logical gate is inserted immediately after its last operand arrives.

  1. theorem OAI.ContinuumCoulomb.qmaMapGate_sites line 12
  2. def OAI.ContinuumCoulomb.qmaGateCut line 18
  3. theorem OAI.ContinuumCoulomb.qmaGateCut_le line 21
  4. theorem OAI.ContinuumCoulomb.qmaGateCut_site line 28
  5. def OAI.ContinuumCoulomb.qmaRowStage line 33
  6. theorem OAI.ContinuumCoulomb.qmaRowStage_tail_avoids line 41
  7. theorem OAI.ContinuumCoulomb.qmaRowStage_matrix line 65