Documentation

Lean 4 Proof

theorem concentration_reduces_max_Keff
    {J : ℕ} (_hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {a₁ a₂ : Fin J → ℝ}
    (hH : herfindahlIndex J a₁ < herfindahlIndex J a₂)
    {Tstar : ℝ} (hTs : 0 < Tstar) :
    generalEffectiveCurvatureKeff J ρ a₂ 0 Tstar
    < generalEffectiveCurvatureKeff J ρ a₁ 0 Tstar := by
  rw [generalKeff_zero_friction hTs, generalKeff_zero_friction hTs]
  exact K_decreasing_in_herfindahl hρ hH

Dependency Graph

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:397

Module Section

## General-Weight Effective Curvature Theorems

In the same file