Documentation

Lean 4 Proof

theorem endogenous_complementarity_lemma (e : NSectorEconomy N) :
    -- d(rho_bar)/dT > 0
    -- Average complementarity increases during crises
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/BusinessCycles.lean:336

Module Section

Results 47-62: Business Cycles on the CES Landscape

In the same file