Prove2Me

Derivative of the time correlation ⟨ξi(t)xk⟩\langle\xi_i(t)x_k\rangle

Proved
OnsagerReciprocal.timeCorrelation_hasDerivAt

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 and λ\lambda a real n×nn\times n matrix, with γ=λβ−1\gamma=\lambda\beta^{-1}. Average over the Gaussian fluctuation distribution w(x)∝exp⁡(−12βikxixk)w(x)\propto\exp(-\tfrac12\beta_{ik}x_ix_k), and let ξ(t;x)=e−tλx\xi(t;x)=e^{-t\lambda}x, Ξ(t;x)=β ξ(t;x)\Xi(t;x)=\beta\,\xi(t;x). Then for all indices i,ki,k and all t∈Rt\in\mathbb R, the time correlation Cik(t)=⟨ξi(t;x) xk⟩C_{ik}(t)=\langle\xi_i(t;x)\,x_k\rangle is differentiable at tt and

ddt⟨ξi(t) xk⟩=−γil ⟨Ξl(t) xk⟩.\frac{d}{dt}\big\langle\xi_i(t)\,x_k\big\rangle=-\gamma_{il}\,\big\langle\Xi_l(t)\,x_k\big\rangle .

This is the "differentiate and substitute" step of the proof of Onsager's principle.

Preamble
import Mathlib
import Definitions.Def_OnsagerReciprocal_basic

open Matrix
Formal statement
namespace OnsagerReciprocal
theorem timeCorrelation_hasDerivAt {n : ℕ} (β lam : Matrix (Fin n) (Fin n) ℝ)
    (hβ : β.PosDef) (i k : Fin n) (t : ℝ) :
    HasDerivAt (fun s => timeCorrelation β lam s i k)
      (-∑ l : Fin n, kineticCoeff β lam i l *
        fluctuationAverage β (fun x => meanConjugate β lam t x l * x k)) 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, every real n×nn\times n matrix λ\lambda, all indices i,k∈{1,…,n}i,k\in\{1,\dots,n\} and every real tt: the real function

s↦Cik(s)=∫Rn(e−sλx)i xk wβ(x) dx∫Rnwβ(x) dx,wβ(x)=e−12xTβx,s\mapsto C_{ik}(s)=\frac{\int_{\mathbb R^n}\big(e^{-s\lambda}x\big)_i\,x_k\,w_\beta(x)\,dx}{\int_{\mathbb R^n}w_\beta(x)\,dx},\qquad w_\beta(x)=e^{-\frac12x^{\mathsf T}\beta x},

is differentiable at tt, with derivative

Cik′(t)=−∑l=1nγil ∫Rn(βe−tλx)l xk wβ(x) dx∫Rnwβ(x) dx,γ=λβ−1.C_{ik}'(t)=-\sum_{l=1}^n\gamma_{il}\,\frac{\int_{\mathbb R^n}\big(\beta e^{-t\lambda}x\big)_l\,x_k\,w_\beta(x)\,dx}{\int_{\mathbb R^n}w_\beta(x)\,dx},\qquad \gamma=\lambda\beta^{-1}.

(Integrals are Lebesgue integrals; the formal averages would be 00 for non-integrable integrands, but no such case is excluded or singled out by the statement.)

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