ThmDex – An index of mathematical definitions, results, and conjectures.
Result R5211 on D2455: Real geometric mean
Tight upper bound to a product of three unsigned real numbers
Formulation 0
Let $x, y, z \in [0, \infty)$ each be an D4767: Unsigned real number.
Then
(1) \begin{equation} x y z \leq \left( \frac{x + y + z}{3} \right)^3 \end{equation}
(2) \begin{equation} x y z = \left( \frac{x + y + z}{3} \right)^3 \quad \iff\quad x = y = z \end{equation}
Proofs
Proof 0
Let $x, y, z \in [0, \infty)$ each 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$