Virial theorem for power-law forces: $\langle T\rangle_\tau-\tfrac n2\langle V_{\mathrm{TOT}}\rangle_\tau\to0$

Proved

VirialTheorem.virial_theorem_power_law

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 the particles interact only through power-law pair potentials $V_{jk}(s)=\alpha_{jk}s^n$ ( $\alpha_{jk}=\alpha_{kj}$ ): for all $t\ge0$ the momentum $p_k$ has derivative equal to the net pair force at the configuration $r(t)$ , and $\dot r_k=v_k$ for all $t$ . Suppose the motion is collision-free ( $r_j(t)\ne r_k(t)$ for $j\ne k$ , $t\ge0$ ) and bounded ( $\|r_k(t)\|,\|v_k(t)\|\le C$ for $t\ge0$ ). Then

\lim_{\tau\to\infty}\Big(\langle T\rangle_\tau-\frac n2\langle V_{\mathrm{TOT}}\rangle_\tau\Big)=0 .

Formalization Note The limit statement is the precise content of " $\langle T\rangle=\frac n2\langle V_{\mathrm{TOT}}\rangle$ for stably bound systems"; the individual averages need not converge.

Preamble

import Mathlib
import Definitions.Def_virial_theorem_defs

open Filter Topology

Formal statement

namespace VirialTheorem

theorem virial_theorem_power_law {N : ℕ} (m : Fin N → ℝ) (r v : Fin N → ℝ → Space)
    (α : Fin N → Fin N → ℝ) (n : ℝ)
    (hα : ∀ j k, α j k = α k j)
    (hr : ∀ k t, HasDerivAt (r k) (v k t) t)
    (hp : ∀ k, ∀ t ≥ 0, HasDerivAt (fun s => m k • v k s)
      (netPairForce (powerLawPotential α n) (fun i => r i t) k) t)
    (hx : ∀ t ≥ 0, ∀ j k, j ≠ k → r j t ≠ r k t)
    (hbdd : ∃ C : ℝ, ∀ t ≥ 0, ∀ k, ‖r k t‖ ≤ C ∧ ‖v k t‖ ≤ C) :
    Tendsto (fun τ => timeAverage (kineticEnergy m v) τ -
        (n / 2) * timeAverage (fun t => totalPotential (powerLawPotential α n)
          (fun i => r i t)) τ) 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' (power-law forces)

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:\mathbb R\to\mathbb R^3$ , symmetric real coefficients $\alpha_{jk}=\alpha_{kj}$ , and a real exponent $n$ . Assume: for all $k$ and all $t\in\mathbb R$ , $r_k$ has derivative $v_k(t)$ at $t$ ; for all $k$ and all $t\ge0$ , $s\mapsto m_kv_k(s)$ has derivative at $t$ equal to the net pair force for the potentials $V_{jk}(s)=\alpha_{jk}s^n$ at the configuration $r(t)$ (nothing is assumed about the momentum for $t<0$ ); for all $t\ge0$ and $j\ne k$ , $r_j(t)\ne r_k(t)$ ; and there is $C$ with $\|r_k(t)\|\le C$ , $\|v_k(t)\|\le C$ for all $k$ and $t\ge0$ . Then, as $\tau\to+\infty$ ,

\tau^{-1}\!\int_0^\tau T(t)\,dt-\frac n2\,\tau^{-1}\!\int_0^\tau V_{\mathrm{TOT}}(r(t))\,dt\;\longrightarrow\;0,

where $V_{\mathrm{TOT}}(x)=\sum_k\sum_{j<k}\alpha_{jk}\|x_k-x_j\|^n$ .

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 for power-law forces: ⟨T⟩τ−n2⟨VTOT⟩τ→0\langle T\rangle_\tau-\tfrac n2\langle V_{\mathrm{TOT}}\rangle_\tau\to0⟨T⟩τ​−2n​⟨VTOT​⟩τ​→0

Virial theorem for power-law forces: $\langle T\rangle_\tau-\tfrac n2\langle V_{\mathrm{TOT}}\rangle_\tau\to0$