OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/Model.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Full spinful continuum Coulomb energy

Nuclear data and electronic states use the weak H¹ domain and translated Hardy bounds. Antisymmetry permutes spin and position together. No orbital projection or spin sector is imposed. The bottom takes values in EReal so its definition does not assume existence of a normalized state or a minimizing eigenvector.

  1. abbrev OAI.ContinuumCoulomb.Position line 22

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:355 (same declaration text).

  2. abbrev OAI.ContinuumCoulomb.Configuration line 23

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:356 (same declaration text).

  3. abbrev OAI.ContinuumCoulomb.SpinConfiguration line 24

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:357 (same declaration text).

  4. structure OAI.ContinuumCoulomb.NuclearData line 27

    Source documentation

    Finite clamped-nucleus data for binary-encoded positive integer charges.

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:359 (same declaration text).

    structure NuclearData where
…
  5. structure OAI.ContinuumCoulomb.UnitNuclearData line 38

    Source documentation

    Unit-charge inputs carry no independently chosen charge parameters.

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:369 (same declaration text).

    structure UnitNuclearData where
…
  6. def OAI.ContinuumCoulomb.UnitNuclearData.toNuclearData line 46

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:377 (same declaration text).

  7. theorem OAI.ContinuumCoulomb.realPosition_atLeastTwo line 58

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:389 (same declaration text).

  8. def OAI.ContinuumCoulomb.realPosition line 63

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:394 (same declaration text).

  9. theorem OAI.ContinuumCoulomb.realPosition_injective line 68

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:399 (same declaration text).

  10. def OAI.ContinuumCoulomb.NuclearData.toNuclei line 76

    Source documentation

    Integer positive charges satisfy the real-charge library interface.

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:406 (same declaration text).

    def NuclearData.toNuclei (d : NuclearData) : Coulomb.Nuclei d.nuclei where
