ThmDex – An index of mathematical definitions, results, and conjectures.
Unique global maximizer for a finite product of unsigned real numbers with a given sum
Formulation 0
Let $a \in [0, \infty)$ be an D4767: Unsigned real number.
Then \begin{equation} \frac{1}{N} (a, a, \ldots, a) = \underset{x \in [0, \infty)^N : \sum_{n = 1}^N x_n = a}{\text{arg max}} \, \prod_{n = 1}^N x_n \end{equation}
Proofs
Proof 0
Let $a \in [0, \infty)$ be an D4767: Unsigned real number.
This result is a particular case of R5182: Tight upper bound to a finite product of unsigned real numbers. $\square$