Documentation

Lean 4 Proof

def crisisDuration (ℓ ω₀ ω_b ΔΦ T : ℝ) : ℝ :=
  1 / kramersRate ℓ ω₀ ω_b ΔΦ T

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:368

Module Section

### Kramers Escape Rate

In the same file