Prove2Me

Exact time-averaged equation ⟨dG/dt⟩τ=2⟨T⟩τ+∑k⟨Fk⋅rk⟩τ\langle dG/dt\rangle_\tau = 2\langle T\rangle_\tau+\sum_k\langle F_k\cdot r_k\rangle_\tau

Proved
VirialTheorem.timeAverage_virialG_deriv

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

classical-mechanicsvirial-theorem

Throughout, NN point particles move in R3\mathbb R^3; particle kk has constant mass mk∈Rm_k\in\mathbb R, position rk(t)r_k(t) and velocity vk(t)v_k(t), and momentum pk=mkvkp_k=m_kv_k. Suppose for all times tt that r˙k=vk\dot r_k=v_k and p˙k=Fk\dot p_k=F_k, with each force FkF_k continuous in time. Then for every duration τ>0\tau>0,

⟨dGdt⟩τ=G(τ)−G(0)τand⟨dGdt⟩τ=2⟨T⟩τ+∑k=1N⟨Fk⋅rk⟩τ,\left\langle\frac{dG}{dt}\right\rangle_\tau=\frac{G(\tau)-G(0)}{\tau}\qquad\text{and}\qquad\left\langle\frac{dG}{dt}\right\rangle_\tau=2\langle T\rangle_\tau+\sum_{k=1}^N\langle F_k\cdot r_k\rangle_\tau,

where ⟨f⟩τ=1τ∫0τf dt\langle f\rangle_\tau=\frac1\tau\int_0^\tau f\,dt.

Formalization Note Continuity of the forces is the standing smoothness convention of classical mechanics; it makes all the averaged quantities integrable.

Preamble
import Mathlib
import Definitions.Def_virial_theorem_defs

open Filter Topology
Formal statement
namespace VirialTheorem

theorem timeAverage_virialG_deriv {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))
    (τ : ℝ) (hτ : 0 < τ) :
    timeAverage (deriv (virialG m r v)) τ = (virialG m r v τ - virialG m r v 0) / τ ∧
    timeAverage (deriv (virialG m r v)) τ =
      2 * timeAverage (kineticEnergy m v) τ +
        ∑ k, timeAverage (fun t => inner ℝ (F k t) (r k t)) τ := by sorry

end VirialTheorem
Source
Wikipedia, "Virial theorem" (article supplied as Virial_theorem.pdf), https://en.wikipedia.org/wiki/Virial_theorem, section 'Time averaging' (exact equation)
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≥0N\ge0, masses mk∈Rm_k\in\mathbb R, functions rk,vk,Fk:R→R3r_k,v_k,F_k:\mathbb R\to\mathbb R^3. Assume for every kk and every time t∈Rt\in\mathbb R: rkr_k has derivative vk(t)v_k(t) at tt, and s↦mkvk(s)s\mapsto m_kv_k(s) has derivative Fk(t)F_k(t) at tt; assume each FkF_k is continuous on R\mathbb R. Let τ>0\tau>0. Writing G˙\dot G for the derivative function of GG (Lean's deriv) and ⟨f⟩τ=τ−1∫0τf\langle f\rangle_\tau=\tau^{-1}\int_0^\tau f, both of the following hold:

⟨G˙⟩τ=G(τ)−G(0)τ,⟨G˙⟩τ=2⟨T⟩τ+∑k⟨t↦⟨Fk(t),rk(t)⟩⟩τ.\langle\dot G\rangle_\tau=\frac{G(\tau)-G(0)}{\tau},\qquad \langle\dot G\rangle_\tau=2\langle T\rangle_\tau+\sum_k\big\langle t\mapsto\langle F_k(t),r_k(t)\rangle\big\rangle_\tau .
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