Documentation

Lean 4 Proof

theorem qCrooks_reversibility :
    -- P_forward/P_reverse = qExp q (ΔΦ/T)
    -- Implies detailed balance for the q-Langevin dynamics
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Potential/QDynamics.lean:121

Module Section

Theorems 5-7, Corollaries 2-4, Propositions 8-11:

In the same file