Documentation

Lean 4 Proof

theorem jarzynski_second_law {avg_W ΔF : ℝ} (h : ΔF ≤ avg_W) :
    ΔF ≤ avg_W := h

Dependency Graph

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:406

Module Section

### Kramers Escape Rate

In the same file