Fourier transform of the Yukawa potential: $\hat V(k) = -g^2\,4\pi/(|k|^2+(\alpha m)^2)$

Proved

YukawaPotential.yukawaPotential_fourier_transform

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

mathematical-physicsyukawa-potential

Let $g\in\mathbb R$ , $\alpha>0$ and $m>0$ , and let $V(r)=-g^2e^{-\alpha m r}/r$ . For every $k\in\mathbb R^3$ ,

\int_{\mathbb R^3} e^{-i\,k\cdot x}\,V(|x|)\,d^3x \;=\; -g^2\,\frac{4\pi}{|k|^2+(\alpha m)^2}.

This is the momentum-space form of the Yukawa potential: the sections Fourier transform and Feynman amplitude identify $-g^2\cdot 4\pi/(k^2+m^2)$ (with $\alpha=1$ ), the lowest-order single-meson-exchange amplitude, as the Fourier transform of the Yukawa potential, with $4\pi/(k^2+m^2)$ the propagator (Green's function) of the Klein–Gordon equation.

Formalization Note The integral is a Lebesgue (Bochner) integral over EuclideanSpace ℝ (Fin 3), which converges absolutely for $\alpha m>0$ ; the value of the integrand at the single point $x=0$ is irrelevant. The convention is $\hat V(k)=\int e^{-ik\cdot x}V(|x|)\,d^3x$ , matching the inverse formula $V=(2\pi)^{-3}\int e^{ik\cdot x}\hat V\,d^3k$ of the article.

Preamble

import Mathlib
import Definitions.Def_YukawaPotential_Defs

open MeasureTheory Filter Topology

Formal statement

namespace YukawaPotential
theorem yukawaPotential_fourier_transform (g α m : ℝ) (hα : 0 < α) (hm : 0 < m)
    (k : EuclideanSpace ℝ (Fin 3)) :
    ∫ x : EuclideanSpace ℝ (Fin 3),
        Complex.exp (-(Complex.I * (inner ℝ k x : ℝ))) * ((yukawaPotential g α m ‖x‖ : ℝ) : ℂ) =
      ((-g ^ 2 * (4 * Real.pi / (‖k‖ ^ 2 + (α * m) ^ 2)) : ℝ) : ℂ) := by sorry
end YukawaPotential

Source

Wikipedia, "Yukawa potential", revision oldid=1371658231, https://en.wikipedia.org/w/index.php?title=Yukawa_potential&oldid=1371658231, sections 'Fourier transform' and 'Feynman amplitude': V(k) = -g² 4π/(k² + m²) 'is seen to be the Fourier transform of the Yukawa potential'.

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 $g$ and real numbers $\alpha>0$ , $m>0$ , and a vector $k\in\mathbb R^3$ (arbitrary, including $k=0$ ). The statement asserts the equality of complex numbers

\int_{\mathbb R^3} e^{-i\,\langle k,x\rangle}\;\Bigl(-g^2\,\frac{e^{-\alpha m |x|}}{|x|}\Bigr)\,dx \;=\; -g^2\cdot\frac{4\pi}{|k|^2+(\alpha m)^2},

where the left side is the Bochner integral with respect to Lebesgue measure on $\mathbb R^3$ , $\langle k,x\rangle$ is the Euclidean inner product, $|\cdot|$ the Euclidean norm, the integrand at $x=0$ takes the value $0$ (division convention), and the right side is a real number viewed as a complex number. If the integrand were not integrable the left side would default to $0$ ; for $g=0$ both sides are $0$ .

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

Fourier transform of the Yukawa potential: V^(k)=−g2 4π/(∣k∣2+(αm)2)\hat V(k) = -g^2\,4\pi/(|k|^2+(\alpha m)^2)V^(k)=−g24π/(∣k∣2+(αm)2)

Fourier transform of the Yukawa potential: $\hat V(k) = -g^2\,4\pi/(|k|^2+(\alpha m)^2)$