Documentation

Lean 4 Proof

theorem minsky_trap_margin {dTstar_dT : ℝ} (h : dTstar_dT < 1) :
    dTstar_dT - 1 < 0 := by linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/BusinessCycles.lean:359

Module Section

Results 47-62: Business Cycles on the CES Landscape

In the same file