Half the derivative of the moment of inertia is $G$

Proved

VirialTheorem.momentOfInertia_hasDerivAt

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

classical-mechanicsvirial-theorem

Throughout, $N$ point particles move in $\mathbb R^3$ ; particle $k$ has constant mass $m_k\in\mathbb R$ , position $r_k(t)$ and velocity $v_k(t)$ , and momentum $p_k=m_kv_k$ . Let $I(t)=\sum_k m_k\|r_k(t)\|^2$ and $G(t)=\sum_k p_k(t)\cdot r_k(t)$ . If at time $t$ every $r_k$ is differentiable with derivative $v_k(t)$ , then $I$ is differentiable at $t$ and

\frac{dI}{dt}(t)=2\,G(t).

This identifies $G$ as half the rate of change of the moment of inertia, the first step of the derivation of the virial theorem.

Preamble

import Mathlib
import Definitions.Def_virial_theorem_defs

open Filter Topology

Formal statement

namespace VirialTheorem

theorem momentOfInertia_hasDerivAt {N : ℕ} (m : Fin N → ℝ) (r v : Fin N → ℝ → Space) (t : ℝ)
    (hr : ∀ k, HasDerivAt (r k) (v k t) t) :
    HasDerivAt (momentOfInertia m r) (2 * virialG m r v t) t := by sorry

end VirialTheorem

Source

Wikipedia, "Virial theorem" (article supplied as Virial_theorem.pdf), https://en.wikipedia.org/wiki/Virial_theorem, section 'Statement and derivation' (derivation of dI/dt)

Read-back

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

Non-blind read-back. This read-back is not independent testimony. It was written by the same agent that drafted the Lean statements, with full knowledge of the source article and of the intended meaning. Reviewers must not treat it as a blind audit; an independent read-back should still be obtained before relying on it.

Let $N\ge 0$ , let $m_0,\dots,m_{N-1}$ be arbitrary real numbers, let $r_k, v_k:\mathbb R\to\mathbb R^3$ be arbitrary functions for each particle $k$ , and let $t\in\mathbb R$ . Assume that for every $k$ the function $r_k$ has derivative $v_k(t)$ at the point $t$ (only at this single time). Then the function $I(s)=\sum_k m_k\|r_k(s)\|^2$ has a derivative at $t$ equal to

2\,G(t)=2\sum_k\langle m_kv_k(t),\,r_k(t)\rangle .

Nothing is assumed about $v_k$ at other times; masses may be zero or negative; for $N=0$ both sides are $0$ .

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Half the derivative of the moment of inertia is GGG

Half the derivative of the moment of inertia is $G$