Documentation

Lean 4 Proof

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

Dependency Graph

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:219

Module Section

## Entry-Exit Dynamics

In the same file