OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumDistributedInput.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Input checks may occur at separate history times before their qubits are changed.

  1. def OAI.ContinuumCoulomb.qmaInputCheck line 11
  2. theorem OAI.ContinuumCoulomb.qmaMask_norm_sq line 14
  3. theorem OAI.ContinuumCoulomb.qmaInputPenalty_le_checks line 22
  4. def OAI.ContinuumCoulomb.qmaDistributedInput line 42
  5. theorem OAI.ContinuumCoulomb.qmaInputPenalty_le_distributed line 46
  6. def OAI.ContinuumCoulomb.qmaDistributedHistoryEnergy line 78
  7. theorem OAI.ContinuumCoulomb.qmaDistributedHistoryEnergy_sound line 83