OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumMask.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Coordinate projections for the initial and output penalties.

  1. def OAI.ContinuumCoulomb.qmaMask line 11
  2. theorem OAI.ContinuumCoulomb.qmaMask_apply line 19
  3. theorem OAI.ContinuumCoulomb.qmaMask_norm_le line 23
  4. theorem OAI.ContinuumCoulomb.qmaMask_complement_square line 32
  5. theorem OAI.ContinuumCoulomb.qmaMask_sub_norm_le line 41
  6. theorem OAI.ContinuumCoulomb.qmaMask_square_difference line 47
  7. theorem OAI.ContinuumCoulomb.qmaMask_sub_self line 55