…

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

  11. abbrev OAI.ContinuumCoulomb.FormState line 86

    Source documentation

    Every normalized state ranges over the full weak H¹ fermionic space.

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:415 (same declaration text).

    abbrev FormState (n : ℕ) := {state : Coulomb.H1Vector n // Coulomb.Antisymmetric state}

    Mentions: OAI.Coulomb.H1Vector, OAI.Coulomb.Antisymmetric

  12. abbrev OAI.ContinuumCoulomb.normSq line 88

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:417 (same declaration text).

  13. abbrev OAI.ContinuumCoulomb.kineticEnergy line 89

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:418 (same declaration text).

  14. def OAI.ContinuumCoulomb.coulombForm line 92

    Source documentation

    Electronic form with kinetic coefficient 1/2; nuclear repulsion omitted.

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:420 (same declaration text).

    def coulombForm (d : NuclearData) (state : FormState d.electrons) : ℝ :=
…

    Mentions: OAI.ContinuumCoulomb.NuclearData, OAI.ContinuumCoulomb.FormState

  15. def OAI.ContinuumCoulomb.unitCoulombForm line 95

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:423 (same declaration text).

  16. def OAI.ContinuumCoulomb.groundEnergy line 99

    Source documentation

    Variational bottom over every normalized spinful fermionic H¹ state.

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:426 (same declaration text).

    def groundEnergy (d : NuclearData) : EReal :=
…

    Mentions: OAI.ContinuumCoulomb.NuclearData

  17. def OAI.ContinuumCoulomb.unitGroundEnergy line 103

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:430 (same declaration text).

  18. theorem OAI.ContinuumCoulomb.unit_groundEnergy_eq line 108

    Source documentation

    The unit-to-binary inclusion preserves the entire variational energy.

    theorem unit_groundEnergy_eq (d : UnitNuclearData) :
    groundEnergy d.toNuclearData = unitGroundEnergy d := rfl

    Mentions: OAI.ContinuumCoulomb.UnitNuclearData, OAI.ContinuumCoulomb.groundEnergy, OAI.ContinuumCoulomb.unitGroundEnergy

  19. theorem OAI.ContinuumCoulomb.nuclear_integrable line 112

    Source documentation

    Nuclear singularities are integrable on the full declared form domain.

    theorem nuclear_integrable (d : NuclearData) (state : FormState d.electrons)
    (spin : SpinConfiguration d.electrons) :
    Integrable (fun x =>
      (∑ i, Coulomb.attraction d.toNuclei (Coulomb.position x i)) *
        ‖state.val.value spin x‖ ^ 2) :=
…

    Mentions: OAI.ContinuumCoulomb.NuclearData, OAI.ContinuumCoulomb.FormState, OAI.ContinuumCoulomb.SpinConfiguration, OAI.Coulomb.attraction, OAI.Coulomb.position

  20. theorem OAI.ContinuumCoulomb.pair_integrable line 120

    Source documentation

    Pair singularities are integrable too; no extra domain hypothesis is used.

    theorem pair_integrable {n : ℕ} (state : FormState n) (spin : SpinConfiguration n) :
    Integrable (fun x =>
      (∑ i : Fin n, ∑ j : Fin n,
        if i < j then Coulomb.coulombKernel (Coulomb.position x i - Coulomb.position x j)
          else 0) * ‖state.val.value spin x‖ ^ 2) :=
…

    Mentions: OAI.ContinuumCoulomb.FormState, OAI.ContinuumCoulomb.SpinConfiguration, OAI.Coulomb.coulombKernel, OAI.Coulomb.position

  21. theorem OAI.ContinuumCoulomb.normalized_form_lower_bound line 128

    Source documentation

    Explicit instance-dependent lower bound on every normalized state.

    theorem normalized_form_lower_bound (d : NuclearData) (state : FormState d.electrons)
    (hnorm : normSq state = 1) :
    -(2 * (d.electrons : ℝ) * Coulomb.totalCharge d.toNuclei ^ 2) ≤
      coulombForm d state := by
…

    Mentions: OAI.ContinuumCoulomb.NuclearData, OAI.ContinuumCoulomb.FormState, OAI.ContinuumCoulomb.normSq, OAI.Coulomb.totalCharge, OAI.ContinuumCoulomb.coulombForm

  22. theorem OAI.ContinuumCoulomb.groundEnergy_lower_bound line 138

    Source documentation

    The continuum infimum is never minus infinity. This does not assert attainment, binding, or a molecular excitation gap.

    theorem groundEnergy_lower_bound (d : NuclearData) :
    (-(2 * (d.electrons : ℝ) * Coulomb.totalCharge d.toNuclei ^ 2) : ℝ) ≤
      groundEnergy d := by
…

    Mentions: OAI.ContinuumCoulomb.NuclearData, OAI.Coulomb.totalCharge, OAI.ContinuumCoulomb.groundEnergy

  23. theorem OAI.ContinuumCoulomb.groundEnergy_le_trial line 146

    Source documentation

    Restricting admissible states supplies an upper bound on the full bottom.

    theorem groundEnergy_le_trial (d : NuclearData) (state : FormState d.electrons)
    (hnorm : normSq state = 1) :
    groundEnergy d ≤ (coulombForm d state : EReal) :=
…

    Mentions: OAI.ContinuumCoulomb.NuclearData, OAI.ContinuumCoulomb.FormState, OAI.ContinuumCoulomb.normSq, OAI.ContinuumCoulomb.groundEnergy, OAI.ContinuumCoulomb.coulombForm

  24. theorem OAI.ContinuumCoulomb.groundEnergy_ne_bot line 152

    Source documentation

    The lower form bound excludes minus infinity without any binding promise.

    theorem groundEnergy_ne_bot (d : NuclearData) : groundEnergy d ≠ ⊥ := by
…

    Mentions: OAI.ContinuumCoulomb.NuclearData, OAI.ContinuumCoulomb.groundEnergy

  25. theorem OAI.ContinuumCoulomb.groundEnergy_ne_top line 156

    Source documentation

    Any normalized trial state excludes plus infinity; attainment is unnecessary.

    theorem groundEnergy_ne_top (d : NuclearData) (state : FormState d.electrons)
    (hnorm : normSq state = 1) : groundEnergy d ≠ ⊤ := by
…

    Mentions: OAI.ContinuumCoulomb.NuclearData, OAI.ContinuumCoulomb.FormState, OAI.ContinuumCoulomb.normSq, OAI.ContinuumCoulomb.groundEnergy

  26. theorem OAI.ContinuumCoulomb.groundEnergy_coe_toReal line 162

    Source documentation

    Once a normalized trial state is provided, ordinary real threshold accounting applies to the same continuum infimum.

    theorem groundEnergy_coe_toReal (d : NuclearData) (state : FormState d.electrons)
    (hnorm : normSq state = 1) :
    ((groundEnergy d).toReal : EReal) = groundEnergy d :=
…

    Mentions: OAI.ContinuumCoulomb.NuclearData, OAI.ContinuumCoulomb.FormState, OAI.ContinuumCoulomb.normSq, OAI.ContinuumCoulomb.groundEnergy