1 Applications of Jensen’s inequality
In this chapter, \(h\) denotes the function \(h(x) := x \log \frac{1}{x}\) for \(x \in [0,1]\).
\(h\) is strictly concave on \([0,1]\).
Proof
Check that \(h'\) is strictly monotone decreasing.
If \(S\) is a finite set, and \(\sum _{s \in S} w_s = 1\) for some non-negative \(w_s\), and \(p_s \in [0,1]\) for all \(s \in S\), then
\[ \sum _{s \in S} w_s h(p_s) \leq h(\sum _{s \in S} w_s p_s). \]
Proof
Apply Jensen and Lemma 1.1.
If equality holds in the above lemma, then \(p_s = \sum _{s \in S} w_s h(p_s)\) whenever \(w_s \neq 0\).
Proof
Need some converse form of Jensen, not sure if it is already in Mathlib. May also wish to state it as an if and only if.