Documentation

Lean 4 Proof

theorem recovery_speed (epsilon ell gradF : ℝ)
    (h_eps : 0 < epsilon) (hell : 0 < ell) (hgrad : 0 < gradF) :
    0 < epsilon * ell * gradF := by positivity

Dependency Graph

Location

thesis/CESProofs/Dynamics/BusinessCycles.lean:315

Module Section

Results 47-62: Business Cycles on the CES Landscape

In the same file