OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkEffective.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Rational asymmetric fork gadget for reducing the degree of an old spin.

  1. def OAI.ContinuumCoulomb.qmaForkMember line 12
  2. def OAI.ContinuumCoulomb.qmaForkAmplitude line 13
  3. def OAI.ContinuumCoulomb.qmaForkCorrection line 15
  4. theorem OAI.ContinuumCoulomb.qmaFork_effective line 20