Example solution 2: mean squared displacement ⟨‖x‖²⟩ = 2nDt

Proved

FickDiffusion.mean_squared_displacement

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

diffusionpde

Let $n\in\mathbb N$ , $D>0$ and $t>0$ . The position (relative to its starting point) of a particle diffusing in $\mathbb R^n$ with diffusion coefficient $D$ has density $\varphi^{(n)}_D(\cdot,t)$ at time $t$ , where

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

Its mean squared displacement is

\int_{\mathbb R^n}\|x\|^2\,\varphi^{(n)}_D(x,t)\,dx=2nDt .

This is the diffusion-length law used throughout the article: the root-mean-square distance travelled grows like $\sqrt{2nDt}$ .

Formalization Note $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with its Lebesgue (volume) measure and Euclidean norm; the Brownian particle is modelled by its Gaussian transition density, i.e. the $n$ -dimensional fundamental solution of Fick's second law. For $n=0$ both sides are $0$ .

Preamble

import Mathlib
import Definitions.Def_FickDiffusion_defs

open Real Filter Topology MeasureTheory

Formal statement

namespace FickDiffusion

theorem mean_squared_displacement (n : ℕ) (D t : ℝ) (hD : 0 < D) (ht : 0 < t) :
    ∫ x, ‖x‖ ^ 2 * heatKernelEuclid n D x t = 2 * n * D * t := 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 "Example solution 2: Brownian particle and mean squared displacement" (p. 7), first displayed equation

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 natural number $n$ and all real $D,t$ with $D>0$ and $t>0$ :

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

where $\mathbb R^n$ is $n$ -dimensional Euclidean space (functions $\{0,\dots,n-1\}\to\mathbb R$ with the Euclidean norm $\|\cdot\|$ ), the integral is the Bochner integral with respect to its standard volume (Lebesgue) measure ( $0$ by convention if not integrable), and $(4\pi Dt)^{-n/2}$ is the real power of a positive base. The case $n=0$ is included (then $\mathbb R^0$ is a single point and the right-hand side is $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