Documentation

Lean 4 Proof

theorem convergenceRate_entry_pos {lambda sf : ℝ}
    (hlam : 0 < lambda) (hsf : 0 < sf) :
    0 < convergenceRate_entry lambda sf := by
  simp only [convergenceRate_entry]
  exact mul_pos hlam hsf

Dependency Graph

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:215

Module Section

## Entry-Exit Dynamics

In the same file