Energy bookkeeping for finite families of electron shells

Bilinearity for a finite family of positive measures, without subtraction.

A symmetric finite double sum consists of its diagonal and twice its upper triangle.

theorem LiebThirring.coulombEnergy_finsetSum {ι : Type u_1} (s : Finset ι) (μ : ι → MeasureTheory.Measure Position) [∀ (i : ι), MeasureTheory.SFinite (μ i)] : coulombEnergy (∑ i ∈ s, μ i) (∑ j ∈ s, μ j) = ∑ i ∈ s, ∑ j ∈ s, coulombEnergy (μ i) (μ j)

Bilinearity for a finite family of positive measures, without subtraction.

theorem LiebThirring.symmetric_sum_eq_diagonal_add {n : ℕ} (f : Fin n → Fin n → ENNReal) (hf : ∀ (i j : Fin n), f i j = f j i) : ∑ i : Fin n, ∑ j : Fin n, f i j = ∑ i : Fin n, f i i + 2 * ∑ i : Fin n, ∑ j : Fin n with i < j, f i j

A symmetric finite double sum consists of its diagonal and twice its upper triangle.

theorem LiebThirring.coulombEnergy_sum_shell_ne_top {N : ℕ} (a : Fin N → Position) (r : Fin N → ℝ) (hr : ∀ (i : Fin N), 0 < r i) : coulombEnergy (∑ i : Fin N, shell (a i) (r i)) (∑ i : Fin N, shell (a i) (r i)) ≠ ⊤

A finite sum of positive-radius electron shells has finite Coulomb energy.

theorem LiebThirring.coulombEnergy_sum_shell_div_two_le {N : ℕ} (x : Configuration N) (r : Fin N → ℝ) (hr : ∀ (i : Fin N), 0 < r i) : coulombEnergy (∑ i : Fin N, shell (particlePosition x i) (r i)) (∑ i : Fin N, shell (particlePosition x i) (r i)) / 2 ≤ electronRepulsion x + (∑ i : Fin N, (ENNReal.ofReal (r i))⁻¹) / 2

Smearing bounds the total half-energy by repulsion and the shell self terms.