Documentation

Lean 4 Proof

theorem theil_zero_at_equality (hJ : 0 < J) :
    theilIndex J (fun _ : Fin J => (1 / ↑J : ℝ)) = 0 := by
  simp only [theilIndex]
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  conv_lhs =>
    arg 2; ext j
    rw [show (↑J : ℝ) * (1 / ↑J) = 1 from by field_simp]
  simp [Real.log_one]

Dependency Graph

Location

thesis/CESProofs/Applications/Inequality.lean:228

Module Section

## CES Inequality Measures

In the same file