Documentation

Lean 4 Proof

theorem kramersRate_pos {ℓ ω₀ ω_b ΔΦ T : ℝ}
    (hℓ : 0 < ℓ) (hω₀ : 0 < ω₀) (hω_b : 0 < ω_b) :
    0 < kramersRate ℓ ω₀ ω_b ΔΦ T := by
  unfold kramersRate
  apply mul_pos
  · exact div_pos (mul_pos (mul_pos hℓ hω₀) hω_b)
      (mul_pos (by norm_num) Real.pi_pos)
  · exact Real.exp_pos _

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:318

Module Section

### Kramers Escape Rate

In the same file