Bounded motion: $\langle dG/dt\rangle_\tau\to0$

Proved

VirialTheorem.timeAverage_virialG_deriv_tendsto_zero

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$ . Suppose for all times that $\dot r_k=v_k$ and $\dot p_k=F_k$ with continuous forces, and that 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

\lim_{\tau\to\infty}\left\langle\frac{dG}{dt}\right\rangle_\tau=0 .

Preamble

import Mathlib
import Definitions.Def_virial_theorem_defs

open Filter Topology

Formal statement

namespace VirialTheorem

theorem timeAverage_virialG_deriv_tendsto_zero {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 τ => timeAverage (deriv (virialG m r v)) τ) atTop (𝓝 0) := by sorry

end VirialTheorem

Source

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

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$ , functions $r_k,v_k,F_k:\mathbb R\to\mathbb R^3$ . Assume for all $k$ and all $t\in\mathbb R$ that $r_k$ has derivative $v_k(t)$ and $s\mapsto m_kv_k(s)$ has derivative $F_k(t)$ at $t$ ; that each $F_k$ is continuous; and that there is a real $C$ such that $\|r_k(t)\|\le C$ and $\|v_k(t)\|\le C$ for all $k$ and all $t\ge0$ (nothing is assumed for $t<0$ ). Then $\tau\mapsto\tau^{-1}\int_0^\tau\dot G(t)\,dt$ tends to $0$ as $\tau\to+\infty$ , where $\dot G$ is the derivative function of $G(t)=\sum_k\langle m_kv_k(t),r_k(t)\rangle$ .

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

Bounded motion: ⟨dG/dt⟩τ→0\langle dG/dt\rangle_\tau\to0⟨dG/dt⟩τ​→0

Bounded motion: $\langle dG/dt\rangle_\tau\to0$