$dG/dt = 2T + \sum_k F_k\cdot r_k$

Proved

VirialTheorem.virialG_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 $F_k(t)$ be the net force on particle $k$ , i.e. $F_k=\frac{dp_k}{dt}$ . If at time $t$ each $r_k$ has derivative $v_k(t)$ and each momentum $p_k=m_kv_k$ has derivative $F_k(t)$ , then $G=\sum_k p_k\cdot r_k$ is differentiable at $t$ and

\frac{dG}{dt}(t)=2T(t)+\sum_{k=1}^N F_k(t)\cdot r_k(t),\qquad T=\tfrac12\sum_k m_k\|v_k\|^2 .

Preamble

import Mathlib
import Definitions.Def_virial_theorem_defs

open Filter Topology

Formal statement

namespace VirialTheorem

theorem virialG_hasDerivAt {N : ℕ} (m : Fin N → ℝ) (r v F : Fin N → ℝ → Space) (t : ℝ)
    (hr : ∀ k, HasDerivAt (r k) (v k t) t)
    (hp : ∀ k, HasDerivAt (fun s => m k • v k s) (F k t) t) :
    HasDerivAt (virialG m r v) (2 * kineticEnergy m v t + ∑ k, inner ℝ (F k t) (r k 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 dG/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\ge0$ , masses $m_k\in\mathbb R$ (arbitrary sign), functions $r_k,v_k,F_k:\mathbb R\to\mathbb R^3$ , and a time $t$ . Assume, at the single time $t$ and for every $k$ : $r_k$ has derivative $v_k(t)$ at $t$ , and the function $s\mapsto m_k v_k(s)$ has derivative $F_k(t)$ at $t$ . Then $G(s)=\sum_k\langle m_kv_k(s),r_k(s)\rangle$ has derivative at $t$ equal to

2\,T(t)+\sum_k\langle F_k(t),\,r_k(t)\rangle,\qquad T(t)=\tfrac12\sum_k m_k\|v_k(t)\|^2 .

$F$ is an arbitrary function tied to the motion only through the second hypothesis; if $m_k=0$ that hypothesis forces $F_k(t)=0$ and says nothing about $v_k$ .

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

dG/dt=2T+∑kFk⋅rkdG/dt = 2T + \sum_k F_k\cdot r_kdG/dt=2T+∑k​Fk​⋅rk​

$dG/dt = 2T + \sum_k F_k\cdot r_k$