OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QubitMediatorHilbert.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual Hilbert-space low and complementary coordinates for qubit mediators.

  1. def OAI.ContinuumCoulomb.qmaMediatorInclusion line 14
  2. def OAI.ContinuumCoulomb.qmaMediatorRestriction line 17
  3. def OAI.ContinuumCoulomb.qmaMediatorHighProjection line 20
  4. theorem OAI.ContinuumCoulomb.qmaMediator_restrict_include line 24
  5. theorem OAI.ContinuumCoulomb.qmaMediator_inclusion_adjoint line 31
  6. theorem OAI.ContinuumCoulomb.qmaMediator_highPart line 40
  7. theorem OAI.ContinuumCoulomb.qmaMediator_norm_decomposition line 51
  8. theorem OAI.ContinuumCoulomb.qmaMediatorHighProjection_norm line 57
  9. theorem OAI.ContinuumCoulomb.qmaMediatorRestriction_high line 62
  10. theorem OAI.ContinuumCoulomb.qmaMediatorRestriction_column line 69