OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/PhysicalGroundComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Transfer manufactured-form estimates to the actual full-domain physical ground energy. Inverse dilation covers every weak-H1 state; upper bounds use positive-mass trial states and do not assume an attained continuum minimum.

  1. theorem OAI.ContinuumCoulomb.formGroundEnergy_dilated_lower line 22
  2. theorem OAI.ContinuumCoulomb.formGroundEnergy_dilated_trial line 46
  3. theorem OAI.ContinuumCoulomb.formGroundEnergy_dilated_upper line 65