OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumFourProjector.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The rational projection is exactly the normalized singlet range.

  1. theorem OAI.ContinuumCoulomb.qmaFourNormalization_square line 12
  2. theorem OAI.ContinuumCoulomb.qmaFourProjectionRational_factor line 26
  3. theorem OAI.ContinuumCoulomb.qmaFourEncoding_projector line 34
  4. theorem OAI.ContinuumCoulomb.qmaFour_complement_gap line 44