Import stability of matter and the kinetic Lieb–Thirring inequality

LeanPool/LiebThirring.lean

@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2026 Scott Armstrong, Amélie Loher. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Armstrong, Amélie Loher
+-/
+
+module
+
+public import LeanPool.LiebThirring.Theorems.Baxter
+public import LeanPool.LiebThirring.Theorems.KineticEnergySchwartz
+public import LeanPool.LiebThirring.Theorems.KineticLiebThirring
+public import LeanPool.LiebThirring.Theorems.StabilityOfMatter
+public import LeanPool.LiebThirring.Theorems.StabilityOfMatterReal
+
+/-!
+# Stability of matter and the kinetic Lieb–Thirring inequality
+
+Source: arxiv:2007.09326, url:https://github.com/scottnarmstrong/LiebThirring/tree/8bf4656f07f5aaa227b0b850d77b16976915bbd4
+Authors: Scott Armstrong, Amélie Loher
+Status: verified
+Main declarations: `LiebThirring.stability_of_matter`
+Tags: mathematical-physics, stability-of-matter, lieb-thirring, coulomb-energy, fourier-analysis
+MSC: 81Q10, 35P15, 46N50
+-/
+
+/-!
+# Stability of non-relativistic Coulomb matter
+
+The stability, kinetic and electrostatic dependency closure from Armstrong and Loher.
+Imported from
+https://github.com/scottnarmstrong/LiebThirring/tree/8bf4656f07f5aaa227b0b850d77b16976915bbd4.
+The upstream ionization, thermodynamic-limit and Thomas–Fermi developments are separate from this
+scope.
+
+The kinetic and stability formulations follow Frank, arXiv:2007.09326, Section 2.
+The explicit Rumin coefficient and Baxter correction follow Lundholm’s lecture notes,
+Theorems 6.1 and 7.2; this import does not assert an optimal kinetic constant.
+Lundholm’s notes: https://www.math.lmu.de/~lundholm/methmmp.pdf.
+
+Scott Armstrong acknowledges ERC grant No. 101200828. Amélie Loher acknowledges support from the
+Fondation Sciences Mathématiques de Paris.
+-/

