OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/NuclearPacking.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The bounded overlap needed by the near-node form estimate follows from separation of the actual nuclear positions, by disjoint small balls.

  1. theorem OAI.ContinuumCoulomb.separated_position_card_bound line 14
  2. theorem OAI.ContinuumCoulomb.separated_ball_overlap line 57