Lean 4 Proof

theorem transition_time_pos {k : ℝ} (hk : 0 < k) :
    0 < medianTransitionTime k := by
  simp only [medianTransitionTime]
  exact div_pos (Real.log_pos (by norm_num)) hk

Dependency Graph

Location

thesis/CESProofs/Dynamics/SymmetricAdjustment.lean:136

Module Section

Results 17-25: Symmetric Adjustment and Transition Rates

In the same file