Documentation

Lean 4 Proof

theorem crooksRatio_pos (W ΔF T : ℝ) :
    0 < crooksRatio W ΔF T :=
  Real.exp_pos _

Dependency Graph

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:395

Module Section

### Kramers Escape Rate

In the same file