OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/SeparatedNuclearNear.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Separation of the actual point nuclei supplies the bounded-overlap hypothesis in the weak-H1 near-node estimate.

  1. theorem OAI.ContinuumCoulomb.separated_electron_ball_overlap line 14
  2. theorem OAI.ContinuumCoulomb.separated_nuclear_near_bound line 25