ThmDex – An index of mathematical definitions, results, and conjectures.
Tight lower bound to a finite product of positive real numbers
Formulation 0
Let $x_1, \dots, x_N \in (0, \infty)$ each be a D5407: Positive real number.
Then
(1) \begin{equation} \left( \frac{1}{\frac{1}{N} \sum_{n = 1}^N \frac{1}{x_n}} \right)^N \leq \prod_{n = 1}^N x_n \end{equation}
(2) \begin{equation} \left( \frac{1}{\frac{1}{N} \sum_{n = 1}^N \frac{1}{x_n}} \right)^N = \prod_{n = 1}^N x_n \quad \iff \quad \frac{1}{x_1} = \frac{1}{x_2} = \cdots = \frac{1}{x_N} \end{equation}
Subresults
R5186: Unique global minimizer for a finite product of positive real numbers with a given sum of multiplicative inverses
Proofs
Proof 0
Let $x_1, \dots, x_N \in (0, \infty)$ each be a D5407: Positive real number.
This result is a particular case of R4666: Real GM-HM inequality. $\square$