Prove2Me

Mean values relax as ξ˙=−γ Ξ\dot\xi=-\gamma\,\Xi

Proved
OnsagerReciprocal.meanFluctuation_dynamics

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsonsagerthermodynamics

Let β\beta be a positive definite real symmetric n×nn\times n matrix, λ\lambda a real n×nn\times n matrix, γ=λβ−1\gamma=\lambda\beta^{-1}, and x0∈Rnx_0\in\mathbb R^n. Let ξ(t)=e−tλx0\xi(t)=e^{-t\lambda}x_0 be the mean value at time tt of the fluctuation that equals x0x_0 at t=0t=0, and Ξ(t)=β ξ(t)\Xi(t)=\beta\,\xi(t). Then

ξ(0)=x0andξ˙i(t)=−γik Ξk(t)for all t∈R.\xi(0)=x_0\qquad\text{and}\qquad \dot\xi_i(t)=-\gamma_{ik}\,\Xi_k(t)\quad\text{for all }t\in\mathbb R .

This expresses the relaxation of mean values in terms of the kinetic coefficients and the conjugate mean values.

Preamble
import Mathlib
import Definitions.Def_OnsagerReciprocal_basic

open Matrix
Formal statement
namespace OnsagerReciprocal
theorem meanFluctuation_dynamics {n : ℕ} (β lam : Matrix (Fin n) (Fin n) ℝ)
    (hβ : β.PosDef) (x₀ : Fin n → ℝ) :
    meanFluctuation lam 0 x₀ = x₀ ∧
      ∀ t : ℝ, HasDerivAt (fun s => meanFluctuation lam s x₀)
        (-(kineticCoeff β lam *ᵥ meanConjugate β lam t x₀)) t := by sorry
end OnsagerReciprocal
Source
Wikipedia, "Onsager reciprocal relations", https://en.wikipedia.org/w/index.php?title=Onsager_reciprocal_relations&oldid=1355014688, section "Abstract formulation" and its "Proof" subsection (pp. 5-6 of the PDF export), following L. D. Landau, E. M. Lifshitz, Statistical Physics, Part 1 (1975)
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, with full knowledge of the source text and of the intended meaning. It was not produced by a blind, independent auditor, so reviewers must not treat it as independent testimony; compare the Lean code against the source yourself.

For every n∈Nn\in\mathbb N, every positive definite real n×nn\times n matrix β\beta (symmetric, vTβv>0v^{\mathsf T}\beta v>0 for v≠0v\neq0), every real n×nn\times n matrix λ\lambda and every x0∈Rnx_0\in\mathbb R^n, both of the following hold, with ξ(t)=exp⁡(−tλ) x0\xi(t)=\exp(-t\lambda)\,x_0 (matrix exponential) and γ=λβ−1\gamma=\lambda\beta^{-1}:

  1. ξ(0)=x0\xi(0)=x_0;
  2. for every real tt (negative values included), the map s↦ξ(s)s\mapsto\xi(s) from R\mathbb R to Rn\mathbb R^n is differentiable at tt with derivative
ξ′(t)=−γ (β ξ(t)).\xi'(t)=-\gamma\,\big(\beta\,\xi(t)\big).
Human review

  • Endorsed by Shuze Chen · Oct 10, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 10, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph