Documentation

Lean 4 Proof

theorem faster_entry_faster_convergence {lambda₁ lambda₂ sf : ℝ}
    (hlam : lambda₁ < lambda₂) (hsf : 0 < sf) :
    convergenceRateEntry lambda₁ sf < convergenceRateEntry lambda₂ sf := by
  simp only [convergenceRateEntry]
  exact mul_lt_mul_of_pos_right hlam hsf

Dependency Graph

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:226

Module Section

## Entry-Exit Dynamics

In the same file