The 1D diffusion kernel converges to a Dirac mass as t → 0⁺

Proved

FickDiffusion.heatKernel_tendsto_initial

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

diffusionpde

Let $D>0$ , let $f:\mathbb R\to\mathbb R$ be continuous and bounded, and let $x\in\mathbb R$ . Then

\lim_{t\to0^+}\int_{-\infty}^{\infty}\frac{1}{\sqrt{4\pi Dt}}\exp\Big(-\frac{(x-y)^2}{4Dt}\Big)f(y)\,dy=f(x).

Equivalently, $\varphi_D(\cdot,t)\to\delta_0$ in the sense of distributions tested against bounded continuous functions: the diffusion kernel is the solution of Fick's second law started from a unit point source.

Formalization Note The limit is taken along $t\to0$ with $t>0$ (𝓝[>] 0). Boundedness is stated as the existence of $C$ with $|f(y)|\le C$ for all $y$ .

Preamble

import Mathlib
import Definitions.Def_FickDiffusion_defs

open Real Filter Topology MeasureTheory

Formal statement

namespace FickDiffusion

theorem heatKernel_tendsto_initial (D : ℝ) (hD : 0 < D) (f : ℝ → ℝ) (hf : Continuous f)
    (hbdd : ∃ C, ∀ y, |f y| ≤ C) (x : ℝ) :
    Tendsto (fun t => ∫ y, heatKernel D (x - y) t * f y) (𝓝[>] 0) (𝓝 (f x)) := 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): φ is the fundamental solution (heat kernel)

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 every real $D>0$ , every continuous function $f:\mathbb R\to\mathbb R$ for which there is a constant $C$ with $|f(y)|\le C$ for all $y$ , and every $x\in\mathbb R$ : the function

t\;\mapsto\;\int_{\mathbb R}K(x-y,t)\,f(y)\,dy,\qquad K(z,t)=\frac{1}{\sqrt{4\pi Dt}}\exp\!\Big(\frac{-z^2}{4Dt}\Big),

(Bochner integral in $y$ , with value $0$ if not integrable) tends to $f(x)$ as $t\to0$ through strictly positive values $t>0$ (right-sided limit at $0$ ; values at $t\le0$ are irrelevant).

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