Documentation

Lean 4 Proof

theorem theil_bounded_by_log_J (hJ : 0 < J)
    (hs_pos : ∀ j : Fin J, 0 < s j)
    (hs_sum : ∑ j : Fin J, s j = 1)
    (hs_le : ∀ j : Fin J, s j ≤ 1) :
    theilIndex J s ≤ Real.log ↑J := by
  simp only [theilIndex]
  calc ∑ j : Fin J, s j * Real.log (↑J * s j)
      ≤ ∑ j : Fin J, s j * Real.log ↑J := by
        apply Finset.sum_le_sum
        intro j _
        apply mul_le_mul_of_nonneg_left _ (le_of_lt (hs_pos j))
        apply Real.log_le_log (mul_pos (by exact_mod_cast hJ) (hs_pos j))
        calc ↑J * s j ≤ ↑J * 1 := by
              apply mul_le_mul_of_nonneg_left (hs_le j) (by exact_mod_cast le_of_lt hJ)
            _ = ↑J := mul_one _
    _ = (∑ j : Fin J, s j) * Real.log ↑J := by rw [Finset.sum_mul]
    _ = 1 * Real.log ↑J := by rw [hs_sum]
    _ = Real.log ↑J := one_mul _

Dependency Graph

Location

thesis/CESProofs/Applications/Inequality.lean:280

Module Section

## CES Inequality Measures

In the same file