OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumGateScalarReduction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Exact scalar reduction of a one-site gate tensor to its active entry and spectator equality test. This avoids an ambient spin-basis sum in the literal history-matrix evaluator.

  1. theorem OAI.ContinuumCoulomb.QuantumGateScalarReduction.mul_one line 14
  2. theorem OAI.ContinuumCoulomb.QuantumGateScalarReduction.one_mul line 18
  3. theorem OAI.ContinuumCoulomb.QuantumGateScalarReduction.mul_zero line 22
  4. theorem OAI.ContinuumCoulomb.QuantumGateScalarReduction.zero_mul line 26
  5. theorem OAI.ContinuumCoulomb.QuantumGateScalarReduction.listProduct_single line 30
  6. theorem OAI.ContinuumCoulomb.QuantumGateScalarReduction.listProduct_zero line 43
  7. theorem OAI.ContinuumCoulomb.QuantumGateScalarReduction.finiteProduct_single line 52
  8. theorem OAI.ContinuumCoulomb.QuantumGateScalarReduction.finiteProduct_zero line 61
  9. def OAI.ContinuumCoulomb.QuantumGateScalarReduction.sparseEntry line 69
  10. theorem OAI.ContinuumCoulomb.QuantumGateScalarReduction.finiteProduct_sparse line 73
  11. theorem OAI.ContinuumCoulomb.QuantumGateScalarReduction.hadamard_entry line 92
  12. theorem OAI.ContinuumCoulomb.QuantumGateScalarReduction.phaseT_entry line 96