Documentation

Lean 4 Proof

theorem kramersRate_decreasing_in_barrier {ℓ ω₀ ω_b ΔΦ₁ ΔΦ₂ T : ℝ}
    (hℓ : 0 < ℓ) (hω₀ : 0 < ω₀) (hω_b : 0 < ω_b)
    (hT : 0 < T) (hΔΦ : ΔΦ₁ < ΔΦ₂) :
    kramersRate ℓ ω₀ ω_b ΔΦ₂ T < kramersRate ℓ ω₀ ω_b ΔΦ₁ T := by
  unfold kramersRate
  apply mul_lt_mul_of_pos_left _ (div_pos (mul_pos (mul_pos hℓ hω₀) hω_b)
    (mul_pos (by norm_num) Real.pi_pos))
  apply Real.exp_strictMono
  -- Need: -ΔΦ₂/T < -ΔΦ₁/T
  exact div_lt_div_of_pos_right (neg_lt_neg hΔΦ) hT

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:342

Module Section

### Kramers Escape Rate

In the same file