Documentation

Lean 4 Proof

theorem active_dynamics_iff_nondegen_weights
    {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
  exact sectorGeneralCurvature_pos e n hρ hJ hH

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:429

Module Section

## Corollary 3b.1: Multi-Scale Pre-Crisis Deceleration

In the same file