Coulomb potentials and energies of positive measures

The Coulomb potential Φ_α(x) = ∫ |x - y|⁻¹ dα(y) of a positive measure, in ℝ≥0∞.

The mutual Coulomb energy I(α, β) = double integral |x - y|⁻¹ dα(x) dβ(y) of positive measures, in ℝ≥0∞ (no factor 1/2).

noncomputable def LiebThirring.coulombPotential (α : MeasureTheory.Measure Position) (x : Position) : ENNReal

The Coulomb potential Φ_α(x) = ∫ |x - y|⁻¹ dα(y) of a positive measure, in ℝ≥0∞.

Equations

• LiebThirring.coulombPotential α x = ∫⁻ (y : LiebThirring.Position), LiebThirring.coulombKernel x y ∂α

noncomputable def LiebThirring.coulombEnergy (α β : MeasureTheory.Measure Position) : ENNReal

The mutual Coulomb energy I(α, β) = double integral |x - y|⁻¹ dα(x) dβ(y) of positive measures, in ℝ≥0∞ (no factor 1/2).

Equations

• LiebThirring.coulombEnergy α β = ∫⁻ (x : LiebThirring.Position), LiebThirring.coulombPotential β x ∂α