Geometry and attraction of electron shells

A finite nonempty nuclear configuration has a nearest index.

Identify the nearest distance without a Voronoi tie-breaking choice.

theorem LiebThirring.exists_nearest_nucleus {M : ℕ} (hM : 1 ≤ M) (R : Fin M → Position) (a : Position) : ∃ (k : Fin M), ∀ (l : Fin M), ‖a - R k‖ ≤ ‖a - R l‖

A finite nonempty nuclear configuration has a nearest index.

theorem LiebThirring.nearestNucleusDistance_eq_of_min {M : ℕ} (R : Fin M → Position) (a : Position) (k : Fin M) (hk : ∀ (l : Fin M), ‖a - R k‖ ≤ ‖a - R l‖) : nearestNucleusDistance R a = ENNReal.ofReal ‖a - R k‖

Identify the nearest distance without a Voronoi tie-breaking choice.

theorem LiebThirring.screenedPotential_eq_of_min {M : ℕ} (Z : NNReal) (R : Fin M → Position) (a : Position) (k : Fin M) (hk : ∀ (l : Fin M), ‖a - R k‖ ≤ ‖a - R l‖) : screenedPotential Z R a = ∑ l ∈ Finset.univ.erase k, ↑Z * coulombKernel a (R l)

Removing a nearest nucleus minimizes the remaining nuclear potential.

theorem LiebThirring.nuclearPotential_eq_screened_add {M : ℕ} (hM : 1 ≤ M) (Z : NNReal) (R : Fin M → Position) (a : Position) : ∑ k : Fin M, ↑Z * coulombKernel a (R k) = screenedPotential Z R a + ↑Z * (nearestNucleusDistance R a)⁻¹

The nuclear potential splits into its screened part and nearest singularity.

theorem LiebThirring.shell_nuclear_distance_bound {M : ℕ} (R : Fin M → Position) (a y : Position) (d : ℝ) (hd : ∀ (k : Fin M), d ≤ ‖a - R k‖) (hy : ‖y - a‖ = d / 2) : ENNReal.ofReal (d / 2) ≤ nearestNucleusDistance R y

On a half-nearest-distance sphere every nuclear distance is at least the radius.

theorem LiebThirring.lintegral_shell_nuclearPotential {M : ℕ} (Z : NNReal) (R : Fin M → Position) (a : Position) {d : ℝ} (hd : 0 < d) (hbound : ∀ (k : Fin M), d ≤ ‖a - R k‖) : ∫⁻ (y : Position), ∑ k : Fin M, ↑Z * coulombKernel y (R k) ∂shell a (d / 2) = ∑ k : Fin M, ↑Z * coulombKernel a (R k)

Newton gives exact attraction to each nucleus from an electron shell.

theorem LiebThirring.lintegral_shell_nearest_le {M : ℕ} (Z : NNReal) (R : Fin M → Position) (a : Position) {d : ℝ} (hd : 0 < d) (hbound : ∀ (k : Fin M), d ≤ ‖a - R k‖) : ∫⁻ (y : Position), ↑Z * (nearestNucleusDistance R y)⁻¹ ∂shell a (d / 2) ≤ ↑Z * (ENNReal.ofReal (d / 2))⁻¹

The shell contribution of the nearest singularity is at most 2Z/d.

theorem LiebThirring.measurable_nearestNucleusDistance {M : ℕ} (R : Fin M → Position) : Measurable (nearestNucleusDistance R)

Measurability of the nearest-nucleus distance, including the empty infimum.

theorem LiebThirring.nuclearPotential_le_shell_screened_add {M : ℕ} (hM : 1 ≤ M) (Z : NNReal) (R : Fin M → Position) (a : Position) {d : ℝ} (hd : 0 < d) (hbound : ∀ (k : Fin M), d ≤ ‖a - R k‖) : ∑ k : Fin M, ↑Z * coulombKernel a (R k) ≤ ∫⁻ (y : Position), screenedPotential Z R y ∂shell a (d / 2) + ↑Z * (ENNReal.ofReal (d / 2))⁻¹

Additive attraction estimate on one shell; its screened integral is kept intact.