Documentation

Lean 4 Proof

theorem crisisDuration_increasing_in_barrier {ℓ ω₀ ω_b ΔΦ₁ ΔΦ₂ T : ℝ}
    (hℓ : 0 < ℓ) (hω₀ : 0 < ω₀) (hω_b : 0 < ω_b)
    (hT : 0 < T) (hΔΦ : ΔΦ₁ < ΔΦ₂) :
    crisisDuration ℓ ω₀ ω_b ΔΦ₁ T < crisisDuration ℓ ω₀ ω_b ΔΦ₂ T := by
  unfold crisisDuration
  exact one_div_lt_one_div_of_lt (kramersRate_pos hℓ hω₀ hω_b)
    (kramersRate_decreasing_in_barrier hℓ hω₀ hω_b hT hΔΦ)

Dependency Graph

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:378

Module Section

### Kramers Escape Rate

In the same file