OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkIteration.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Iterating the actual weighted graph keeps a proved full-space energy error.

  1. structure OAI.ContinuumCoulomb.QMAWeightedForkNetwork line 13
  2. def OAI.ContinuumCoulomb.QMAWeightedForkNetwork.energy line 22
  3. def OAI.ContinuumCoulomb.QMAWeightedForkNetwork.scale line 25
  4. def OAI.ContinuumCoulomb.QMAWeightedForkNetwork.next line 32
  5. theorem OAI.ContinuumCoulomb.QMAWeightedForkNetwork.next_energy_error line 38
  6. def OAI.ContinuumCoulomb.QMAWeightedForkNetwork.iterate line 42
  7. theorem OAI.ContinuumCoulomb.QMAWeightedForkNetwork.iterate_graph line 46
  8. theorem OAI.ContinuumCoulomb.QMAWeightedForkNetwork.iterate_energy_error line 54