OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/RoundingPolynomialBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A polynomial coordinate precision controls the full Coulomb ground energy, including the total charge of the large finite nuclear grid.

  1. theorem OAI.ContinuumCoulomb.inverse_power_product_le line 12
  2. theorem OAI.ContinuumCoulomb.rounding_polynomial_budget line 18