OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QubitMediatorForms.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The full physical energy equals the block energy on its genuine vacuum/complement decomposition.

  1. theorem OAI.ContinuumCoulomb.qmaMatrixOperator_real_symmetric line 15
  2. theorem OAI.ContinuumCoulomb.qmaMediatorRestriction_apply line 23
  3. def OAI.ContinuumCoulomb.qmaPhysicalOperator line 29
  4. def OAI.ContinuumCoulomb.qmaPerturbationOperator line 33
  5. def OAI.ContinuumCoulomb.qmaCouplingOperator line 37
  6. def OAI.ContinuumCoulomb.qmaComplementOperator line 41
  7. theorem OAI.ContinuumCoulomb.qmaPhysicalOperator_low line 45
  8. theorem OAI.ContinuumCoulomb.qmaPhysicalPenalty_high line 55
  9. theorem OAI.ContinuumCoulomb.qmaComplementOperator_form line 76
  10. theorem OAI.ContinuumCoulomb.qmaPhysicalOperator_high line 92
  11. theorem OAI.ContinuumCoulomb.qmaPhysicalOperator_energy line 104