Documentation

Lean 4 Proof

def sectorAllocationDistortion (e : NSectorEconomy N) (n : Fin N) : ℝ :=
  allocationDistortion (e.T n) (sectorCriticalFriction e n)

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:156

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file