Virial theorem: $2\langle T\rangle_\tau+\sum_k\langle F_k\cdot r_k\rangle_\tau\to0$ for bounded motion

Proved

VirialTheorem.virial_theorem

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$ , so that $\dot r_k=v_k$ and $\dot p_k=F_k$ for all $t$ , with each $F_k$ continuous. Suppose the motion is bounded: there is a constant $C$ with $\|r_k(t)\|\le C$ and $\|v_k(t)\|\le C$ for all $k$ and all $t\ge0$ . Then, with $T=\frac12\sum_km_k\|v_k\|^2$ and $\langle f\rangle_\tau=\frac1\tau\int_0^\tau f\,dt$ ,

\lim_{\tau\to\infty}\Big(2\langle T\rangle_\tau+\sum_{k=1}^N\langle F_k\cdot r_k\rangle_\tau\Big)=0,

i.e. in the long-time limit $\langle T\rangle=-\frac12\sum_k\langle F_k\cdot r_k\rangle$ .

This is the virial theorem of classical mechanics, relating the time-averaged kinetic energy of a stably bound system to the time-averaged virial of the forces.

Formalization Note The theorem is stated as a limit of the difference, since for a bounded motion the individual averages need not converge. Continuity of the forces is the standing smoothness convention.

Preamble

import Mathlib
import Definitions.Def_virial_theorem_defs

open Filter Topology

Formal statement

namespace VirialTheorem

theorem virial_theorem {N : ℕ} (m : Fin N → ℝ) (r v F : Fin N → ℝ → Space)
    (hr : ∀ k t, HasDerivAt (r k) (v k t) t)
    (hp : ∀ k t, HasDerivAt (fun s => m k • v k s) (F k t) t)
    (hF : ∀ k, Continuous (F k))
    (hbdd : ∃ C : ℝ, ∀ t ≥ 0, ∀ k, ‖r k t‖ ≤ C ∧ ‖v k t‖ ≤ C) :
    Tendsto (fun τ => 2 * timeAverage (kineticEnergy m v) τ +
        ∑ k, timeAverage (fun t => inner ℝ (F k t) (r k t)) τ) atTop (𝓝 0) := by sorry

end VirialTheorem

Source

Wikipedia, "Virial theorem" (article supplied as Virial_theorem.pdf), https://en.wikipedia.org/wiki/Virial_theorem, introduction and section 'Time averaging' (virial theorem)

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$ (any sign), and functions $r_k,v_k,F_k:\mathbb R\to\mathbb R^3$ . Assume: for every $k$ and every $t\in\mathbb R$ , $r_k$ has derivative $v_k(t)$ at $t$ and $s\mapsto m_kv_k(s)$ has derivative $F_k(t)$ at $t$ ; each $F_k$ is continuous on $\mathbb R$ ; and there is a real $C$ such that $\|r_k(t)\|\le C$ and $\|v_k(t)\|\le C$ for every $k$ and every $t\ge0$ . Then, as $\tau\to+\infty$ ,

2\,\tau^{-1}\!\int_0^\tau T(t)\,dt+\sum_k\tau^{-1}\!\int_0^\tau\langle F_k(t),r_k(t)\rangle\,dt\;\longrightarrow\;0,

with $T(t)=\frac12\sum_km_k\|v_k(t)\|^2$ . The forces $F_k$ are arbitrary continuous functions linked to the motion only through $\frac{d}{dt}(m_kv_k)=F_k$ ; no pair structure, potential, or Newton's third law is assumed.

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

Virial theorem: 2⟨T⟩τ+∑k⟨Fk⋅rk⟩τ→02\langle T\rangle_\tau+\sum_k\langle F_k\cdot r_k\rangle_\tau\to02⟨T⟩τ​+∑k​⟨Fk​⋅rk​⟩τ​→0 for bounded motion

Virial theorem: $2\langle T\rangle_\tau+\sum_k\langle F_k\cdot r_k\rangle_\tau\to0$ for bounded motion