Interchanging derivatives: $\partial_t(\nabla\cdot F)=\nabla\cdot(\partial_t F)$

Proved

MaxwellWiki.timeDeriv_div_comm

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

electromagnetismmaxwell-equationsvector-calculus

Interchanging time and space derivatives. Let $F:\mathbb{R}\times\mathbb{R}^3\to\mathbb{R}^3$ , $(t,x)\mapsto F(t,x)$ , be of class $C^2$ jointly in $(t,x)$ . Then for all $t\in\mathbb{R}$ and $x\in\mathbb{R}^3$ ,

\frac{\partial}{\partial t}\big(\nabla\cdot F(t,\cdot)\big)(x)=\nabla\cdot\Big(\frac{\partial F}{\partial t}(t,\cdot)\Big)(x).

This is the "interchanging derivatives" step of the Charge conservation section, applied there to $F=\mathbf E$ to turn $\nabla\cdot(\varepsilon_0\,\partial_t\mathbf E)$ into $\varepsilon_0\,\partial_t(\nabla\cdot\mathbf E)$ .

Formalization Note Joint $C^2$ regularity in $(t,x)$ is assumed; the article leaves the needed smoothness implicit.

Preamble

import Mathlib
import Definitions.Def_MaxwellWiki_Defs

open MaxwellWiki

Formal statement

namespace MaxwellWiki

theorem timeDeriv_div_comm (F : ℝ → Vec3 → Vec3) (hF : ContDiff ℝ 2 (Function.uncurry F))
    (t : ℝ) (x : Vec3) :
    timeDeriv (fun s y => div (F s) y) t x = div (fun y => timeDeriv F t y) x := by sorry

end MaxwellWiki

Source

Wikipedia, "Maxwell's equations", https://en.wikipedia.org/wiki/Maxwell%27s_equations (24-page PDF snapshot supplied by the proposer), section "Charge conservation" (p. 8 of the snapshot): "Expanding the divergence of the right-hand side, interchanging derivatives, and applying Gauss's law gives ..."

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - non-blind, same agent as the drafter

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statement (Aristotle, by Harmonic), with full knowledge of the source and of the intended meaning. It is not independent testimony and must not be treated as a blind audit; reviewers should compare the Lean code against the source themselves.

For every $F:\mathbb{R}\to\mathrm{Vec3}\to\mathrm{Vec3}$ such that the two-variable map $(t,x)\mapsto F(t,x)$ on $\mathbb{R}\times\mathbb{R}^3$ is $C^2$ , and for every $t\in\mathbb{R}$ and $x\in\mathrm{Vec3}$ : the derivative at $t$ of the scalar function $s\mapsto(\nabla\cdot F(s,\cdot))(x)$ equals the divergence at $x$ of the vector field $y\mapsto\partial_tF(t,y)$ , where $\partial_tF(t,y)$ is the derivative at $t$ of $s\mapsto F(s,y)$ :

\frac{d}{ds}\Big|_{s=t}\big(\nabla\cdot F(s,\cdot)\big)(x)=\big(\nabla\cdot\partial_tF(t,\cdot)\big)(x).

Divergence is as in the shared definition file. There are no other hypotheses.

View graph

Interchanging derivatives: ∂t(∇⋅F)=∇⋅(∂tF)\partial_t(\nabla\cdot F)=\nabla\cdot(\partial_t F)∂t​(∇⋅F)=∇⋅(∂t​F)

Interchanging derivatives: $\partial_t(\nabla\cdot F)=\nabla\cdot(\partial_t F)$