OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCrossingBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Polynomial coefficient and operator bounds for the crossing construction.

  1. def OAI.ContinuumCoulomb.qmaCrossingLeft line 12
  2. def OAI.ContinuumCoulomb.qmaCrossingRight line 13
  3. def OAI.ContinuumCoulomb.qmaCrossingWeight line 14
  4. def OAI.ContinuumCoulomb.qmaCrossingOffset line 15
  5. theorem OAI.ContinuumCoulomb.qmaCrossingCorrection_exchange line 17
  6. theorem OAI.ContinuumCoulomb.qmaCrossingCorrection_lift_norm line 25
  7. theorem OAI.ContinuumCoulomb.qmaCrossingAmplitude_norm line 40