$\nabla\cdot(\varphi\mathbf v)=\varphi\,\nabla\cdot\mathbf v+\mathbf v\cdot\nabla\varphi$

Proved

ClausiusDuhem.div_smul_eq

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

continuum-mechanicsmathematical-physicsthermodynamics

Let $\varphi:\mathbb R^3\to\mathbb R$ and $\mathbf v:\mathbb R^3\to\mathbb R^3$ be differentiable at the point $x$ . Then

\nabla\cdot(\varphi\,\mathbf v)(x)=\varphi(x)\,\nabla\cdot\mathbf v(x)+\mathbf v(x)\cdot\nabla\varphi(x).

This product rule converts the divergence of $\mathbf q/T$ and of $\rho\eta\mathbf v$ into the terms appearing in the differential forms of the Clausius–Duhem inequality.

Preamble

import Definitions.Def_ClausiusDuhem_thermo_process

Formal statement

namespace ClausiusDuhem
theorem div_smul_eq (φ : Space → ℝ) (v : Space → Fin 3 → ℝ) (x : Space)
    (hφ : DifferentiableAt ℝ φ x) (hv : DifferentiableAt ℝ v x) :
    div (fun y => φ y • v y) x = φ x * div v x + dot (v x) (grad φ x) := by sorry
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, section "Clausius–Duhem inequality in terms of specific internal energy", Proof, first line (the identity used).

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.

For every function $\varphi:\mathbb R^3\to\mathbb R$ , every function $v:\mathbb R^3\to\mathbb R^3$ and every point $x\in\mathbb R^3$ such that $\varphi$ is (Fréchet) differentiable at $x$ and $v$ is differentiable at $x$ :

\nabla\cdot\big(y\mapsto\varphi(y)\,v(y)\big)(x)=\varphi(x)\,(\nabla\cdot v)(x)+v(x)\cdot\nabla\varphi(x),

where $\nabla\cdot F(x)=\sum_{j=0}^2\partial_jF_j(x)$ , $\nabla\varphi(x)=(\partial_0\varphi(x),\partial_1\varphi(x),\partial_2\varphi(x))$ , $\partial_j$ is the Fréchet derivative applied to the $j$ -th standard basis vector, and $u\cdot w=\sum_i u_iw_i$ . Only differentiability at the single point $x$ is assumed.

View graph

∇⋅(φv)=φ ∇⋅v+v⋅∇φ\nabla\cdot(\varphi\mathbf v)=\varphi\,\nabla\cdot\mathbf v+\mathbf v\cdot\nabla\varphi∇⋅(φv)=φ∇⋅v+v⋅∇φ

$\nabla\cdot(\varphi\mathbf v)=\varphi\,\nabla\cdot\mathbf v+\mathbf v\cdot\nabla\varphi$