Documentation

Lean 4 Proof

theorem crisisDuration_pos {ℓ ω₀ ω_b ΔΦ T : ℝ}
    (hℓ : 0 < ℓ) (hω₀ : 0 < ω₀) (hω_b : 0 < ω_b) :
    0 < crisisDuration ℓ ω₀ ω_b ΔΦ T :=
  div_pos one_pos (kramersRate_pos hℓ hω₀ hω_b)

Dependency Graph

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:372

Module Section

### Kramers Escape Rate

In the same file