Fick's second law: φ(x,t) = (4πDt)^{-1/2} exp(-x²/(4Dt)) is its fundamental solution

Proved

FickDiffusion.heatKernel_fundamental_solution

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

diffusionpde

Let $D>0$ be a diffusion coefficient and let

\varphi_D(x,t)=\frac{1}{\sqrt{4\pi Dt}}\exp\Big(-\frac{x^2}{4Dt}\Big)\qquad(x\in\mathbb R,\ t>0).

Then $\varphi_D$ is the fundamental solution of Fick's second law $\partial_t\varphi=D\,\partial_x^2\varphi$ :

it solves the equation: for all $x\in\mathbb R$ and $t>0$ ,

\frac{\partial\varphi_D}{\partial t}(x,t)=D\,\frac{\partial^2\varphi_D}{\partial x^2}(x,t);

it carries unit mass: for every $t>0$ , $\displaystyle\int_{-\infty}^{\infty}\varphi_D(x,t)\,dx=1$ ;
it starts from a unit point source: for every bounded continuous $f:\mathbb R\to\mathbb R$ and every $x\in\mathbb R$ ,

\lim_{t\to0^+}\int_{-\infty}^{\infty}\varphi_D(x-y,t)\,f(y)\,dy=f(x).

This is the article's identification of the fundamental solution of Fick's second law with the heat kernel (thermal diffusivity replaced by $D$ ); every solution of the 1D diffusion equation with bounded continuous initial data is obtained by convolving that data with $\varphi_D$ .

Formalization Note Derivatives are Mathlib's one-variable deriv; the limit in clause 3 is the right-sided limit 𝓝[>] 0; boundedness of $f$ is the existence of $C$ with $|f(y)|\le C$ .

Preamble

import Mathlib
import Definitions.Def_FickDiffusion_defs

open Real Filter Topology MeasureTheory

Formal statement

namespace FickDiffusion

theorem heatKernel_fundamental_solution (D : ℝ) (hD : 0 < D) :
    (∀ x t : ℝ, 0 < t → deriv (fun s => heatKernel D x s) t =
        D * deriv (fun y => deriv (fun z => heatKernel D z t) y) x) ∧
    (∀ t : ℝ, 0 < t → ∫ x, heatKernel D x t = 1) ∧
    (∀ f : ℝ → ℝ, Continuous f → (∃ 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): "Fick's second law has the same mathematical form as the Heat equation and its fundamental solution is the same as the Heat kernel, except switching thermal conductivity k with diffusion coefficient D"

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$ , with $K(z,s)=\dfrac{1}{\sqrt{4\pi D s}}\exp\!\big(-z^2/(4Ds)\big)$ (real square root, $0$ on negatives; division by $0$ yields $0$ ), all three of the following hold:

for all real $x$ and all $t>0$ : the derivative at $s=t$ of $s\mapsto K(x,s)$ equals $D$ times the derivative at $y=x$ of the function $y\mapsto\big(\text{derivative at }y\text{ of }z\mapsto K(z,t)\big)$ (one-variable derivatives, value $0$ at non-differentiable points);
for all $t>0$ : $\int_{\mathbb R}K(x,t)\,dx=1$ (Lebesgue/Bochner integral, $0$ if not integrable);
for every continuous $f:\mathbb R\to\mathbb R$ such that some constant $C$ satisfies $|f(y)|\le C$ for all $y$ , and every real $x$ : $\int_{\mathbb R}K(x-y,t)f(y)\,dy\to f(x)$ as $t\to0$ through values $t>0$ .

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