Documentation

Lean 4 Proof

theorem K_deficit_from_concentration (hJ : 0 < J) {ρ : ℝ}
    {a : Fin J → ℝ} (_ha_sum : ∑ j : Fin J, a j = 1) :
    curvatureK J ρ - generalCurvatureK J ρ a =
    (1 - ρ) * (herfindahlIndex J a - 1 / ↑J) := by
  simp only [curvatureK, generalCurvatureK, herfindahlIndex]
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  field_simp
  ring

Dependency Graph

Location

thesis/CESProofs/EntryExit/CurvatureInJ.lean:182

Module Section

## Entry with General Weights

In the same file