Documentation

Lean 4 Proof

theorem sectorGeneralCurvature_pos
    {N : ℕ} (e : WeightedNSectorEconomy N) (n : Fin N)
    (hρ : e.ρ n < 1) (hJ : 2 ≤ e.J n)
    (hH : sectorHerfindahl e n < 1) :
    0 < sectorGeneralCurvature e n := by
  unfold sectorGeneralCurvature
  exact gen_quadruple_K_pos hJ hρ (e.ha_pos n) (e.ha_sum n) hH

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/Defs.lean:267

Module Section

## Weighted N-Sector Economy

In the same file