Extended Coulomb measurability and endpoints

Measurability and endpoint identities for extended Coulomb interactions, including singular values and zero charges.

theorem LiebThirring.Assembly.measurable_coulombKernel : Measurable (Function.uncurry coulombKernel)

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

theorem LiebThirring.Assembly.measurable_nearestNucleusInverse {M : ℕ} (R : Fin M → Position) : Measurable fun (x : Position) => (nearestNucleusDistance R x)⁻¹

theorem LiebThirring.Assembly.measurable_electronRepulsion {N : ℕ} : Measurable electronRepulsion

theorem LiebThirring.Assembly.coulombKernel_eq_of_ne {x y : Position} (h : x ≠ y) : coulombKernel x y = ENNReal.ofReal ‖x - y‖⁻¹

theorem LiebThirring.Assembly.attraction_zero {N M : ℕ} (R : Fin M → Position) (x : Configuration N) : attraction (fun (x : Fin M) => 0) R x = 0

theorem LiebThirring.Assembly.nearestNucleusDistance_restrict_le {M m : ℕ} (R : Fin M → Position) (e : Fin m → Fin M) (x : Position) : nearestNucleusDistance R x ≤ nearestNucleusDistance (R ∘ e) x

theorem LiebThirring.Assembly.nearestNucleusControl_restrict_le {N M m : ℕ} (Z : NNReal) (R : Fin M → Position) (e : Fin m → Fin M) (x : Configuration N) : nearestNucleusControl Z (R ∘ e) x ≤ nearestNucleusControl Z R x

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