OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/IsolatedSpectrum.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Stability of the unrestricted isolated-well variational bottom

All infima range over normalized spinful weak-H¹ states. The estimates use form comparison and a concrete normalized bump trial; no eigenfunction, attainment, or spectral oracle is supplied as an assumption.

  1. def OAI.ContinuumCoulomb.oneElectronEnergy line 17
  2. def OAI.ContinuumCoulomb.hydrogenEnergy line 21
  3. def OAI.ContinuumCoulomb.isolatedWellEnergy line 23
  4. theorem OAI.ContinuumCoulomb.oneElectronEnergy_le_trial line 26
  5. theorem OAI.ContinuumCoulomb.oneElectronEnergy_lower_of_forall line 31
  6. theorem OAI.ContinuumCoulomb.oneElectronEnergy_finite line 38
  7. theorem OAI.ContinuumCoulomb.hydrogenEnergy_finite line 46
  8. theorem OAI.ContinuumCoulomb.isolatedWellEnergy_finite line 53
  9. theorem OAI.ContinuumCoulomb.oneElectronEnergy_bounded_perturbation line 66
  10. theorem OAI.ContinuumCoulomb.isolatedWellEnergy_relative line 102
  11. theorem OAI.ContinuumCoulomb.isolatedWellEnergy_other_displacements line 170

    Source documentation

    Keeping the own secondary nucleus fixed yields the small other-site energy Lipschitz bound on the actual infimum, without a ground-state premise.

    theorem isolatedWellEnergy_other_displacements {m : ℕ} {D q q' delta : ℝ}
    (hD : 128 ≤ D) (hq : 0 ≤ q) (hq1 : q ≤ 1) (hq' : 0 ≤ q') (hq'1 : q' ≤ 1)
    (hdelta : 0 ≤ delta) (center a b : Fin m → Position)
    (ha : ∀ j, ‖a j‖ ≤ 4) (hb : ∀ j, ‖b j‖ ≤ 4)
    (hmove : ∀ j, ‖a j - b j‖ ≤ delta) (site : Fin m) (hown : a site = b site) :
    |(isolatedWellEnergy D q q' center b site).toReal -
      (isolatedWellEnergy D q q' center a site).toReal| ≤ 2048 * q' * m / D ^ 2 * delta := by
…

    Mentions: OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.isolatedWellEnergy