Documentation

Lean 4 Proof

theorem kramersRate_increasing_in_T {ℓ ω₀ ω_b ΔΦ T₁ T₂ : ℝ}
    (hℓ : 0 < ℓ) (hω₀ : 0 < ω₀) (hω_b : 0 < ω_b)
    (hΔΦ : 0 < ΔΦ) (hT₁ : 0 < T₁) (_hT₂ : 0 < T₂) (hT : T₁ < T₂) :
    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₂
  -- Since ΔΦ > 0 and T₁ < T₂: ΔΦ/T₁ > ΔΦ/T₂, so -ΔΦ/T₁ < -ΔΦ/T₂
  simp only [neg_div]
  exact neg_lt_neg (div_lt_div_of_pos_left hΔΦ hT₁ hT)

Dependency Graph

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:328

Module Section

### Kramers Escape Rate

In the same file