Documentation

Lean 4 Proof

theorem crooksRatio_gt_one {W ΔF T : ℝ} (hT : 0 < T) (h : ΔF < W) :
    1 < crooksRatio W ΔF T := by
  unfold crooksRatio
  exact Real.one_lt_exp_iff.mpr (div_pos (by linarith) hT)

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:400

Module Section

### Kramers Escape Rate

In the same file