FormStability.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Stability of the full variational bottom under nuclear rounding

The Hardy estimate is combined with coercivity of the actual Coulomb form. Consequently rational rounding is controlled on the unrestricted fermionic ground-energy infimum, without assuming a minimizing eigenvector or an independent kinetic-energy bound.

theorem OAI.ContinuumCoulomb.coulomb_form_coercive line 22
Source documentation
Keeping half of the kinetic form gives a uniform coercive lower bound.
```
theorem coulomb_form_coercive {m n : ℕ} (S : Coulomb.Nuclei m)
    (state : Coulomb.H1Vector n) :
    Coulomb.kinetic state / 2 -
        4 * (n : ℝ) * Coulomb.totalCharge S ^ 2 * Coulomb.mass state ≤
      Coulomb.form S state := by
…
```
Mentions: OAI.Coulomb.Nuclei, OAI.Coulomb.H1Vector, OAI.Coulomb.kinetic, OAI.Coulomb.totalCharge, OAI.Coulomb.mass, OAI.Coulomb.form

theorem OAI.ContinuumCoulomb.coulomb_form_position_error line 47

Source documentation

The rounding estimate includes arbitrary positive nuclear charges, with their total mass rather than their maximum charge in the error budget.

theorem coulomb_form_position_error {m n : ℕ} (S T : Coulomb.Nuclei m)
    (state : Coulomb.H1Vector n) {delta : ℝ}
    (hcharge : S.charge = T.charge)
    (hmove : ∀ a, ‖S.position a - T.position a‖ ≤ delta) :
    |Coulomb.form S state - Coulomb.form T state| ≤
      16 * delta * Coulomb.totalCharge S * Coulomb.kinetic state := by
…

Mentions: OAI.Coulomb.Nuclei, OAI.Coulomb.H1Vector, OAI.Coulomb.form, OAI.Coulomb.totalCharge, OAI.Coulomb.kinetic

def OAI.ContinuumCoulomb.formGroundEnergy line 110
Source documentation
The same full fermionic bottom for real positions, prior to rationalization.
```
def formGroundEnergy {m : ℕ} (S : Coulomb.Nuclei m) (n : ℕ) : EReal :=
…
```
Mentions: OAI.Coulomb.Nuclei
theorem OAI.ContinuumCoulomb.groundEnergy_eq_formGroundEnergy line 114
theorem OAI.ContinuumCoulomb.formGroundEnergy_le_trial line 117
theorem OAI.ContinuumCoulomb.formGroundEnergy_lower_of_forall line 122
theorem OAI.ContinuumCoulomb.formGroundEnergy_finite line 129

theorem OAI.ContinuumCoulomb.formGroundEnergy_position_stability line 145

Source documentation

A quantitative change of the full bottom under nuclear movement. The single normalized trial proves both bottoms finite; it need not minimize. The factor in parentheses is automatically nonnegative by coercivity.

theorem formGroundEnergy_position_stability {m n : ℕ} (S T : Coulomb.Nuclei m)
    (trial : FormState n) (htrial : normSq trial = 1) {delta : ℝ}
    (hdelta : 0 ≤ delta) (hcharge : S.charge = T.charge)
    (hmove : ∀ a, ‖S.position a - T.position a‖ ≤ delta)
    (hsmall : 32 * delta * Coulomb.totalCharge S ≤ 1) :
    |(formGroundEnergy T n).toReal - (formGroundEnergy S n).toReal| ≤
      32 * delta * Coulomb.totalCharge S *
        ((formGroundEnergy S n).toReal + 4 * (n : ℝ) * Coulomb.totalCharge S ^ 2) := by
…

Mentions: OAI.Coulomb.Nuclei, OAI.ContinuumCoulomb.FormState, OAI.ContinuumCoulomb.normSq, OAI.Coulomb.totalCharge, OAI.ContinuumCoulomb.formGroundEnergy

theorem OAI.ContinuumCoulomb.formGroundEnergy_position_stability_trial line 217

Source documentation

An explicit trial energy supplies a computable rounding budget, without requiring the exact real ground energy as input.

theorem formGroundEnergy_position_stability_trial {m n : ℕ} (S T : Coulomb.Nuclei m)
    (trial : FormState n) (htrial : normSq trial = 1) {delta : ℝ}
    (hdelta : 0 ≤ delta) (hcharge : S.charge = T.charge)
    (hmove : ∀ a, ‖S.position a - T.position a‖ ≤ delta)
    (hsmall : 32 * delta * Coulomb.totalCharge S ≤ 1) :
    |(formGroundEnergy T n).toReal - (formGroundEnergy S n).toReal| ≤
      32 * delta * Coulomb.totalCharge S *
        (Coulomb.form S trial.val + 4 * (n : ℝ) * Coulomb.totalCharge S ^ 2) := by
…

Mentions: OAI.Coulomb.Nuclei, OAI.ContinuumCoulomb.FormState, OAI.ContinuumCoulomb.normSq, OAI.Coulomb.totalCharge, OAI.ContinuumCoulomb.formGroundEnergy, OAI.Coulomb.form