OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListInitialAccuracy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual initial odd subdivision changes the full-space ground energy by at most 1/N. Together with the literal fork iteration this is (k+1)/N.

  1. theorem OAI.ContinuumCoulomb.QuantumForkList.initial_accuracy line 13
  2. theorem OAI.ContinuumCoulomb.QuantumForkList.initial_iterated_accuracy line 55