Documentation

Lean 4 Proof

theorem sectorGeneralCurvature_le_standard
    {N : ℕ} (e : WeightedNSectorEconomy N) (n : Fin N)
    (hρ : e.ρ n < 1) (hJ : 2 ≤ e.J n) :
    sectorGeneralCurvature e n ≤ sectorCurvature e.toNSectorEconomy n := by
  unfold sectorGeneralCurvature sectorCurvature
  exact equalWeights_maximize_K hJ hρ (e.ha_pos n) (e.ha_sum n)

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/Defs.lean:276

Module Section

## Weighted N-Sector Economy

In the same file