LeanPool/LiebThirring/Analysis/FundamentalSolution.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2026 Scott Armstrong, Amélie Loher. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Armstrong, Amélie Loher
+-/
+module
+
+-- Imported from upstream commit 8bf4656f07f5aaa227b0b850d77b16976915bbd4.
+-- Imports adapted for Lean Pool.
+
+public import LeanPool.LiebThirring.Analysis.FundamentalSolutionMeasures
+import LeanPool.LiebThirring.Analysis.FundamentalSolutionApproximation
+import LeanPool.LiebThirring.Analysis.FundamentalSolutionLimits
+
+/-!
+# The three-dimensional Coulomb fundamental solution
+
+The Coulomb fundamental-solution identity, the fundamental solution. Together with
+`integrable_inv_norm_sub_mul_laplacian`, this asserts absolute integrability and the value of
+the pairing. `C²` suffices, so in particular the identity holds for every smooth compactly
+supported test.
+
+A finite positive charge with bounded extended potential satisfies the test-function identity
+the fundamental solution. Local integrability is supplied by
+`locallyIntegrable_coulombPotential_toReal`, and absolute test-pairing integrability by
+`integrable_coulombPotential_toReal_mul_laplacian`.
+-/
+
+public section
+
+open MeasureTheory Filter InnerProductSpace Laplacian
+open scoped Topology ENNReal
+
+namespace LiebThirring
+
+/-- The Coulomb fundamental-solution identity, the fundamental solution.
+Together with `integrable_inv_norm_sub_mul_laplacian`, this asserts absolute
+integrability and the value of the pairing. `C²` suffices, so in particular
+the identity holds for every smooth compactly supported test. -/
+theorem integral_inv_norm_sub_mul_laplacian {f : Position → ℝ}
+    (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f) (y : Position) :
+    (∫ x, ‖x - y‖⁻¹ * Δ f x) = -4 * Real.pi * f y := by
+  have hleft := tendsto_integral_regularizedCoulombKernel_sub_mul_laplacian hf hfc y
+  have hright := (tendsto_integral_coulombApproximationDensity_sub_mul
+    hf.continuous hfc y).neg
+  have ht : Tendsto (fun ε : ℝ => ∫ x, regularizedCoulombKernel ε (x - y) * Δ f x)
+      (𝓝[>] 0) (𝓝 (-4 * Real.pi * f y)) := by
+    have h := hright.congr' (by
+      filter_upwards [self_mem_nhdsWithin] with ε (hε : 0 < ε)
+      exact (integral_regularizedCoulombKernel_sub_mul_laplacian hε hf hfc y).symm)
+    simpa only [neg_mul] using h
+  exact tendsto_nhds_unique hleft ht
+
+/-- A finite positive charge with bounded extended potential satisfies
+the test-function identity the fundamental solution. Local integrability is supplied by
+`locallyIntegrable_coulombPotential_toReal`, and absolute test-pairing
+integrability by `integrable_coulombPotential_toReal_mul_laplacian`. -/
+theorem integral_coulombPotential_toReal_mul_laplacian
+    (β : Measure Position) [IsFiniteMeasure β] {C : ℝ≥0∞}
+    (hC : C ≠ ⊤) (hβ : ∀ x, coulombPotential β x ≤ C)
+    {f : Position → ℝ} (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f) :
+    (∫ x, (coulombPotential β x).toReal * Δ f x) = -4 * Real.pi * ∫ y, f y ∂β := by
+  rw [integral_coulombPotential_toReal_mul_laplacian_eq_integral_integral β hC hβ hf hfc]
+  simp_rw [integral_inv_norm_sub_mul_laplacian hf hfc]
+  exact integral_const_mul _ _
+
+end LiebThirring
+
+end

LeanPool/LiebThirring/Analysis/FundamentalSolutionApproximation.lean

