Divergence theorem on a box: $\int_V\nabla\cdot F=\oint_{\partial V}F\cdot d\mathbf S$

Proved

ContinuityEqWiki.integral_div_eq_boxFlux

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

continuity-equationmathematical-physics

Let $V=[a,b]=\prod_{i=0}^{2}[a_i,b_i]\subset\mathbb R^3$ be a closed box with $a\le b$ coordinatewise, and let $F:\mathbb R^3\to\mathbb R^3$ be a continuously differentiable vector field. Then

\int_V \nabla\cdot F(x)\,dx=\oint_{\partial V}F\cdot d\mathbf S,

where the right-hand side is the outward flux of $F$ through the six faces of $V$ .

This is the divergence theorem invoked by the source to pass from the integral form of the continuity equation to its differential form.

Formalization Note The closed surface is the boundary of an axis-parallel box, as in Mathlib's divergence theorem; the flux is the sum over $i$ of the face integrals of $F_i$ over $x_i=b_i$ minus those over $x_i=a_i$ .

Preamble

import Mathlib
import Definitions.Def_ContinuityEqWiki_Defs

Formal statement

namespace ContinuityEqWiki

theorem integral_div_eq_boxFlux (F : Space → Space) (hF : ContDiff ℝ 1 F)
    (a b : Space) (hab : a ≤ b) :
    ∫ x in Set.Icc a b, div F x = boxFlux F a b := by sorry

end ContinuityEqWiki

Source

Wikipedia, "Continuity equation", revision oldid=1378634825, https://en.wikipedia.org/w/index.php?title=Continuity_equation&oldid=1378634825, section "Differential form" ("By the divergence theorem, a general continuity equation can also be written in a 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.

For every vector field $F:\mathbb R^3\to\mathbb R^3$ that is continuously differentiable ( $C^1$ ) on all of $\mathbb R^3$ , and all $a,b\in\mathbb R^3$ with $a_i\le b_i$ for $i=0,1,2$ (degenerate boxes with some $a_i=b_i$ are allowed),

\int_{[a,b]}(\nabla\cdot F)(x)\,dx=\sum_{i=0}^{2}\left(\int_{[a',b']}F_i(\iota_i(b_i,y))\,dy-\int_{[a',b']}F_i(\iota_i(a_i,y))\,dy\right),

where $\nabla\cdot F=\sum_i\partial_iF_i$ (partial derivatives as Fréchet derivatives along unit vectors), the left integral is the Lebesgue integral over the order box $[a,b]$ , $a',b'\in\mathbb R^2$ are $a,b$ with coordinate $i$ removed, and $\iota_i(s,y)$ inserts $s$ as the $i$ -th coordinate of $y\in\mathbb R^2$ .

View graph

Divergence theorem on a box: ∫V∇⋅F=∮∂VF⋅dS\int_V\nabla\cdot F=\oint_{\partial V}F\cdot d\mathbf S∫V​∇⋅F=∮∂V​F⋅dS

Divergence theorem on a box: $\int_V\nabla\cdot F=\oint_{\partial V}F\cdot d\mathbf S$