OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/EulerGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Componentwise box projection preserves Euclidean distance to every point in the box. Rounding the projected numerator adds at most 3 / D; there is no multiplicative loss in the Euler error recurrence.

  1. theorem OAI.ContinuumCoulomb.EulerRegisters.norm_le_of_abs_le line 14
  2. theorem OAI.ContinuumCoulomb.EulerRegisters.norm_of_coordinate_error line 22
  3. theorem OAI.ContinuumCoulomb.EulerRegisters.round_position_error line 42
  4. theorem OAI.ContinuumCoulomb.EulerRegisters.proposal_position line 53