Documentation

Lean 4 Proof

theorem policy_kramers_amplification {_DeltaF delta T : ℝ}
    (hT : 0 < T) (hdelta : 0 < delta) :
    Real.exp (delta / T) > 1 := by
  rw [gt_iff_lt]
  exact Real.one_lt_exp_iff.mpr (div_pos hdelta hT)

Dependency Graph

Location

thesis/CESProofs/Dynamics/SymmetricAdjustment.lean:157

Module Section

Results 17-25: Symmetric Adjustment and Transition Rates

In the same file