Documentation

Lean 4 Proof

structure NSectorEconomy (N : ℕ) where
  J : Fin N → ℕ
  hJ : ∀ n, 2 ≤ J n
  ρ : Fin N → ℝ
  hρ : ∀ n, ρ n < 1
  T : Fin N → ℝ
  hT : ∀ n, 0 ≤ T n
  ℓ : Fin N → ℝ
  hℓ : ∀ n, 0 < ℓ n
  c : Fin N → ℝ
  hc : ∀ n, 0 < c n
  d_sq : Fin N → ℝ
  hd : ∀ n, 0 < d_sq n

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/Defs.lean:37

Module Section

Core definitions for the Lean formalization of Paper 3:

In the same file