@@ -0,0 +1,109 @@
+/-
+Copyright (c) 2026 Scott Armstrong, Amélie Loher. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Armstrong, Amélie Loher
+-/
+module
+
+-- Imported from upstream commit 8bf4656f07f5aaa227b0b850d77b16976915bbd4.
+-- Imports adapted for Lean Pool.
+
+public import LeanPool.LiebThirring.Analysis.FundamentalSolutionRadial
+
+/-!
+# Approximate identity from the regularized Coulomb density
+
+Scaling of the fundamental solution's regularization density in physical dimension three.
+
+The density pairing can be evaluated after dilating about its pole.
+-/
+
+public section
+
+open MeasureTheory Filter Set
+open scoped Topology
+
+namespace LiebThirring
+
+/-- Scaling of the fundamental solution's regularization density in physical dimension three. -/
+theorem coulombApproximationDensity_smul {ε : ℝ} (hε : 0 < ε) (x : Position) :
+    coulombApproximationDensity ε (ε • x) =
+      (ε ^ 3)⁻¹ * coulombApproximationDensity 1 x := by
+  unfold coulombApproximationDensity
+  rw [norm_smul, Real.norm_eq_abs, abs_of_pos hε]
+  have hs : (ε * ‖x‖) ^ 2 + ε ^ 2 = ε ^ 2 * (‖x‖ ^ 2 + 1) := by ring
+  rw [hs, Real.mul_rpow (sq_nonneg _) (by positivity)]
+  have hp : (ε ^ 2) ^ (-(5 / 2 : ℝ)) = (ε ^ 5)⁻¹ := by
+    rw [← Real.rpow_natCast ε 2, ← Real.rpow_mul hε.le]
+    norm_num
+  rw [hp]
+  norm_num only [one_pow, mul_one]
+  field_simp [hε.ne']
+
+/-- The density pairing can be evaluated after dilating about its pole. -/
+theorem integral_coulombApproximationDensity_sub_mul {ε : ℝ} (hε : 0 < ε)
+    (f : Position → ℝ) (y : Position) :
+    (∫ x, coulombApproximationDensity ε (x - y) * f x) =
+      ∫ x, coulombApproximationDensity 1 x * f (y + ε • x) := by
+  have ht : (∫ x, coulombApproximationDensity ε (x - y) * f x) =
+      ∫ x, coulombApproximationDensity ε x * f (y + x) := by
+    have h := integral_add_right_eq_self y (μ := (volume : Measure Position))
+      (f := fun x => coulombApproximationDensity ε (x - y) * f x)
+    calc
+      _ = ∫ x, coulombApproximationDensity ε x * f (x + y) := by
+        simpa only [add_sub_cancel_right] using h.symm
+      _ = _ := by
+        apply integral_congr_ae
+        filter_upwards with x
+        rw [add_comm x y]
+  rw [ht]
+  have h := Measure.integral_comp_smul_of_nonneg (volume : Measure Position)
+    (fun x => coulombApproximationDensity ε x * f (y + x)) ε (hR := hε.le)
+  simp only [Position, finrank_euclideanSpace_fin, smul_eq_mul] at h
+  simp_rw [coulombApproximationDensity_smul hε] at h
+  rw [show (fun x => (ε ^ 3)⁻¹ * coulombApproximationDensity 1 x * f (y + ε • x)) =
+      (fun x => (ε ^ 3)⁻¹ * (coulombApproximationDensity 1 x * f (y + ε • x))) by
+        funext x; ring, integral_const_mul] at h
+  exact (mul_left_cancel₀ (inv_ne_zero (pow_ne_zero _ hε.ne')) h).symm
+
+/-- The regularized density converges to a point mass of weight `4π`. -/
+theorem tendsto_integral_coulombApproximationDensity_sub_mul
+    {f : Position → ℝ} (hf : Continuous f) (hfc : HasCompactSupport f) (y : Position) :
+    Tendsto (fun ε : ℝ => ∫ x, coulombApproximationDensity ε (x - y) * f x)
+      (𝓝[>] 0) (𝓝 (4 * Real.pi * f y)) := by
+  obtain ⟨M, hM⟩ := (hfc.isCompact_range hf).isBounded.exists_norm_le
+  have hbound (x : Position) : ‖f x‖ ≤ M := hM (f x) (mem_range_self x)
+  have ht : Tendsto (fun ε : ℝ =>
+      ∫ x, coulombApproximationDensity 1 x * f (y + ε • x)) (𝓝[>] 0)
+      (𝓝 (∫ x, coulombApproximationDensity 1 x * f y)) := by
+    apply tendsto_integral_filter_of_dominated_convergence
+      (fun x => coulombApproximationDensity 1 x * M)
+    · filter_upwards with ε
+      have hq : Continuous (coulombApproximationDensity 1) := by
+        unfold coulombApproximationDensity
+        apply Continuous.mul continuous_const
+        exact ((continuous_norm.pow 2).add continuous_const).rpow_const
+          (fun x => Or.inl (norm_sq_add_sq_pos zero_lt_one x).ne')
+      have hm : Continuous (fun x : Position => y + ε • x) :=
+        continuous_const.add (continuous_id.const_smul ε)
+      exact (hq.mul (hf.comp hm)).aestronglyMeasurable
+    · filter_upwards with ε
+      filter_upwards with x
+      rw [norm_mul, Real.norm_eq_abs, abs_of_nonneg (coulombApproximationDensity_nonneg _ _)]
+      exact mul_le_mul_of_nonneg_left (hbound _) (coulombApproximationDensity_nonneg _ _)
+    · exact integrable_coulombApproximationDensity_one.mul_const M
+    · filter_upwards with x
+      have hi : Tendsto (fun ε : ℝ => y + ε • x) (𝓝[>] 0) (𝓝 y) := by
+        have hiε : Tendsto (fun ε : ℝ => ε) (𝓝[>] 0) (𝓝 0) :=
+          tendsto_id.mono_left nhdsWithin_le_nhds
+        simpa only [zero_smul, add_zero] using
+          (tendsto_const_nhds (x := y)).add (hiε.smul (tendsto_const_nhds (x := x)))
+      exact tendsto_const_nhds.mul ((hf.tendsto y).comp hi)
+  rw [integral_mul_const, integral_coulombApproximationDensity_one] at ht
+  apply ht.congr'
+  filter_upwards [self_mem_nhdsWithin] with ε (hε : 0 < ε)
+  exact (integral_coulombApproximationDensity_sub_mul hε f y).symm
+
+end LiebThirring
+
+end

LeanPool/LiebThirring/Analysis/FundamentalSolutionIntegrability.lean

@@ -0,0 +1,123 @@
+/-
+Copyright (c) 2026 Scott Armstrong, Amélie Loher. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Armstrong, Amélie Loher
+-/
+module
+
+-- Imported from upstream commit 8bf4656f07f5aaa227b0b850d77b16976915bbd4.
+-- Imports adapted for Lean Pool.
+
+public import Mathlib.MeasureTheory.Function.LocallyIntegrable
+public import Mathlib.Analysis.InnerProductSpace.Laplacian
+public import LeanPool.LiebThirring.Electrostatics.Basic
+import all LeanPool.LiebThirring.Electrostatics.Basic
+import LeanPool.LiebThirring.Electrostatics.SphereRadial
+import LeanPool.LiebThirring.Analysis.WeakHarmonicConvolution
+
+/-!
+# Integrability for the three-dimensional fundamental solution
+
+The real inverse-norm kernel is integrable on every ball about its pole.
+
+The inverse-norm singularity is locally integrable in three dimensions.
+-/
+
+public section
+
+open MeasureTheory Set Metric InnerProductSpace Laplacian
+open scoped Topology ENNReal
+
+namespace LiebThirring
+
+/-- The real inverse-norm kernel is integrable on every ball about its pole. -/
+theorem integrableOn_inv_norm_sub_ball (y : Position) (R : ℝ) :
+    IntegrableOn (fun x : Position => ‖x - y‖⁻¹) (ball y R) := by
+  have hzero : IntegrableOn (fun x : Position => ‖x‖⁻¹) (ball 0 R) := by
+    apply (integrableOn_fun_norm_addHaar (volume : Measure Position)).mpr
+    simp only [Position, finrank_euclideanSpace_fin, Nat.reduceSub, smul_eq_mul]
+    have hr : IntegrableOn (fun r : ℝ => r) (Ioo 0 R) :=
+      continuous_id.integrableOn_Icc.mono_set Ioo_subset_Icc_self
+    apply hr.congr_fun _ measurableSet_Ioo
+    intro r hr
+    field_simp
+  have hpre : (fun x : Position => x - y) ⁻¹' ball 0 R = ball y R := by
+    ext x
+    simp only [mem_preimage, mem_ball, dist_eq_norm, sub_zero]
+  have he := (Homeomorph.subRight y).measurableEmbedding
+  simpa only [Function.comp_def, hpre] using
+    ((measurePreserving_sub_right (volume : Measure Position) y).integrableOn_comp_preimage
+      he).mpr hzero
+
+/-- The inverse-norm singularity is locally integrable in three dimensions. -/
+theorem locallyIntegrable_inv_norm_sub (y : Position) :
+    LocallyIntegrable (fun x : Position => ‖x - y‖⁻¹) := by
+  intro x
+  refine ⟨ball y (‖x - y‖ + 1), isOpen_ball.mem_nhds ?_,
+    integrableOn_inv_norm_sub_ball y _⟩
+  rw [mem_ball, dist_eq_norm]
+  exact lt_add_one _
+
+/-- A `C²` function has continuous Mathlib Laplacian on `Position`. -/
+theorem continuous_laplacian_position {f : Position → ℝ} (hf : ContDiff ℝ 2 f) :
+    Continuous (Δ f) := by
+  have heq : Δ f = fun x => ∑ i,
+      fderiv ℝ (fderiv ℝ f) x ((stdOrthonormalBasis ℝ Position) i)
+        ((stdOrthonormalBasis ℝ Position) i) := by
+    funext x
+    simp only [laplacian_eq_iteratedFDeriv_stdOrthonormalBasis,
+      iteratedFDeriv_two_apply, Matrix.cons_val_zero, Matrix.cons_val_one]
+  rw [heq]
+  exact continuous_finsetSum _ (fun i _ => continuous_kernel_hessian hf _ _)
+
+/-- Taking the Laplacian preserves compact support. -/
+theorem hasCompactSupport_laplacian_position {f : Position → ℝ}
+    (hf : HasCompactSupport f) : HasCompactSupport (Δ f) := by
+  have heq : Δ f = ∑ i,
+      (fun x => fderiv ℝ (fderiv ℝ f) x ((stdOrthonormalBasis ℝ Position) i)
+        ((stdOrthonormalBasis ℝ Position) i)) := by
+    funext x
+    simp only [laplacian_eq_iteratedFDeriv_stdOrthonormalBasis,
+      iteratedFDeriv_two_apply, Matrix.cons_val_zero, Matrix.cons_val_one, Finset.sum_apply]
+  rw [heq]
+  exact HasCompactSupport.finset_sum (fun i _ => hasCompactSupport_kernel_hessian hf _ _)
+
+/-- Absolute integrability in the fundamental solution, before the distributional identity. -/
+theorem integrable_inv_norm_sub_mul_laplacian {f : Position → ℝ}
+    (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f) (y : Position) :
+    Integrable (fun x => ‖x - y‖⁻¹ * Δ f x) :=
+  (locallyIntegrable_inv_norm_sub y).integrable_smul_right_of_hasCompactSupport
+    (continuous_laplacian_position hf) (hasCompactSupport_laplacian_position hfc)
+
+/-- The shared extended potential is measurable for an s-finite charge. -/
+theorem measurable_coulombPotential (β : Measure Position) [SFinite β] :
+    Measurable (coulombPotential β) := by
+  unfold coulombPotential
+  have hK : Measurable (Function.uncurry coulombKernel) :=
+    ((measurable_fst.sub measurable_snd).norm.ennreal_ofReal).inv
+  exact hK.lintegral_prod_right (ν := β)
+
+/-- Bounded extended Coulomb potentials are locally integrable after `toReal`.
+The bound is on the extended potential, so it also asserts finiteness everywhere. -/
+theorem locallyIntegrable_coulombPotential_toReal (β : Measure Position) [SFinite β]
+    {C : ℝ≥0∞} (hC : C ≠ ⊤) (hβ : ∀ x, coulombPotential β x ≤ C) :
+    LocallyIntegrable (fun x => (coulombPotential β x).toReal) := by
+  apply (locallyIntegrable_const (c := C.toReal)).mono
+    (measurable_coulombPotential β).ennreal_toReal.aestronglyMeasurable
+  filter_upwards with x
+  rw [Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg,
+    Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg]
+  exact ENNReal.toReal_mono hC (hβ x)
+
+/-- The left-hand test-function pairing in the fundamental solution is absolutely integrable. -/
+theorem integrable_coulombPotential_toReal_mul_laplacian
+    (β : Measure Position) [SFinite β] {C : ℝ≥0∞}
+    (hC : C ≠ ⊤) (hβ : ∀ x, coulombPotential β x ≤ C)
+    {f : Position → ℝ} (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f) :
+    Integrable (fun x => (coulombPotential β x).toReal * Δ f x) :=
+  (locallyIntegrable_coulombPotential_toReal β hC hβ).integrable_smul_right_of_hasCompactSupport
+      (continuous_laplacian_position hf) (hasCompactSupport_laplacian_position hfc)
+
+end LiebThirring
+
+end