OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/NuclearGridCoordinates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The serialized physical nuclei and the analytic finite grid share one explicit index. This supplies both the exact list identity and the numerical coordinate error in physical units.

  1. abbrev OAI.ContinuumCoulomb.NuclearGridCoordinates.Input line 15
  2. abbrev OAI.ContinuumCoulomb.NuclearGridCoordinates.Index line 16
  3. def OAI.ContinuumCoulomb.NuclearGridCoordinates.label line 18
  4. def OAI.ContinuumCoulomb.NuclearGridCoordinates.node line 21
  5. def OAI.ContinuumCoulomb.NuclearGridCoordinates.nucleus line 25
  6. theorem OAI.ContinuumCoulomb.NuclearGridCoordinates.nuclei_eq_ofFn line 29
  7. theorem OAI.ContinuumCoulomb.NuclearGridCoordinates.physical_coordinate_error line 41
  8. theorem OAI.ContinuumCoulomb.NuclearGridCoordinates.nucleus_position_injective line 55