OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/GridNodePrecision.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Explicit polynomial precision for the emitted nodes: separation and the full-ground rounding budget account for all nuclei in the centered box.

  1. theorem OAI.ContinuumCoulomb.exists_grid_node_separation_offset line 13
  2. theorem OAI.ContinuumCoulomb.grid_node_rounding_budget line 32