Documentation

Lean 4 Proof

theorem K_decreasing_in_herfindahl
    {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 *
  have hρ_pos : 0 < 1 - ρ := by linarith
  nlinarith

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:363

Module Section

## General-Weight Effective Curvature Theorems

In the same file