NuclearRounding.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Stability under rounding a nuclear position

Translated Hardy estimates uniformly control rational rounding on arbitrary form-domain states. The constant eight permits a pointwise kernel inequality also at the poles, using Lean's convention 0⁻¹ = 0, and suffices for the polynomial precision budget.

theorem OAI.ContinuumCoulomb.coulomb_kernel_shift_bound line 21

Source documentation

Pointwise control valid even where an inverse distance is totalized to zero.

theorem coulomb_kernel_shift_bound (x a b : Coulomb.Space) :
    |Coulomb.coulombKernel (x - a) - Coulomb.coulombKernel (x - b)| ≤
      ‖a - b‖ * (Coulomb.coulombKernel (x - a) ^ 2 +
        Coulomb.coulombKernel (x - b) ^ 2) := by
…

Mentions: OAI.Coulomb.Space, OAI.Coulomb.coulombKernel

theorem OAI.ContinuumCoulomb.nuclear_hardy_square line 65

Source documentation

Translated Hardy as a bound for the square of the physical Coulomb kernel.

theorem nuclear_hardy_square {n : ℕ} (state : Coulomb.H1Vector n)
    (spin : Coulomb.Spins n) (i : Fin n) (a : Coulomb.Space) :
    Integrable (fun x => Coulomb.coulombKernel (Coulomb.position x i - a) ^ 2 *
      ‖state.value spin x‖ ^ 2) ∧
    (∫ x, Coulomb.coulombKernel (Coulomb.position x i - a) ^ 2 *
      ‖state.value spin x‖ ^ 2) ≤
      4 * ∑ k : Fin 3, ∫ x, ‖state.gradient spin (i, k) x‖ ^ 2 := by
…

Mentions: OAI.Coulomb.H1Vector, OAI.Coulomb.Spins, OAI.Coulomb.Space, OAI.Coulomb.coulombKernel, OAI.Coulomb.position

theorem OAI.ContinuumCoulomb.nuclear_position_rounding_bound line 78

Source documentation

An actual form-domain estimate on every spin component, uniform in both nuclear positions and without a separation condition.

theorem nuclear_position_rounding_bound {n : ℕ} (state : Coulomb.H1Vector n)
    (spin : Coulomb.Spins n) (i : Fin n) (a b : Coulomb.Space) :
    |∫ x, (Coulomb.coulombKernel (Coulomb.position x i - a) -
      Coulomb.coulombKernel (Coulomb.position x i - b)) * ‖state.value spin x‖ ^ 2| ≤
      8 * ‖a - b‖ * ∑ k : Fin 3, ∫ x, ‖state.gradient spin (i, k) x‖ ^ 2 := by
…

Mentions: OAI.Coulomb.H1Vector, OAI.Coulomb.Spins, OAI.Coulomb.Space, OAI.Coulomb.coulombKernel, OAI.Coulomb.position

theorem OAI.ContinuumCoulomb.all_nuclei_rounding_bound line 130

Source documentation

Rounding all equal-charge nuclei is controlled on every many-electron spinful H¹ vector. charge = 1 / λ gives the dilated unit-nucleus estimate. The total mass factor is explicit, including the large slab volume.

theorem all_nuclei_rounding_bound {n m : ℕ} (state : Coulomb.H1Vector n)
    (oldPosition newPosition : Fin m → Coulomb.Space) {delta charge : ℝ}
    (hcharge : 0 ≤ charge)
    (hmove : ∀ a, ‖oldPosition a - newPosition a‖ ≤ delta) :
    |charge * ∑ spin : Coulomb.Spins n, ∑ i : Fin n, ∑ a : Fin m,
      ∫ x, (Coulomb.coulombKernel (Coulomb.position x i - oldPosition a) -
        Coulomb.coulombKernel (Coulomb.position x i - newPosition a)) *
          ‖state.value spin x‖ ^ 2| ≤
      16 * charge * (m : ℝ) * delta * Coulomb.kinetic state := by
…

Mentions: OAI.Coulomb.H1Vector, OAI.Coulomb.Space, OAI.Coulomb.Spins, OAI.Coulomb.coulombKernel, OAI.Coulomb.position, OAI.Coulomb.kinetic