Cartesian vector calculus on $\mathbb R^3$ (Clausius–Duhem mission)

Definition

ClausiusDuhem_field_calculus

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

continuum-mechanicsmathematical-physicsthermodynamics

Vector calculus on physical space $\mathbb R^3$ in Cartesian coordinates $x=(x_0,x_1,x_2)$ .

Partial derivative of a scalar field $f$ : $\partial f/\partial x_j(x)$ , the Fréchet derivative of $f$ at $x$ applied to the unit vector $e_j$ .
Gradient $\nabla f = (\partial f/\partial x_0, \partial f/\partial x_1, \partial f/\partial x_2)$ ; divergence $\nabla\cdot F = \sum_j \partial F_j/\partial x_j$ ; dot product $u\cdot w=\sum_i u_i w_i$ .
Velocity gradient $(\nabla \mathbf v)_{ij} = \partial v_i/\partial x_j$ and double contraction $A:B=\sum_{i,j}A_{ij}B_{ij}$ .
Partial time derivative $\partial\varphi/\partial t$ and material time derivative

\dot\varphi = \frac{\partial\varphi}{\partial t} + \nabla\varphi\cdot\mathbf v.

Outward flux through the boundary of the box $\Omega=[a,b]=\prod_i[a_i,b_i]$ :

\int_{\partial\Omega}F\cdot\mathbf n\,dA=\sum_{i}\Big(\int_{\{x_i=b_i\}}F_i\,dA-\int_{\{x_i=a_i\}}F_i\,dA\Big).

These are the operators in which every statement of the mission is written.

Formalization Note Space is Fin 3 → ℝ. Derivatives are Fréchet derivatives (Mathlib fderiv, deriv), which return $0$ at points of non-differentiability; all theorems of the mission assume enough differentiability that this convention is never used. Each box face is parametrized by the two remaining coordinates and carries two-dimensional Lebesgue measure.

Definition code

import Mathlib

/-!
Vector calculus on Euclidean 3-space `ℝ³ = Fin 3 → ℝ`, in Cartesian coordinates,
as used in the Wikipedia article "Clausius–Duhem inequality" (oldid=1182390552).
-/

namespace ClausiusDuhem

/-- Physical space `ℝ³`, with Cartesian coordinates `x 0, x 1, x 2`. -/
abbrev Space := Fin 3 → ℝ

/-- The partial derivative `∂f/∂x_j` of a scalar field `f` at the point `x`. -/
noncomputable def partialDeriv (f : Space → ℝ) (j : Fin 3) (x : Space) : ℝ :=
  fderiv ℝ f x (Pi.single j (1 : ℝ))

/-- The gradient `∇f(x) = (∂f/∂x_0, ∂f/∂x_1, ∂f/∂x_2)` of a scalar field. -/
noncomputable def grad (f : Space → ℝ) (x : Space) : Fin 3 → ℝ :=
  fun j => partialDeriv f j x

/-- The divergence `∇ · F(x) = ∑_j ∂F_j/∂x_j` of a vector field `F`. -/
noncomputable def div (F : Space → Fin 3 → ℝ) (x : Space) : ℝ :=
  ∑ j : Fin 3, partialDeriv (fun y => F y j) j x

/-- The Euclidean dot product `u · w = ∑_i u_i w_i`. -/
def dot (u w : Fin 3 → ℝ) : ℝ :=
  ∑ i : Fin 3, u i * w i

/-- The velocity gradient `(∇v)_{ij} = ∂v_i/∂x_j` of a vector field `v`. -/
noncomputable def velocityGradient (v : Space → Fin 3 → ℝ) (x : Space) :
    Matrix (Fin 3) (Fin 3) ℝ :=
  fun i j => partialDeriv (fun y => v y i) j x

/-- The double contraction `A : B = ∑_{i,j} A_{ij} B_{ij}` of two second-order tensors. -/
def doubleDot (A B : Matrix (Fin 3) (Fin 3) ℝ) : ℝ :=
  ∑ i : Fin 3, ∑ j : Fin 3, A i j * B i j

/-- The partial time derivative `∂φ/∂t (t, x)` of a time-dependent scalar field. -/
noncomputable def timeDeriv (φ : ℝ → Space → ℝ) (t : ℝ) (x : Space) : ℝ :=
  deriv (fun τ => φ τ x) t

/-- The material time derivative `φ̇ = ∂φ/∂t + ∇φ · v` of a scalar field `φ`
following the velocity field `v`. -/
noncomputable def materialDeriv (φ : ℝ → Space → ℝ) (v : ℝ → Space → Fin 3 → ℝ)
    (t : ℝ) (x : Space) : ℝ :=
  timeDeriv φ t x + dot (grad (φ t) x) (v t x)

