ThmDex – An index of mathematical definitions, results, and conjectures.
Result R5647 on D5725: Simple random variable entropy
Subresult of R5358: Gibbs' inequality for simple relative entropy
Gibb's inequality for simple entropy
Formulation 0
Let $p_1, p_2, \, \ldots, \, p_N \in (0, 1]$ each be a D993: Real number such that
(i) \begin{equation} \sum_{n = 1}^N p_n = 1 \end{equation}
Let $\log_a$ be the D866: Standard real logarithm function in base $a \in (0, \infty) \setminus \{ 1 \}$.
Then
(1) \begin{equation} - \sum_{n = 1}^N p_n \log_a p_n \leq \log_a N \end{equation}
(2) \begin{equation} - \sum_{n = 1}^N p_n \log_a p_n = \log_a N \quad \iff \quad p_1 = p_2 = \cdots = p_N = \frac{1}{N} \end{equation}
Formulation 1
Let $X \in \text{Random}(\mathcal{X})$ be a D5723: Simple random variable.
Let $\log_a$ be the D866: Standard real logarithm function in base $a \in (0, \infty) \setminus \{ 1 \}$.
Then
(1) \begin{equation} - \sum_{x \in \mathcal{X}} \mathbb{P}(X = x) \log_a \mathbb{P}(X = x) \leq \log_a |\mathcal{X}| \end{equation}
(2) \begin{equation} - \sum_{x \in \mathcal{X}} \mathbb{P}(X = x) \log_a \mathbb{P}(X = x) = \log_a |\mathcal{X}| \quad \iff \quad \forall \, x \in \mathcal{X} : \mathbb{P}(X = x) = \frac{1}{|\mathcal{X}|} \end{equation}
Formulation 2
Let $X \in \text{Random}(\mathcal{X})$ be a D5723: Simple random variable such that
(i) \begin{equation} \forall \, x \in \mathcal{X} : p(x) : = \mathbb{P}(X = x) \end{equation}
Let $\log_a$ be the D866: Standard real logarithm function in base $a \in (0, \infty) \setminus \{ 1 \}$.
Then
(1) \begin{equation} - \sum_{x \in \mathcal{X}} p(x) \log_a p(x) \leq \log_a |\mathcal{X}| \end{equation}
(2) \begin{equation} - \sum_{x \in \mathcal{X}} p(x) \log_a p(x) = \log_a |\mathcal{X}| \quad \iff \quad \forall \, x \in \mathcal{X} : p(x) = \frac{1}{|\mathcal{X}|} \end{equation}
Proofs
Proof 0
Let $p_1, p_2, \, \ldots, \, p_N \in (0, 1]$ each be a D993: Real number such that
(i) \begin{equation} \sum_{n = 1}^N p_n = 1 \end{equation}
Let $\log_a$ be the D866: Standard real logarithm function in base $a \in (0, \infty) \setminus \{ 1 \}$.
This result is a special case of R5358: Gibbs' inequality for simple relative entropy with \begin{equation} q_1 = q_2 = \cdots = q_N = \frac{1}{N} \end{equation} This is because in this case we have \begin{equation} \log_a q_n = \log_a \frac{1}{N} = \log_a 1 - \log_a N = - \log_a N \end{equation} and therefore \begin{equation} - \sum_{n = 1}^N p_n \log_a q_n = - \sum_{n = 1}^N p_n \log_a \frac{1}{N} = \log_a N \sum_{n = 1}^N p_n = \log_a N \end{equation} $\square$