Prove2Me

Yukawa potential as the inverse Fourier transform of −g2 4π/(k2+(αm)2)-g^2\,4\pi/(k^2+(\alpha m)^2)

Open
YukawaPotential.yukawaPotential_inverse_fourier

by Lucas · Oct 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsyukawa-potential

Let g∈Rg\in\mathbb R, α>0\alpha>0, m>0m>0, and let x∈R3x\in\mathbb R^3, x≠0x\neq0. Then

V(∣x∣)=lim⁡Λ→∞  −g2(2π)3∫∣k∣<Λeik⋅x 4π∣k∣2+(αm)2 d3k,V(|x|) = \lim_{\Lambda\to\infty}\;\frac{-g^2}{(2\pi)^3}\int_{|k|<\Lambda} e^{i k\cdot x}\,\frac{4\pi}{|k|^2+(\alpha m)^2}\,d^3k,

where V(r)=−g2e−αmr/rV(r)=-g^2e^{-\alpha m r}/r and k⋅xk\cdot x is the Euclidean inner product.

This is the formula of the section Fourier transform, with the integral over all momenta k∈R3k\in\mathbb R^3 understood as the limit of integrals over balls.

Formalization Note The function 4π/(∣k∣2+(αm)2)4\pi/(|k|^2+(\alpha m)^2) is not Lebesgue-integrable on R3\mathbb R^3, so the integral over all of R3\mathbb R^3 would be assigned the junk value 00 in Lean; the statement therefore takes the limit of the integrals over the open balls of radius Λ\Lambda as Λ→∞\Lambda\to\infty, computed in C\mathbb C.

Preamble
import Mathlib
import Definitions.Def_YukawaPotential_Defs

open MeasureTheory Filter Topology
Formal statement
namespace YukawaPotential
theorem yukawaPotential_inverse_fourier (g α m : ℝ) (hα : 0 < α) (hm : 0 < m)
    (x : EuclideanSpace ℝ (Fin 3)) (hx : x ≠ 0) :
    Tendsto (fun Λ : ℝ => ((-g ^ 2 / (2 * Real.pi) ^ 3 : ℝ) : ℂ) *
        ∫ k in Metric.ball (0 : EuclideanSpace ℝ (Fin 3)) Λ,
          Complex.exp (Complex.I * (inner ℝ k x : ℝ)) *
            ((4 * Real.pi / (‖k‖ ^ 2 + (α * m) ^ 2) : ℝ) : ℂ))
      atTop (𝓝 ((yukawaPotential g α m ‖x‖ : ℝ) : ℂ)) := by sorry
end YukawaPotential
Source
Wikipedia, "Yukawa potential", revision oldid=1371658231, https://en.wikipedia.org/w/index.php?title=Yukawa_potential&oldid=1371658231, section 'Fourier transform': V(r) = (-g²/(2π)³) ∫ e^{ik·r} 4π/(k² + (αm)²) d³k.
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — non-blind, same agent as the drafter

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement it describes, with full knowledge of the source article and of the intended meaning. It was produced at the explicit request of the proposal owner and must not be mistaken for a blind, independent audit.

Fix a real number gg, real numbers α>0\alpha>0 and m>0m>0, and a point x∈R3x\in\mathbb R^3 with x≠0x\neq0. For each real Λ\Lambda define the complex number

I(Λ)=−g2(2π)3∫{k∈R3: ∣k∣<Λ}ei ⟨k,x⟩ 4π∣k∣2+(αm)2 dk,I(\Lambda) = \frac{-g^2}{(2\pi)^3}\int_{\{k\in\mathbb R^3:\ |k|<\Lambda\}} e^{i\,\langle k,x\rangle}\,\frac{4\pi}{|k|^2+(\alpha m)^2}\,dk,

a Bochner integral with respect to Lebesgue measure restricted to the open ball of radius Λ\Lambda about the origin (empty, hence I(Λ)=0I(\Lambda)=0, when Λ≤0\Lambda\le0); ⟨k,x⟩\langle k,x\rangle is the Euclidean inner product and π\pi is the circle constant. The statement asserts that I(Λ)I(\Lambda) converges in C\mathbb C, as Λ→+∞\Lambda\to+\infty, to the real number −g2e−αm∣x∣/∣x∣-g^2 e^{-\alpha m|x|}/|x| (viewed as a complex number).

Human review

  • Endorsed by Shuze Chen · Oct 8, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 8, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph