The 1D diffusion kernel has unit mass

Proved

FickDiffusion.heatKernel_integral_eq_one

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

diffusionpde

Let $D>0$ and $t>0$ . Then

\int_{-\infty}^{\infty}\frac{1}{\sqrt{4\pi Dt}}\exp\Big(-\frac{x^2}{4Dt}\Big)\,dx=1 .

The total amount of diffusing substance carried by the fundamental solution is one unit at every positive time; this is the normalization implicit in calling $\varphi_D$ the fundamental solution.

Formalization Note The integral is the Lebesgue integral over $\mathbb R$ ; the integrand is integrable, so no junk value arises.

Preamble

import Mathlib
import Definitions.Def_FickDiffusion_defs

open Real Filter Topology MeasureTheory

Formal statement

namespace FickDiffusion

theorem heatKernel_integral_eq_one (D : ℝ) (hD : 0 < D) (t : ℝ) (ht : 0 < t) :
    ∫ x, heatKernel D x t = 1 := by sorry

end FickDiffusion

Source

Wikipedia, "Fick's laws of diffusion" (PDF snapshot supplied by the proposer, 21 pp.), https://en.wikipedia.org/wiki/Fick%27s_laws_of_diffusion, section "Fick's second law" (p. 4), the fundamental solution φ(x,t)=(4πDt)^{-1/2} exp(-x²/(4Dt))

Read-back

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

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statements, with full knowledge of the source and of the intended meaning, at the explicit instruction of the account owner. It is not a blind audit. Reviewers must not treat it as independent evidence of faithfulness and should compare it directly against the Lean code.

For all real $D,t$ with $D>0$ and $t>0$ :

\int_{\mathbb R}\frac{1}{\sqrt{4\pi D t}}\exp\!\Big(\frac{-x^2}{4Dt}\Big)\,dx\;=\;1,

the integral being the Bochner/Lebesgue integral with respect to Lebesgue measure on $\mathbb R$ (which by convention would be $0$ if the integrand were not integrable).

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph