Documentation

Lean 4 Proof

theorem asymmetric_kramers_ratio {DeltaF_fwd DeltaF_rev T : ℝ}
    (hT : 0 < T) (hfwd_lower : DeltaF_fwd < DeltaF_rev) :
    Real.exp (DeltaF_rev / T) > Real.exp (DeltaF_fwd / T) := by
  exact Real.exp_strictMono (div_lt_div_of_pos_right hfwd_lower hT)

Dependency Graph

Location

thesis/CESProofs/Dynamics/SymmetricAdjustment.lean:178

Module Section

Results 17-25: Symmetric Adjustment and Transition Rates

In the same file