Kramers Rate

def proved Dynamics & Crises

Documentation

Lean 4 Proof

def kramersRate (ℓ ω₀ ω_b ΔΦ T : ℝ) : ℝ :=
  ℓ * ω₀ * ω_b / (2 * Real.pi) * Real.exp (-ΔΦ / T)

Dependency Graph

Used by

kramersRate_increasing_in_curvature crisisDuration kramersRate_increasing_in_T kramersRate_decreasing_in_barrier kramersRate_pos

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:314

Module Section

### Kramers Escape Rate