Documentation

Lean 4 Proof

theorem sectorAllocationDistortion_nonneg (e : NSectorEconomy N) (n : Fin N) :
    0 ≤ sectorAllocationDistortion e n := by
  unfold sectorAllocationDistortion
  exact allocationDistortion_nonneg (e.hT n) (sectorCriticalFriction_pos e n)

Dependency Graph

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:160

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file