OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/GroundRoundingInterval.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Rounding a cloud using an already proved two-sided ground-energy interval. No minimizing eigenvector or independent kinetic bound is needed.

  1. theorem OAI.ContinuumCoulomb.formGroundEnergy_exists_trial_of_upper line 11
  2. theorem OAI.ContinuumCoulomb.formGroundEnergy_position_stability_of_upper line 18
  3. theorem OAI.ContinuumCoulomb.formGroundEnergy_rounding_interval line 34