Continuity equation: integral form $\iff$ differential form

Proved

ContinuityEqWiki.integral_form_iff_differential_form

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

continuity-equationmathematical-physics

Let $\rho:\mathbb R\times\mathbb R^3\to\mathbb R$ be the volume density of a quantity $q$ , $\mathbf j:\mathbb R\times\mathbb R^3\to\mathbb R^3$ its flux, and $\sigma:\mathbb R\times\mathbb R^3\to\mathbb R$ its generation rate per unit volume per unit time. Assume $\rho$ and $\mathbf j$ are $C^1$ jointly in $(t,x)$ and $\sigma$ is continuous. Then the following are equivalent.

Integral form. For every box $V=\prod_i[a_i,b_i]$ with $a_i<b_i$ and every time $t$ ,

\frac{dq}{dt}+\oint_{\partial V}\mathbf j\cdot d\mathbf S=\Sigma,\qquad q(t)=\int_V\rho(t,x)\,dx,\quad \Sigma(t)=\int_V\sigma(t,x)\,dx .

Differential form. For every $t$ and $x$ ,

\frac{\partial\rho}{\partial t}+\nabla\cdot\mathbf j=\sigma .

This is the central statement of the source: any continuity equation can be expressed either in integral form, for finite regions, or in differential form, at points.

Formalization Note The source quantifies over all closed surfaces $S$ enclosing a volume $V$ . Here $V$ ranges over non-degenerate axis-parallel boxes, the setting of Mathlib's divergence theorem. This weakens the hypothesis of the direction (1) $\Rightarrow$ (2) and the conclusion of (2) $\Rightarrow$ (1).

Preamble

import Mathlib
import Definitions.Def_ContinuityEqWiki_Defs

Formal statement

namespace ContinuityEqWiki

theorem integral_form_iff_differential_form
    (ρ : ℝ → Space → ℝ) (j : ℝ → Space → Space) (σ : ℝ → Space → ℝ)
    (hρ : ContDiff ℝ 1 (Function.uncurry ρ)) (hj : ContDiff ℝ 1 (Function.uncurry j))
    (hσ : Continuous (Function.uncurry σ)) :
    IntegralForm ρ j σ ↔ DifferentialForm ρ j σ := by sorry

end ContinuityEqWiki

Source

Wikipedia, "Continuity equation", revision oldid=1378634825, https://en.wikipedia.org/w/index.php?title=Continuity_equation&oldid=1378634825, section "General equation", subsections "Integral form" and "Differential form"

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - drafting agent, non-blind read-back

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement it describes, at the explicit request of the proposal owner. Its author knew the source text and the intended meaning while writing it, so it must not be mistaken for a blind, independent audit. Reviewers should compare the Lean code against the source themselves.

Let $\rho,\sigma:\mathbb R\times\mathbb R^3\to\mathbb R$ and $\mathbf j:\mathbb R\times\mathbb R^3\to\mathbb R^3$ (written $f(t,x)$ ). Assume $(t,x)\mapsto\rho(t,x)$ and $(t,x)\mapsto\mathbf j(t,x)$ are $C^1$ on $\mathbb R\times\mathbb R^3$ and $(t,x)\mapsto\sigma(t,x)$ is continuous. The statement is the equivalence of:

for all $a,b\in\mathbb R^3$ with $a_i<b_i$ for $i=0,1,2$ , and all $t\in\mathbb R$ ,

\frac{d}{ds}\Big|_{s=t}\int_{[a,b]}\rho(s,x)\,dx+\sum_{i=0}^{2}\left(\int_{[a',b']}\mathbf j(t,\iota_i(b_i,y))_i\,dy-\int_{[a',b']}\mathbf j(t,\iota_i(a_i,y))_i\,dy\right)=\int_{[a,b]}\sigma(t,x)\,dx,

where $a',b'\in\mathbb R^2$ are $a,b$ with coordinate $i$ deleted and $\iota_i(s,y)$ inserts $s$ as coordinate $i$ into $y\in\mathbb R^2$ (the derivative is the one-variable derivative, junk $0$ if it did not exist); 2. for all $t\in\mathbb R$ and $x\in\mathbb R^3$ ,

\partial_t\rho(t,x)+\sum_{i=0}^{2}\partial_i\big(\mathbf j(t,\cdot)_i\big)(x)=\sigma(t,x).

View graph

Continuity equation: integral form ⟺ \iff⟺ differential form

Continuity equation: integral form $\iff$ differential form