$\nabla(1/T)=-\nabla T/T^2$

Proved

ClausiusDuhem.grad_inv_eq

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

continuum-mechanicsmathematical-physicsthermodynamics

Let $T:\mathbb R^3\to\mathbb R$ be differentiable at $x$ with $T(x)\neq0$ . Then

\nabla\Big(\frac1T\Big)(x)=-\frac{1}{T(x)^2}\,\nabla T(x).

This is the step that turns $\mathbf q\cdot\nabla(1/T)$ into $-\mathbf q\cdot\nabla T/T^2$ in the derivation of the internal-energy form.

Preamble

import Definitions.Def_ClausiusDuhem_thermo_process

Formal statement

namespace ClausiusDuhem
theorem grad_inv_eq (T : Space → ℝ) (x : Space)
    (hT : DifferentiableAt ℝ T x) (hTx : T x ≠ 0) :
    grad (fun y => (T y)⁻¹) x = -(1 / T x ^ 2) • grad T 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 (index-notation computation of the gradient of 1/T).

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 $T:\mathbb R^3\to\mathbb R$ and every point $x$ such that $T$ is differentiable at $x$ and $T(x)\ne0$ :

\nabla\big(y\mapsto T(y)^{-1}\big)(x)=-\frac{1}{T(x)^2}\,\nabla T(x),

an equality of vectors in $\mathbb R^3$ (componentwise: $\partial_j(1/T)(x)=-\partial_jT(x)/T(x)^2$ for $j=0,1,2$ ), where $\partial_j$ is the Fréchet derivative applied to the $j$ -th standard basis vector. Here $T(y)^{-1}$ denotes the real inverse, which is $0$ where $T(y)=0$ ; only $T(x)\ne0$ at the single point $x$ is assumed.

View graph

∇(1/T)=−∇T/T2\nabla(1/T)=-\nabla T/T^2∇(1/T)=−∇T/T2

$\nabla(1/T)=-\nabla T/T^2$