Second principle with possibly infinite mean work

Open

QAlgorithms.Papers.Independent.Intakethird100.P15.secondPrinciple_extendedMean

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 negative part $e^-:=\max(-e,0)$ is integrable. Define the signed extended expectation by the positive-part integral minus the negative-part integral; in particular,

\mathbb E_P e=\int e^+\,dP-\int e^-\,dP\in\mathbb R\cup\{+\infty\}.

With this convention for the logarithmic expectation as well,

0=-\frac1\beta\log\mathbb E_P[e^{-\beta e}]\leq-\frac1\beta\mathbb E_P[\log(e^{-\beta e})]=\mathbb E_P e.

If $e$ is integrable, the extended mean equals the ordinary real integral $\int e\,dP$ . No finite-mean assumption is imposed for the main inequality.

This is the annealed-versus-quenched formulation of the second principle, preserving the placement of each logarithm.

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, (16)--(17): annealed <= quenched, with the two logarithm
placements preserved. The negative work part is integrable; the extended mean may
be +infinity. The final clause recovers the ordinary expectation if work is integrable.
No finite-mean-work hypothesis is added to the main assertion. -/
theorem secondPrinciple_extendedMean [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 : ℝ => max (-e) 0) P ∧
    (∫⁻ e, ENNReal.ofReal (max (-e) 0) ∂P) < ∞ ∧
    (0 : EReal) = ((-(1 / beta) * Real.log (∫ e, Real.exp (-beta * e) ∂P) : ℝ) : EReal) ∧
    ((-(1 / beta) * Real.log (∫ e, Real.exp (-beta * e) ∂P) : ℝ) : EReal) ≤
      ((-(1 / beta) : ℝ) : EReal) * extendedExpectation P (fun e => Real.log (Real.exp (-beta * e))) ∧
    ((-(1 / beta) : ℝ) : EReal) * extendedExpectation P (fun e => Real.log (Real.exp (-beta * e))) =
      extendedExpectation P (fun e => e) ∧
    (Integrable (fun e : ℝ => e) P →
      extendedExpectation P (fun e => e) = (((∫ e : ℝ, e ∂P) : ℝ) : EReal)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P15

Source

A Quantum Fluctuation Theorem, arXiv:cond-mat/0007360v2, PDF p. 4, Second principle as annealed/quenched inequality, (16)–(17)

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 supplies $T>0$ , $\hbar>0$ , $C\in\mathbb N$ , and spectral data $H_t=(\mu_t,h_t,F_t)$ , where $h_t$ is measurable, $F_t:E\to L^2(\mu_t;\mathbb C)$ is a complex linear isometric bijection taking each $b_i$ to a real function almost everywhere, and $H_{t+T}=H_t=H_{-t}$ . Its slice isometries 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,\quad 0\le r\le n,

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

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}, \qquad \mathbb E_P^{\mathrm{ext}}[f] = \left(\int^{-}\operatorname{ofReal}(f)\,dP\right) - \left(\int^{-}\operatorname{ofReal}(-f)\,dP\right),

where the last difference is in the extended real numbers and $\operatorname{ofReal}(r)=\max(r,0)$ . The theorem asserts that $e\mapsto\max(-e,0)$ is integrable and its nonnegative extended integral is strictly less than $+\infty$ , together with the extended-real chain

0 = -\frac1\beta\log\!\left(\int e^{-\beta e}\,dP(e)\right) \le -\frac1\beta\,\mathbb E_P^{\mathrm{ext}} \!\left[\log(e^{-\beta e})\right] = \mathbb E_P^{\mathrm{ext}}[e].

The real expression immediately after $0$ is embedded into the extended reals. Finally, if $e\mapsto e$ is integrable with respect to $P$ , then $\mathbb E_P^{\mathrm{ext}}[e]$ equals the real integral $\int e\,dP(e)$ , embedded into the extended reals. 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