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

Result R5211 on D2455: Real geometric mean
Subresult of R5182: Tight upper bound to a finite product of unsigned real numbers

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.