Thermostated finite-time fluctuation relation for bath energy plus system observable

Open

QAlgorithms.Papers.Independent.Intakethird100.P15.bath_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$ .

Use a complete real product eigenbasis $|a\rangle_B\otimes|s\rangle_S$ , with nonempty finite or countable labels on each tensor factor. Let bath energies be $\epsilon_a^B$ and system observable eigenvalues $o_s$ , with $O$ bounded below. Fix $\beta>0$ , positive finite normalizers $Z_B=\sum_a e^{-\beta\epsilon_a^B}$ and $Z_O=\sum_s e^{-\beta o_s}$ , and require for every $0<\mu<1$ that

\sum_a e^{-2\beta\mu\epsilon_a^B}<\infty,\qquad\sum_s p_s^{2\mu}<\infty,\quad p_s=\frac{e^{-\beta o_s}}{Z_O}.

Prepare the uncorrelated product weights $e^{-\beta\epsilon_a^B}p_s/Z_B$ . The drive acts on the joint Hilbert space and may include interactions. Measure $D=H_B\otimes I+I\otimes O$ at both ends, so its eigenvalue at $(a,s)$ is $d_{a,s}=\epsilon_a^B+o_s$ . Let $P_D$ be the Born law with these initial weights and work $d_{g,r}-d_{a,s}$ . Then, for $r(e)=-e$ ,

r_*P_D(de)=e^{-\beta e}P_D(de),\qquad P_D(\{e\})=e^{\beta e}P_D(\{-e\}).

The law is a probability measure and is equivalent to its reflection. The exact measured change includes both bath energy and system $O$ , and need not equal the change of the interacting Hamiltonian or bath heat alone.

This is the finite-time thermostated result; no normalized infinite-bath Gibbs state or large-time limit is asserted.

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.5--6, (22)--(26): finite-time thermostated fluctuation relation.
The basis indexed by B x S is the tensor-product eigenbasis, so the bath and system
observables commute and D has their sum spectrum. The total driven Hamiltonian may
interact and is not assumed equal to D. A finite bath may have infinite-dimensional
Hilbert space. Every 0 < mu < 1 is included in (26); no large-bath/time limit is taken. -/
theorem bath_fluctuation {B S : Type*} [Countable B] [Nonempty B]
    [Countable S] [Nonempty S]
    (b : HilbertBasis (B × S) ℂ E) (d : CyclicDrive (Ω := Ω) b)
    (bathEnergy : B → ℝ) (systemO : S → ℝ) (beta : ℝ) (hbeta : 0 < beta)
    (hO_lower : ∃ L : ℝ, ∀ s, L ≤ systemO s)
    (hZbath : 0 < heatTrace bathEnergy beta)
    (hZsystem : 0 < heatTrace systemO beta)
    (hbath_beta : Summable (fun a => Real.exp (-beta * bathEnergy a)))
    (hsystem_beta : Summable (fun a => Real.exp (-beta * systemO a)))
    (hbath_strip : ∀ mu : ℝ, 0 < mu → mu < 1 →
      Summable (fun a => Real.exp (-(2 * beta * mu) * bathEnergy a)))
    (hpower : ∀ mu : ℝ, 0 < mu → mu < 1 →
      Summable (fun a => (spectralGibbsWeight systemO beta a) ^ (2 * mu))) :
    let P := preparedWorkLaw b d.evolution (bathObservedEnergy bathEnergy systemO)
      (bathPreparation bathEnergy systemO 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. 6, Thermostated finite-time fluctuation relation for D=H_bath+O, (23)–(26)

Read-back

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

Let $B,S$ be countable nonempty types, $E$ a complex Hilbert space, $\Omega$ a measurable space, and $(b_{a,s})_{(a,s)\in B\times S}$ a Hilbert basis. The cyclic drive has $T>0$ , $\hbar>0$ , $C\in\mathbb N$ , and spectral data $H_t=(\mu_t,h_t,F_t)$ , where $h_t:\Omega\to\mathbb R$ is measurable and $F_t:E\to L^2(\mu_t;\mathbb C)$ is a complex linear isometric bijection taking each basis vector to a real function almost everywhere; the data satisfy $H_{t+T}=H_t$ and $H_{-t}=H_t$ . Its slice isometries $V_{n,r}$ , $0\le r\le n$ , satisfy, for every $x,y\in E$ ,

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

and their chronological products converge on each vector to the supplied evolution $U$ . Let $E_B:B\to\mathbb R$ , $O:S\to\mathbb R$ , and $\beta>0$ . Assume there is $L\in\mathbb R$ with $L\le O(s)$ for every $s$ ; that

Z_B=\sum_a e^{-\beta E_B(a)}>0, \qquad Z_S=\sum_s e^{-\beta O(s)}>0;

that both families defining these sums are summable; and that for every real $0<\mu<1$ , both

\left(e^{-2\beta\mu E_B(a)}\right)_{a\in B} \quad\text{and}\quad \left(\left(\frac{e^{-\beta O(s)}}{Z_S}\right)^{2\mu}\right)_{s\in S}

are summable, with the second expression using real powers. For $p=(a,s)$ , define $\varepsilon_p=E_B(a)+O(s)$ and $w_p=e^{-\beta E_B(a)}e^{-\beta O(s)}/(Z_BZ_S)$ , and put

P=\sum_{p,q\in B\times S} w_p|\langle b_q,U b_p\rangle|^2\,\delta_{\varepsilon_q-\varepsilon_p}, \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\}).

The density equality means $\check P(A)=\int_A e^{-\beta e}\,dP(e)$ , and singleton masses are interpreted as real numbers. The cycle count $C=0$ is permitted.

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