$\langle X_i x_k\rangle=\delta_{ik}$

Proved

OnsagerReciprocal.conjugate_fluctuation_average

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

mathematical-physicsonsagerthermodynamics

Let $\beta$ be a positive definite real symmetric $n\times n$ matrix, and let the fluctuations $x\in\mathbb R^n$ be distributed with the Gaussian density $w(x)=\tilde A\exp(-\tfrac12\beta_{ik}x_ix_k)$ , where $\tilde A$ normalizes $w$ . With the conjugate quantities $X_i=\beta_{ik}x_k$ , for all indices $i,k$ ,

\langle X_i\,x_k\rangle=\delta_{ik}.

Equivalently, the covariance matrix of the fluctuations is $\beta^{-1}$ . This identity is used at the last step of the proof of Onsager's principle.

Preamble

import Mathlib
import Definitions.Def_OnsagerReciprocal_basic

open Matrix

Formal statement

namespace OnsagerReciprocal
theorem conjugate_fluctuation_average {n : ℕ} (β : Matrix (Fin n) (Fin n) ℝ)
    (hβ : β.PosDef) (i k : Fin n) :
    fluctuationAverage β (fun x => conjugate β x i * x k) = if i = k then 1 else 0 := 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\in\mathbb N$ , every positive definite real $n\times n$ matrix $\beta$ (symmetric, $v^{\mathsf T}\beta v>0$ for $v\ne0$ ) and all indices $i,k\in\{1,\dots,n\}$ :

\frac{\int_{\mathbb R^n}(\beta x)_i\,x_k\,e^{-\frac12x^{\mathsf T}\beta x}\,dx}{\int_{\mathbb R^n}e^{-\frac12x^{\mathsf T}\beta x}\,dx}=\begin{cases}1,& i=k,\\0,& i\neq k,\end{cases}

integrals with respect to Lebesgue measure on $\mathbb R^n$ . No time dependence or matrix $\lambda$ is involved. For $n=0$ there are no indices and the statement is empty.

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

⟨Xixk⟩=δik\langle X_i x_k\rangle=\delta_{ik}⟨Xi​xk​⟩=δik​

$\langle X_i x_k\rangle=\delta_{ik}$