OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CoulombRawEvaluation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The fixed polynomial schedule approximates the actual unnormalized Coulomb box integral uniformly in every rational separation.

  1. theorem OAI.ContinuumCoulomb.CoulombEvaluation.position_shift line 12
  2. theorem OAI.ContinuumCoulomb.CoulombEvaluation.denominator_inverse line 22
  3. theorem OAI.ContinuumCoulomb.CoulombEvaluation.rational_box_quadrature_error line 26
  4. theorem OAI.ContinuumCoulomb.CoulombEvaluation.natural_quadrature_budget line 51
  5. theorem OAI.ContinuumCoulomb.CoulombEvaluation.raw_approximation_error line 86