Quantum Jarzynski work identity

Proved

QAlgorithms.Papers.Independent.Intakethird100.P15.jarzynski_identity

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $\mathcal H$ be a nonzero complex Hilbert space with a nonempty finite or countable complete orthonormal basis real in a fixed conjugation. The self-adjoint Hamiltonian $H(t)$ is real in that conjugation, periodic with period $t_0>0$ , and satisfies $H(-t)=H(t)$ . Start at this symmetry origin and observe an integer number of full cycles. Let $U$ be the well-defined unitary strong limit of the chronological infinitesimal slice products, with each slice equal to $\exp(+i\tau H/\hbar)$ and $\hbar>0$ .

Let $\varepsilon_a$ be the eigenvalues of $H(0)$ in the chosen complete real energy eigenbasis, retaining multiplicities. Assume $Z(t)=\sum_a e^{-t\varepsilon_a}<\infty$ for every $t>0$ , and fix $\beta>0$ . Prepare eigenstate $a$ with probability $e^{-\beta\varepsilon_a}/Z(\beta)$ , evolve by $U$ , and measure the same $H(0)$ . Thus the work $e$ is final minus initial energy. Its atomic law is

P=\sum_{a,g}\frac{e^{-\beta\varepsilon_a}}{Z(\beta)}|\langle g|U|a\rangle|^2\,\delta_{\varepsilon_g-\varepsilon_a}.

Here $\delta_x$ is the unit point mass at $x$ .

The exponential work moment is integrable and satisfies

\mathbb E_P[e^{-\beta e}]=\int_{\mathbb R}e^{-\beta e}\,P(de)=1.

The nonnegative Lebesgue integral also equals $1$ ; the average includes both the canonical initial choice and the final Born outcome.

This is the cyclic work identity, with zero free-energy difference because the same Hamiltonian is measured twice.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P15

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P15

open MeasureTheory Filter

open QAlgorithms.Papers.Independent.Information100.P37 (transition)

open QAlgorithms.Papers.Independent.Support21.P03 (reflectedLaw)

open QAlgorithms.Papers.Independent.Next46.P01 (extendedExpectation)

open scoped ENNReal Topology

universe u v w

variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]

variable {ι : Type v} {Ω : Type w} [MeasurableSpace Ω]

/-- Kurchan, PDF p.4, (15): quantum Jarzynski identity, including finiteness of the
nonnegative moment. This averages both Gibbs preparation and the Born outcome;
there is no free-energy difference since the measured Hamiltonian is unchanged. -/
theorem jarzynski_identity [Countable ι] [Nonempty ι]
    (b : HilbertBasis ι ℂ E) (d : CyclicDrive (Ω := Ω) b)
    (energy : ι → ℝ) (beta : ℝ) (hbeta : 0 < beta)
    (henergy : IsInitialEnergyBasis b d energy) (hheat : HasFiniteHeatTraces energy) :
    let P := workLaw b d.evolution energy beta
    Integrable (fun e : ℝ => Real.exp (-beta * e)) P ∧
    (∫ e, Real.exp (-beta * e) ∂P) = 1 ∧
    (∫⁻ e, ENNReal.ofReal (Real.exp (-beta * e)) ∂P) = 1 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P15

Source

A Quantum Fluctuation Theorem, arXiv:cond-mat/0007360v2, PDF p. 4, Quantum Jarzynski work identity, (15)

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $E$ be a complex Hilbert space, $\Omega$ a measurable space, and $b=(b_i)_{i\in\iota}$ a Hilbert basis with $\iota$ countable and nonempty. The cyclic drive has $T>0$ , $\hbar>0$ , $C\in\mathbb N$ , and spectral data $H_t=(\mu_t,h_t,F_t)$ , with measurable real $h_t$ , complex linear isometric bijections $F_t:E\to L^2(\mu_t;\mathbb C)$ , and every $F_tb_i$ real almost everywhere; these data satisfy $H_{t+T}=H_t$ and $H_{-t}=H_t$ . Its slice isometries $V_{n,r}$ , $0\le r\le n$ , satisfy

\langle x,V_{n,r}y\rangle = \int \overline{F_{t_{n,r}}x(s)} e^{\,i(\Delta_n/\hbar)h_{t_{n,r}}(s)} F_{t_{n,r}}y(s)\,d\mu_{t_{n,r}}(s), \quad \Delta_n=\frac{CT}{n+1},\quad t_{n,r}=(r+\tfrac12)\Delta_n,

for all $x,y$ , and their chronological products converge on each vector to the supplied evolution $U$ . For $\varepsilon:\iota\to\mathbb R$ and $\beta>0$ , assume $h_0F_0b_i=\varepsilon_iF_0b_i$ almost everywhere for every $i$ , and summability of $(e^{-t\varepsilon_i})_i$ for every $t>0$ . Set

Z(t)=\sum_i e^{-t\varepsilon_i}, \qquad P=\sum_{i,j} \frac{e^{-\beta\varepsilon_i}}{Z(\beta)} |\langle b_j,U b_i\rangle|^2\,\delta_{\varepsilon_j-\varepsilon_i}.

Then $e\mapsto e^{-\beta e}$ is integrable with respect to $P$ , and both its real integral and its nonnegative extended integral equal $1$ :

\int_{\mathbb R}e^{-\beta e}\,dP(e)=1, \qquad \int_{\mathbb R}^{-}\operatorname{ofReal}(e^{-\beta e})\,dP(e)=1.

Here $\operatorname{ofReal}(r)=\max(r,0)$ , viewed in $[0,\infty]$ , and $C=0$ is included.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph