ThmDex – An index of mathematical definitions, results, and conjectures.

Let $x_1, \dots, x_N \in [0, \infty)$ each be an D4767: Unsigned real number.
Let $\lambda_1, \dots, \lambda_N \in [0, \infty)$ each be an D4767: Unsigned real number such that

(i)	\begin{equation} \sum_{n = 1}^N \lambda_n = 1 \end{equation}

Since we can write $x^{\lambda_n}_n = e^{\lambda_n \log x_n}$, we can apply results

(i)	R3500: Homomorphism property of the standard natural real exponential function
(ii)	R3567: Standard natural real exponential function is subconvex

to conclude \begin{equation} \begin{split} \prod_{n = 1}^N x_n^{\lambda_n} = \prod_{n = 1}^N e^{\lambda_n \log x_n} = \exp \left( \sum_{n = 1}^N \lambda_n \log x_n \right) \leq \sum_{n = 1}^N \lambda_n e^{\log x_n} = \sum_{n = 1}^N \lambda_n x_n \end{split} \end{equation} The second claim is a consequence of the above results together with the result R5181: Subconvex real function preserves convex combination iff convex combination elements are all equal. $\square$

(1)	\begin{equation} \prod_{n = 1}^N x_n^{\lambda_n} \leq \sum_{n = 1}^N \lambda_n x_n \end{equation}
(2)	\begin{equation} \prod_{n = 1}^N x_n^{\lambda_n} = \sum_{n = 1}^N \lambda_n x_n \quad \iff \quad x_1 = x_2 = \cdots = x_N \end{equation}