Documentation

Lean 4 Proof

theorem theil_decomposition_additive (hJ : 0 < J) (s : Fin J → ℝ)
    (hs_pos : ∀ j : Fin J, 0 < s j)
    (hs_sum : ∑ j : Fin J, s j = 1) :
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Applications/Inequality.lean:354

Module Section

## CES Inequality Measures

In the same file