/-- The outward flux `∫_{∂Ω} F · n dA` of a vector field `F` through the boundary of the
closed rectangular box `Ω = [a, b] = ∏_i [a_i, b_i]`.  The face `x_i = b_i` has outward
normal `e_i` and the face `x_i = a_i` has outward normal `-e_i`; each face is parametrised by
the two remaining coordinates and carries two-dimensional Lebesgue (area) measure. -/
noncomputable def boxOutwardFlux (F : Space → Fin 3 → ℝ) (a b : Space) : ℝ :=
  ∑ i : Fin 3,
    ((∫ y in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), F (i.insertNth (b i) y) i) -
      ∫ y in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), F (i.insertNth (a i) y) i)

end ClausiusDuhem

Source

Wikipedia, "Clausius–Duhem inequality", revision oldid=1182390552, https://en.wikipedia.org/w/index.php?title=Clausius%E2%80%93Duhem_inequality&oldid=1182390552, sections "Clausius–Duhem inequality in terms of the specific entropy" (integral form, proof) and "Clausius–Duhem inequality in terms of specific internal energy" (index notation).

Read-back

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

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the source article and of the intended meaning. It was not produced by a blind, independent auditor, so it must not be mistaken for independent testimony; reviewers should compare it against the Lean code themselves.

This file introduces, inside the namespace ClausiusDuhem, the following objects, where space means the set of functions $\{0,1,2\}\to\mathbb R$ (i.e. $\mathbb R^3$ with its product structure).

Partial derivative. For $f:\mathbb R^3\to\mathbb R$ , $j\in\{0,1,2\}$ and $x\in\mathbb R^3$ : $\partial_j f(x) := Df(x)[e_j]$ , the Fréchet derivative of $f$ at $x$ evaluated on the $j$ -th standard basis vector. If $f$ is not differentiable at $x$ , the Fréchet derivative is by convention the zero map, so $\partial_j f(x)=0$ .
Gradient. $\nabla f(x) := (\partial_0 f(x),\partial_1 f(x),\partial_2 f(x))$ .
Divergence. For $F:\mathbb R^3\to\mathbb R^3$ : $\nabla\cdot F(x) := \sum_{j=0}^{2}\partial_j F_j(x)$ , where $F_j$ is the $j$ -th component function.
Dot product. $u\cdot w := \sum_{i=0}^2 u_i w_i$ .
Velocity gradient. For $v:\mathbb R^3\to\mathbb R^3$ : the $3\times3$ real matrix $(\nabla v(x))_{ij} := \partial_j v_i(x)$ .
Double contraction. For $3\times3$ real matrices: $A:B := \sum_{i}\sum_{j}A_{ij}B_{ij}$ .
Time derivative. For $\varphi:\mathbb R\times\mathbb R^3\to\mathbb R$ (curried as $\varphi(t)(x)$ ): $\partial_t\varphi(t,x) := \frac{d}{d\tau}\varphi(\tau,x)\big|_{\tau=t}$ , the one-variable derivative; it is $0$ if $\tau\mapsto\varphi(\tau,x)$ is not differentiable at $t$ .
Material derivative. For $\varphi$ as above and $v:\mathbb R\times\mathbb R^3\to\mathbb R^3$ :

\dot\varphi(t,x) := \partial_t\varphi(t,x) + \nabla\big(\varphi(t,\cdot)\big)(x)\cdot v(t,x).

Box outward flux. For $F:\mathbb R^3\to\mathbb R^3$ and $a,b\in\mathbb R^3$ :

\Phi_{[a,b]}(F) := \sum_{i=0}^{2}\left(\int_{R_i}F_i\big(\iota_i(b_i,y)\big)\,dy - \int_{R_i}F_i\big(\iota_i(a_i,y)\big)\,dy\right),

where $R_i\subset\mathbb R^2$ is the closed rectangle $\prod_{k\ne i}[a_k,b_k]$ (coordinates other than $i$ , in increasing order), $\iota_i(c,y)\in\mathbb R^3$ is the point whose $i$ -th coordinate is $c$ and whose other two coordinates are $y$ , and $dy$ is two-dimensional Lebesgue measure. The integrals are Bochner integrals, equal to $0$ when the integrand is not integrable. No condition $a\le b$ is imposed by the definition itself (if $a_k>b_k$ for some $k\ne i$ , $R_i$ is empty).

View graph

Cartesian vector calculus on R3\mathbb R^3R3 (Clausius–Duhem mission)

Cartesian vector calculus on $\mathbb R^3$ (Clausius–Duhem mission)