Documentation

Lean 4 Proof

theorem kramersRate_increasing_in_curvature {ℓ ω₀₁ ω₀₂ ω_b ΔΦ T : ℝ}
    (hℓ : 0 < ℓ) (_hω₀₁ : 0 < ω₀₁) (_hω₀₂ : 0 < ω₀₂)
    (hω_b : 0 < ω_b) (hω : ω₀₁ < ω₀₂) :
    kramersRate ℓ ω₀₁ ω_b ΔΦ T < kramersRate ℓ ω₀₂ ω_b ΔΦ T := by
  unfold kramersRate
  apply mul_lt_mul_of_pos_right _ (Real.exp_pos _)
  apply div_lt_div_of_pos_right _ (mul_pos (by norm_num) Real.pi_pos)
  exact mul_lt_mul_of_pos_right (mul_lt_mul_of_pos_left hω hℓ) hω_b

Dependency Graph

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:354

Module Section

### Kramers Escape Rate

In the same file