Documentation

Lean 4 Proof

theorem share_variance_eq_H_minus_inv (hJ : 0 < J)
    (hs_sum : ∑ j : Fin J, s j = 1) :
    shareVariance J s = herfindahlIndex J s - 1 / ↑J := by
  simp only [shareVariance, herfindahlIndex]
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  have expand : ∀ j : Fin J, (s j - 1 / ↑J) ^ 2 = s j ^ 2 - 2 * s j / ↑J + (1 / ↑J) ^ 2 := by
    intro j; ring
  simp_rw [expand]
  rw [Finset.sum_add_distrib, Finset.sum_sub_distrib]
  simp_rw [show ∀ j : Fin J, 2 * s j / (↑J : ℝ) = 2 / ↑J * s j from fun j => by ring]
  rw [← Finset.mul_sum, hs_sum]
  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  field_simp
  ring

Dependency Graph

Location

thesis/CESProofs/Applications/Inequality.lean:316

Module Section

## CES Inequality Measures

In the same file