Coulomb symmetry and positivity

The defining iterated integral, exposed without changing the shared definitions.

Symmetry by Tonelli; no energy-finiteness assumption is needed.

theorem LiebThirring.coulombEnergy_eq_lintegral (α β : MeasureTheory.Measure Position) : coulombEnergy α β = ∫⁻ (x : Position), ∫⁻ (y : Position), coulombKernel x y ∂β ∂α

The defining iterated integral, exposed without changing the shared definitions.

theorem LiebThirring.coulombEnergy_symm (α β : MeasureTheory.Measure Position) [MeasureTheory.SFinite α] [MeasureTheory.SFinite β] : coulombEnergy α β = coulombEnergy β α

Symmetry by Tonelli; no energy-finiteness assumption is needed.

noncomputable def LiebThirring.coulombFeature (x : Position) (u : ℝ × Position) : ENNReal

The Gaussian feature used to represent the Coulomb kernel.

Equations

• LiebThirring.coulombFeature x u = LiebThirring.gaussianFeature (2 / √Real.pi) (u.1 ^ 2) x u.2

noncomputable def LiebThirring.coulombFeatureMeasure : MeasureTheory.Measure (ℝ × Position)

The parameter-space measure for the Gaussian Coulomb representation.

Equations

• LiebThirring.coulombFeatureMeasure = (MeasureTheory.volume.restrict (Set.Ioi 0)).prod MeasureTheory.volume

theorem LiebThirring.measurable_coulombFeature : Measurable (Function.uncurry coulombFeature)

Joint measurability of the Coulomb feature.

theorem LiebThirring.coulombKernel_eq_lintegral_feature (x y : Position) : coulombKernel x y = ∫⁻ (u : ℝ × Position), coulombFeature x u * coulombFeature y u ∂coulombFeatureMeasure

The Coulomb kernel is an integral Gram kernel, including the diagonal.

instance LiebThirring.instSFiniteProdRealPositionCoulombFeatureMeasure : MeasureTheory.SFinite coulombFeatureMeasure

noncomputable def LiebThirring.coulombTransform (α : MeasureTheory.Measure Position) (u : ℝ × Position) : ENNReal

The nonnegative feature transform of a positive charge.

Equations

• LiebThirring.coulombTransform α u = ∫⁻ (x : LiebThirring.Position), LiebThirring.coulombFeature x u ∂α

theorem LiebThirring.measurable_coulombTransform (α : MeasureTheory.Measure Position) [MeasureTheory.SFinite α] : Measurable (coulombTransform α)

theorem LiebThirring.coulombEnergy_eq_lintegral_transform (α β : MeasureTheory.Measure Position) [MeasureTheory.SFinite α] [MeasureTheory.SFinite β] : coulombEnergy α β = ∫⁻ (u : ℝ × Position), coulombTransform α u * coulombTransform β u ∂coulombFeatureMeasure

Coulomb energies are integral Gram pairings of the feature transforms.

theorem LiebThirring.coulombEnergy_mul_self_le (α β : MeasureTheory.Measure Position) [MeasureTheory.SFinite α] [MeasureTheory.SFinite β] : coulombEnergy α β ^ 2 ≤ coulombEnergy α α * coulombEnergy β β

Extended Coulomb Cauchy–Schwarz. S-finiteness suffices, even when energies are infinite.

theorem LiebThirring.coulombEnergy_ne_top (α β : MeasureTheory.Measure Position) [MeasureTheory.SFinite α] [MeasureTheory.SFinite β] (hα : coulombEnergy α α ≠ ⊤) (hβ : coulombEnergy β β ≠ ⊤) : coulombEnergy α β ≠ ⊤

Finite self-energies imply finite mutual energy, without circular Coulomb Fubini.

theorem LiebThirring.two_mul_coulombEnergy_le (α β : MeasureTheory.Measure Position) [MeasureTheory.SFinite α] [MeasureTheory.SFinite β] (hα : coulombEnergy α α ≠ ⊤) (hβ : coulombEnergy β β ≠ ⊤) : 2 * coulombEnergy α β ≤ coulombEnergy α α + coulombEnergy β β

Positivity of the signed form for the difference of two finite-energy charges.