Documentation

Lean 4 Proof

theorem K_decreasing_in_herfindahl_sector
    {J : ℕ} {ρ : ℝ} (hρ : ρ < 1)
    {a₁ a₂ : Fin J → ℝ}
    (hH : herfindahlIndex J a₁ < herfindahlIndex J a₂) :
    generalCurvatureK J ρ a₂ < generalCurvatureK J ρ a₁ := by
  unfold generalCurvatureK herfindahlIndex at *
  nlinarith [show 0 < 1 - ρ from by linarith]

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/Defs.lean:284

Module Section

## Weighted N-Sector Economy

In the same file