OAI/MathematicalPhysics/ContinuumCoulomb/Programs/EnumeratedGridNuclei.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The centered label list and the analytic finite grid describe the same nuclear cloud, including after physical dilation.

  1. theorem OAI.ContinuumCoulomb.formGroundEnergy_eq_of_attraction line 15
  2. instance OAI.ContinuumCoulomb.centeredGridIndices_nonempty line 23
  3. theorem OAI.ContinuumCoulomb.CenteredGaussLabels.gauss_point_injective line 29
  4. def OAI.ContinuumCoulomb.CenteredGaussLabels.nuclei line 37
  5. theorem OAI.ContinuumCoulomb.CenteredGaussLabels.nuclei_attraction line 52
  6. theorem OAI.ContinuumCoulomb.CenteredGaussLabels.nuclei_ground line 63
  7. theorem OAI.ContinuumCoulomb.CenteredGaussLabels.dilated_nuclei_ground line 71
  8. theorem OAI.ContinuumCoulomb.CenteredGaussLabels.nuclei_totalCharge line 81