Documentation

Lean 4 Proof

theorem theil_nonneg (hJ : 0 < J) (s : Fin J → ℝ)
    (hs_pos : ∀ j : Fin J, 0 < s j)
    (hs_sum : ∑ j : Fin J, s j = 1) :
    0 ≤ theilIndex J s := by
  simp only [theilIndex]
  -- Use Jensen's inequality: f convex, weights w_j = 1/J, points p_j = J * s_j
  -- f(∑ w_j * p_j) ≤ ∑ w_j * f(p_j) where f(x) = x * log(x)
  have hJpos : (0 : ℝ) < (↑J : ℝ) := Nat.cast_pos.mpr hJ
  have hJne : (↑J : ℝ) ≠ 0 := ne_of_gt hJpos
  -- The weighted sum of points equals 1
  have hw_sum : ∑ j : Fin J, (1 / (↑J : ℝ)) = 1 := by
    rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin]
    simp [hJne]
  -- Rewrite: ∑ s_j * log(J * s_j) = ∑ (1/J) * ((J*s_j) * log(J*s_j))
  have key : ∀ j : Fin J,
      s j * Real.log (↑J * s j) = (1 / ↑J) * ((↑J * s j) * Real.log (↑J * s j)) := by
    intro j; field_simp
  simp_rw [key]
  -- The weighted sum of points: ∑ (1/J) * (J * s_j) = ∑ s_j = 1
  have hcenter : ∑ j : Fin J, (1 / (↑J : ℝ)) • (↑J * s j) = 1 := by
    simp only [smul_eq_mul]
    have : ∀ j : Fin J, 1 / (↑J : ℝ) * (↑J * s j) = s j := by
      intro j; field_simp
    simp_rw [this, hs_sum]
  -- Apply Jensen: f(1) ≤ ∑ (1/J) * f(J * s_j)
  have jensen := ConvexOn.map_sum_le Real.convexOn_mul_log
    (fun i _ => le_of_lt (div_pos one_pos hJpos))
    hw_sum
    (fun i _ => Set.mem_Ici.mpr (le_of_lt (mul_pos hJpos (hs_pos i))))
  -- f(1) = 1 * log 1 = 0
  rw [hcenter] at jensen
  simp only [smul_eq_mul, Real.log_one, mul_zero] at jensen
  linarith

Dependency Graph

Location

thesis/CESProofs/Applications/Inequality.lean:245

Module Section

## CES Inequality Measures

In the same file