Reindexing nuclear repulsion

The symmetric off-diagonal sum counts each nuclear pair twice.

Deleting zero-charge nuclei and reindexing the remaining support preserve nuclear repulsion, including singular configurations.

theorem LiebThirring.Assembly.nuclearRepulsion_double_sum {M : ℕ} (z : Fin M → NNReal) (R : Fin M → Position) : (∑ k : Fin M, ∑ l : Fin M, if k ≠ l then ↑(z k) * ↑(z l) * coulombKernel (R k) (R l) else 0) = 2 * nuclearRepulsion z R

The symmetric off-diagonal sum counts each nuclear pair twice.

theorem LiebThirring.Assembly.nuclearRepulsion_reindex_support {M m : ℕ} (I : Set (Fin M)) (e : Fin m ≃ ↑I) (z : Fin M → NNReal) (R : Fin M → Position) (hz : ∀ k ∉ I, z k = 0) : nuclearRepulsion z R = nuclearRepulsion (fun (j : Fin m) => z ↑(e j)) fun (j : Fin m) => R ↑(e j)

Deleting zero-charge nuclei and reindexing the remaining support preserve nuclear repulsion, including singular configurations.