Documentation

Lean 4 Proof

structure HierarchicalCESEconomy (N : ℕ) extends NSectorEconomy N where
  /-- Gain elasticity at each level. -/
  beta : Fin N → ℝ
  hbeta : ∀ n, 0 < beta n
  /-- Depreciation rate at each level. -/
  sigma : Fin N → ℝ
  hsigma : ∀ n, 0 < sigma n
  /-- Characteristic timescale at each level. -/
  eps : Fin N → ℝ
  heps : ∀ n, 0 < eps n
  /-- Equilibrium aggregate output at each level. -/
  Fbar : Fin N → ℝ
  hFbar : ∀ n, 0 < Fbar n

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/Defs.lean:39

Module Section

Core definitions for the Lean formalization of Paper 4:

In the same file