Theorem: Limit of Hölder Mean as Exponent tends to Zero is Geometric Mean

Let $x_1, x_2, \ldots, x_n \in \R_{\ge 0}$ be real numbers.
For $p \in \R_{\ne 0}$, let $\map {M_p} {x_1, x_2, \ldots, x_n}$ denote the '''Hölder mean with exponent $p$ of $x_1, x_2, \ldots, x_n$'''.
Then:
:$\ds \lim_{p \mathop \to 0} \map {M_p} {x_1, x_2, \ldots, x_n} = \paren {x_1 x_2 \cdots x_n}^{1 / n}$
which is the geometric mean of $x_1, x_2, \ldots, x_n$.

Proof:
Let $p \in \R$ such that $p \ne 0$.
{{begin-eqn}}
{{eqn | l = \map {M_p} {x_1, x_2, \ldots, x_n}
      | r = \paren {\frac 1 n \sum_{k \mathop = 1}^n {x_k}^p}^{1 / p}
      | c = {{Defof|Hölder Mean}}
}}
{{eqn | ll= \leadsto
      | l = \map \ln {\map {M_p} {x_1, x_2, \ldots, x_n} }
      | r = \map \ln {\frac 1 n \sum_{k \mathop = 1}^n {x_k}^p}^{1 / p}
      | c = taking logarithm of both sides
}}
{{eqn | r = \dfrac {\map \ln {\dfrac 1 n \ds \sum_{k \mathop = 1}^n {x_k}^p} } p
      | c = Logarithm of Power
}}
{{eqn | ll= \leadsto
      | l = \map {M_p} {x_1, x_2, \ldots, x_n}
      | r = \map \exp {\dfrac {\map \ln {\dfrac 1 n \ds \sum_{k \mathop = 1}^n {x_k}^p} } p}
      | c = taking exponential of both sides
}}
{{end-eqn}}
With a view to using L'Hôpital's Rule, let us express the argument of the  exponential on the {{RHS}} in the form:
{{begin-eqn}}
{{eqn | l = \dfrac {\map \ln {\dfrac 1 n \ds \sum_{k \mathop = 1}^n {x_k}^p} } p
      | r = \dfrac {\map f p} {\map g p}
      | c = where $\map f p := \map \ln {\dfrac 1 n \ds \sum_{k \mathop = 1}^n {x_k}^p}$ and $\map g p := p$
}}
{{end-eqn}}
Then we have:
{{begin-eqn}}
{{eqn | l = \map {f'} p
      | r = \map {\dfrac \d {\d p} } {\map \ln {\dfrac 1 n \sum_{k \mathop = 1}^n {x_k}^p} }
      | c = 
}}
{{eqn | r = \dfrac 1 {\dfrac 1 n \ds \sum_{k \mathop = 1}^n {x_k}^p} \paren {\dfrac 1 n \ds \sum_{k \mathop = 1}^n {x_k}^p \ln x_k}
      | c = Derivative of Natural Logarithm Function, Derivative of General Exponential Function, Chain Rule for Derivatives
}}
{{eqn | r = \dfrac {\ds \sum_{k \mathop = 1}^n {x_k}^p \ln x_k} {\ds \sum_{k \mathop = 1}^n {x_k}^p}
      | c = simplifying
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \map {g'} p
      | r = \map {\dfrac \d {\d p} } p
      | c = 
}}
{{eqn | r = 1
      | c = Derivative of Identity Function
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \lim_{p \mathop \to 0} \dfrac {\map f p} {\map g p}
      | r = \lim_{p \mathop \to 0} \dfrac {\map {f'} p} {\map {g'} p}
      | c = L'Hôpital's Rule
}}
{{eqn | r = \lim_{p \mathop \to 0} \dfrac {\paren {\dfrac {\ds \sum_{k \mathop = 1}^n {x_k}^p \ln x_k} {\ds \sum_{k \mathop = 1}^n {x_k}^p} } } 1
      | c = substituting for $f'$ and $g'$
}}
{{eqn | r = \lim_{p \mathop \to 0} \dfrac {\ds \sum_{k \mathop = 1}^n {x_k}^p \ln x_k} {\ds \sum_{k \mathop = 1}^n {x_k}^p}
      | c = simplifying
}}
{{eqn | r = \dfrac {\ds \sum_{k \mathop = 1}^n {x_k}^0 \ln x_k} {\ds \sum_{k \mathop = 1}^n {x_k}^0}
      | c = letting $p \to 0$
}}
{{eqn | r = \dfrac {\ds \sum_{k \mathop = 1}^n 1 \ln x_k} {\ds \sum_{k \mathop = 1}^n 1}
      | c = Zeroth Power of Real Number equals One
}}
{{eqn | r = \dfrac 1 n \sum_{k \mathop = 1} \ln x_k
      | c = further simplification
}}
{{eqn | r = \dfrac 1 n \ln \prod_{k \mathop = 1} x_k
      | c = Sum of Logarithms
}}
{{eqn | r = \map \ln {\paren {\prod_{k \mathop = 1} x_k}^{1 / n} }
      | c = Logarithm of Power
}}
{{eqn | ll= \leadsto
      | l = \lim_{p \mathop \to 0} \map {M_p} {x_1, x_2, \ldots, x_n}
      | r = \map \exp {\map \ln {\paren {\prod_{k \mathop = 1} x_k}^{1 / n} } }
      | c = 
}}
{{eqn | r = \paren {\prod_{k \mathop = 1} x_k}^{1 / n}
      | c = 
}}
{{eqn | r = \paren {x_1 x_2 \cdots x_n}^{1 / n}
      | c = 
}}
{{end-eqn}}
{{qed}}