Documentation

Lean 4 Proof

theorem entry_rate_pos_when_profitable {lambda pi cost : ℝ}
    (hlam : 0 < lambda) (hprofit : cost < pi) :
    0 < entryRate lambda pi cost := by
  simp only [entryRate]
  exact mul_pos hlam (lt_max_of_lt_right (by linarith))

Dependency Graph

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:174

Module Section

## Entry-Exit Dynamics

In the same file