Rationalization.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Rational nuclear output with a ground-energy error budget

Coordinate rounding controls the full Coulomb variational infimum while retaining the nuclear charges, nuclei count and electron number.

def OAI.ContinuumCoulomb.rationalizeNuclei line 17

Source documentation

Rational nuclear data produced from real centers and integral charges.

def rationalizeNuclei {m : ℕ} (S : Coulomb.Nuclei m) (n : ℕ) (hn : 0 < n)
    (charge : Fin m → ℕ) (hcharge : ∀ a, (charge a : ℝ) = S.charge a)
    (denominator : ℕ) (hdenom : 0 < denominator)
    (hsep : ∀ i j, i ≠ j → 6 / (denominator : ℝ) < ‖S.position i - S.position j‖) :
    NuclearData where
…

Mentions: OAI.Coulomb.Nuclei, OAI.ContinuumCoulomb.NuclearData

theorem OAI.ContinuumCoulomb.rationalizeNuclei_charge line 36
theorem OAI.ContinuumCoulomb.rationalizeNuclei_position_error line 45

theorem OAI.ContinuumCoulomb.rationalizeNuclei_groundEnergy_error line 58

Source documentation

The rounded output has distinct rational positions and the same integer charges, and its true fermionic bottom changes by at most the stated budget.

theorem rationalizeNuclei_groundEnergy_error {m n denominator : ℕ} (S : Coulomb.Nuclei m)
    (hn : 0 < n) (charge : Fin m → ℕ) (hcharge : ∀ a, (charge a : ℝ) = S.charge a)
    (hdenom : 0 < denominator)
    (hsep : ∀ i j, i ≠ j → 6 / (denominator : ℝ) < ‖S.position i - S.position j‖)
    (trial : FormState n) (htrial : normSq trial = 1)
    (hsmall : 96 * Coulomb.totalCharge S / (denominator : ℝ) ≤ 1) :
    |(groundEnergy (rationalizeNuclei S n hn charge hcharge denominator hdenom hsep)).toReal -
      (formGroundEnergy S n).toReal| ≤
      96 * Coulomb.totalCharge S / (denominator : ℝ) *
        (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.groundEnergy, OAI.ContinuumCoulomb.rationalizeNuclei, OAI.ContinuumCoulomb.formGroundEnergy, OAI.Coulomb.form

def OAI.ContinuumCoulomb.rationalizeUnitNuclei line 84

Source documentation

In the unit-charge case the output uses the unit-charge input structure.

def rationalizeUnitNuclei {m : ℕ} (S : Coulomb.Nuclei m) (n : ℕ) (hn : 0 < n)
    (denominator : ℕ) (hdenom : 0 < denominator)
    (hsep : ∀ i j, i ≠ j → 6 / (denominator : ℝ) < ‖S.position i - S.position j‖) :
    UnitNuclearData where
…

Mentions: OAI.Coulomb.Nuclei, OAI.ContinuumCoulomb.UnitNuclearData

theorem OAI.ContinuumCoulomb.rationalizeUnitNuclei_groundEnergy_error line 95