Isolated-system quantum fluctuation theorem

Open

QAlgorithms.Papers.Independent.Intakethird100.P15.isolated_fluctuation

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$ .

Writing $r(e)=-e$ , the law $P$ is a Borel probability measure and

r_*P(de)=e^{-\beta e}P(de),\qquad P(\{e\})=e^{\beta e}P(\{-e\})\quad(e\in\mathbb R).

The two measures $P$ and $r_*P$ are mutually absolutely continuous. The point-mass equation includes zero-probability events and uses no probability ratio.

This identifies the exact asymmetry between energy gain and energy loss in the cyclic experiment.

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 pp.3--4, (8), (14), and abstract p.1: isolated fluctuation theorem.
The same initial Hamiltonian is measured at both ends; all multiplicities are kept.
Point-mass identities hold also at zero mass, without dividing by probabilities. -/
theorem isolated_fluctuation [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
    IsProbabilityMeasure P ∧
    reflectedLaw P = P.withDensity (fun e => ENNReal.ofReal (Real.exp (-beta * e))) ∧
    (P ≪ reflectedLaw P) ∧ (reflectedLaw P ≪ P) ∧
    (∀ e : ℝ, (P {e}).toReal = Real.exp (beta * e) * (P {-e}).toReal) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P15

Source

A Quantum Fluctuation Theorem, arXiv:cond-mat/0007360v2, PDF p. 4, Isolated-system quantum fluctuation theorem, abstract and (14)

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_i)_{i\in\iota}$ a Hilbert basis indexed by a countable nonempty type. The given cyclic drive has $T>0$ , $\hbar>0$ , $C\in\mathbb N$ , and spectral data $H_t=(\mu_t,h_t,F_t)$ , with $h_t$ measurable and $F_t:E\to L^2(\mu_t;\mathbb C)$ a complex linear isometric bijection taking every $b_i$ to a real function almost everywhere; the data satisfy $H_{t+T}=H_t$ and $H_{-t}=H_t$ . For each $n$ , its 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 every $x,y\in E$ , and $V_{n,n}\circ\cdots\circ V_{n,0}$ converges on each vector to its supplied evolution $U$ . Let $\varepsilon:\iota\to\mathbb R$ and $\beta>0$ . Assume that $h_0(s)F_0b_i(s)=\varepsilon_iF_0b_i(s)$ for $\mu_0$ -almost every $s$ , for every $i$ , and that $(e^{-t\varepsilon_i})_{i\in\iota}$ is summable for every $t>0$ . Put $Z(t)=\sum_i e^{-t\varepsilon_i}$ and

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

Then $P$ is a probability measure,

\check P=e^{-\beta e}P,\qquad P\ll\check P,\qquad \check P\ll P,\qquad \forall e\in\mathbb R,\quad P(\{e\})=e^{\beta e}P(\{-e\}).

Here the density equality means $\check P(A)=\int_A e^{-\beta e}\,dP(e)$ ; singleton masses are read as real numbers. The cycle count may be $0$ .

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