Diffusion kernels (1D and n-D) and the complementary error function

Definition

FickDiffusion_defs

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

diffusionheat-kernelpde

Three objects used throughout the mission.

One-dimensional diffusion kernel. For a diffusion coefficient $D$ , position $x\in\mathbb R$ and time $t$ ,

\varphi_D(x,t)=\frac{1}{\sqrt{4\pi D t}}\exp\!\Big(-\frac{x^2}{4Dt}\Big).

This is the fundamental solution of Fick's second law $\partial_t\varphi=D\,\partial_x^2\varphi$ (the heat kernel with the thermal diffusivity replaced by $D$ ).

$n$ -dimensional diffusion kernel. For $x\in\mathbb R^n$ with the Euclidean norm $\|x\|$ ,

\varphi^{(n)}_D(x,t)=(4\pi D t)^{-n/2}\exp\!\Big(-\frac{\|x\|^2}{4Dt}\Big).

Complementary error function.

\operatorname{erfc}(x)=\frac{2}{\sqrt\pi}\int_x^{\infty}e^{-s^2}\,ds .

These definitions are only physically meaningful for $D>0$ and $t>0$ ; every theorem of the mission that uses them assumes this explicitly.

Formalization Note Lean's square root returns $0$ on negative inputs, division by $0$ returns $0$ , and the real power uses Real.rpow; these junk values are never reached because all theorems assume $D>0$ , $t>0$ . Mathlib has no error function, so erfc is defined here directly by the (convergent) Gaussian tail integral.

Definition code

import Mathlib

namespace FickDiffusion

open Real

/-- The one-dimensional fundamental solution of Fick's second law
`∂φ/∂t = D ∂²φ/∂x²` (the heat kernel with diffusivity `D`):
`φ(x,t) = 1/√(4πDt) · exp(-x²/(4Dt))`. Meaningful for `D > 0`, `t > 0`. -/
noncomputable def heatKernel (D x t : ℝ) : ℝ :=
  1 / Real.sqrt (4 * π * D * t) * Real.exp (-x ^ 2 / (4 * D * t))

/-- The `n`-dimensional Gaussian diffusion kernel on `ℝⁿ` (Euclidean space):
`φ(x,t) = (4πDt)^(-n/2) · exp(-‖x‖²/(4Dt))`. Meaningful for `D > 0`, `t > 0`. -/
noncomputable def heatKernelEuclid (n : ℕ) (D : ℝ) (x : EuclideanSpace ℝ (Fin n)) (t : ℝ) : ℝ :=
  (4 * π * D * t) ^ (-(n : ℝ) / 2) * Real.exp (-‖x‖ ^ 2 / (4 * D * t))

/-- The complementary error function `erfc x = (2/√π) ∫ₓ^∞ exp(-s²) ds`. -/
noncomputable def erfc (x : ℝ) : ℝ :=
  2 / Real.sqrt π * ∫ s in Set.Ioi x, Real.exp (-s ^ 2)

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, sections "Fick's second law" (p. 4), "Example solution 1" (p. 6), "Example solution 2" (p. 7)

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.

The file declares, inside the namespace FickDiffusion, three real-valued functions and nothing else (no theorems).

heatKernel D x t for real $D,x,t$ is

\frac{1}{\sqrt{4\pi D t}}\cdot\exp\!\Big(\frac{-x^2}{4Dt}\Big),

where $\sqrt{\cdot}$ is the real square root (which returns $0$ for negative arguments), and real division by $0$ returns $0$ . Consequently, if $Dt\le 0$ the prefactor is $1/0=0$ (or $1/\sqrt{\text{negative}}=0$ ), so the function is identically $0$ whenever $Dt\le 0$ ; when $Dt=0$ the exponent is also $0$ .

heatKernelEuclid n D x t for a natural number $n$ , real $D,t$ and $x$ in $n$ -dimensional Euclidean space $\mathbb R^n$ (with the Euclidean norm) is

(4\pi D t)^{-n/2}\cdot\exp\!\Big(\frac{-\|x\|^2}{4Dt}\Big),

where the power is the real power function with real exponent $-n/2$ : for a positive base $b$ it is $b^{-n/2}$ ; for a negative base $b$ it is $|b|^{-n/2}\cos(n\pi/2)$ ; for base $0$ and $n\ge1$ it equals $0$ ; for $n=0$ the prefactor is $1$ .

erfc x for real $x$ is

\frac{2}{\sqrt\pi}\int_{(x,\infty)}e^{-s^2}\,ds,

a Lebesgue (Bochner) integral over the open half-line $(x,\infty)$ ; the integrand is integrable there, so no junk value occurs.

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