Equivalence of Definitions of Real Exponential Function

From ProofWiki
Jump to: navigation, search

Theorem

The following definitions of the concept of Real Exponential Function are equivalent:

As a Sum of a Series

The exponential function can be defined as a power series:

$\exp x := \displaystyle \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}$

As a Limit of a Sequence

The exponential function can be defined as the following limit of a sequence:

$\exp x := \displaystyle \lim_{n \mathop \to +\infty} \paren {1 + \frac x n}^n$

As an Extension of the Rational Exponential

Let $e$ denote Euler's number.

Let $f: \Q \to \R$ denote the real-valued function defined as:

$f \left({ x }\right) = e^x$

That is, let $f \left({ x }\right)$ denote $e$ to the power of $x$, for rational $x$.


Then $\exp : \R \to \R$ is defined to be the unique continuous extension of $f$ to $\R$.

$\exp \left({ x }\right)$ is called the exponential of $x$.

As the Inverse of the Natural Logarithm

Consider the natural logarithm $\ln x$, which is defined on the open interval $\left({0 \,.\,.\, +\infty}\right)$.

From Logarithm is Strictly Increasing:

$\ln x$ is strictly increasing.

From Inverse of Strictly Monotone Function:

the inverse of $\ln x$ always exists.


The inverse of the natural logarithm function is called the exponential function, which is denoted as $\exp$.

Thus for $x \in \R$, we have:

$y = \exp x \iff x = \ln y$

As the Solution of a Differential Equation

The exponential function can be defined as the unique solution $y = f \left({x}\right)$ to the first order ODE:

$\dfrac {\d y} {\d x} = y$

satisfying the initial condition $f \left({0}\right) = 1$.


Proof

Inverse of Natural Logarithm implies Limit of Sequence

Let $\exp x$ be the real function defined as the inverse of the natural logarithm:

$y = \exp x \iff x = \ln y$


Let $\left \langle {x_n} \right \rangle$ be the sequence in $\R$ defined as:

$x_n = \paren {1 + \dfrac x n}^n$


First it needs to be noted that $\left \langle {x_n} \right \rangle$ does indeed converge to a limit.

From Equivalence of Definitions of Real Exponential Function: Limit of Sequence implies Sum of Series, we have:

$\displaystyle \lim_{n \mathop \to \infty} \paren {1 + \dfrac x n}^n = \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}$

From Series of Power over Factorial Converges, the right hand side is indeed shown to converge to a limit.


It will next be shown that:

$\displaystyle \ln \paren {\lim_{n \mathop \to \infty} \left \langle {x_n} \right \rangle} = x$


We have:

\(\displaystyle \ln \paren {\paren {1 + \frac x n}^n}\) \(=\) \(\displaystyle n \ln \paren {1 + x n^{-1} }\) $\quad$ Logarithms of Powers $\quad$
\(\displaystyle \) \(=\) \(\displaystyle x \frac {\ln \paren {1 + x n^{-1} } } {x n^{-1} }\) $\quad$ multiplying by $1 = \dfrac {x n^{-1} } {x n^{-1} }$ $\quad$

From Limit of Sequence is Limit of Real Function, we can consider the differentiable analogue of the sequence.

From Derivative of Logarithm at One we have:

$\displaystyle \lim_{x \mathop \to 0} \frac {\ln \paren {1 + x} } x = 1$


But $x n^{-1} \to 0$ as $n \to \infty$ from Power of Reciprocal.

Thus:

$\displaystyle x \frac {\ln \paren {1 + x n^{-1} } } {x n^{-1} } \to x$

as $n \to \infty$.


From Exponential Function is Continuous:

$\paren {1 + \dfrac x n}^n = \exp \paren {n \ln \paren {1 + \dfrac x n} } \to \exp x = e^x$

as $n \to \infty$.

$\blacksquare$


Limit of Sequence implies Sum of Series

Let $\exp x$ be the real function defined as the limit of the sequence:

$\exp x := \displaystyle \lim_{n \mathop \to \infty} \paren {1 + \frac x n}^n$

From the General Binomial Theorem:

\(\displaystyle \paren {1 + \frac x n}^n\) \(=\) \(\displaystyle 1 + x + \frac {n \paren {n - 1} x^2} {2! \ n^2} + \frac {n \paren {n - 1} \paren {n - 2} x^3} {3! \ n^3} + \cdots\) $\quad$ $\quad$
\(\displaystyle \) \(=\) \(\displaystyle \frac {x^0} {0!} + \frac {x^1} {1!} + \paren {\frac {n - 1} n} \frac {x^2} {2!} + \paren {\frac {\paren {n - 1} \paren {n - 2} } {n^2} } \frac {x^3} {3!} + \cdots\) $\quad$ $\quad$
\(\displaystyle \leadsto \ \ \) \(\displaystyle 0\) \(=\) \(\displaystyle \paren {1 + \frac x n}^n - \frac {x^0} {0!} + \frac {x^1} {1!} + \paren {\frac {n - 1} n} \frac {x^2} {2!} + \paren {\frac {\paren {n - 1} \paren {n - 2} } {n^2} } \frac {x^3} {3!} + \cdots\) $\quad$ $\quad$

From Power over Factorial, this converges to:

$\exp x - \dfrac {x^0} {0!} + \dfrac {x^1} {1!} + \dfrac {x^2} {2!} + \dfrac {x^3} {3!} + \cdots = 0$

as $n \to +\infty$:

\(\displaystyle \leadsto \ \ \) \(\displaystyle \exp x\) \(=\) \(\displaystyle \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}\) $\quad$ $\quad$

$\blacksquare$


Limit of Sequence implies Extension of Rational Exponential

Let the restriction of the exponential function to the rationals be defined as:

$\displaystyle \exp \restriction_\Q: x \mapsto \lim_{n \mathop \to +\infty}\left ({1 + \frac x n}\right)^n$


Thus, let $e$ be Euler's Number defined as:

$e = \displaystyle \lim_{n \mathop \to +\infty}\left ({1 + \frac 1 n}\right)^n$


For $x = 0$:

\(\displaystyle \exp \restriction_\Q \paren 0 \ \ \) \(\displaystyle \) \(=\) \(\displaystyle \lim_{n \mathop \to +\infty} \paren {1 + \frac 0 n}^n\) $\quad$ $\quad$
\(\displaystyle \) \(=\) \(\displaystyle 1\) $\quad$ $\quad$
\(\displaystyle \) \(=\) \(\displaystyle e^0\) $\quad$ $\quad$

For $x \ne 0$:

\(\displaystyle \exp \restriction_\Q \paren x \ \ \) \(\displaystyle \) \(=\) \(\displaystyle \lim_{n \mathop \to +\infty}\paren {1 + \frac x n}^n\) $\quad$ $\quad$
\(\displaystyle \) \(=\) \(\displaystyle \lim_{\paren {n/x} \mathop \to +\infty}\paren {\paren {1 + \frac 1 {\paren {n/x} } }^{\paren {n/x} } }^x\) $\quad$ Exponent Combination Laws $\quad$
\(\displaystyle \) \(=\) \(\displaystyle e^x\) $\quad$ $\quad$

For $x \in \R \setminus \Q$, we invoke Power Function to Rational Power permits Unique Continuous Extension.

$\blacksquare$


Extension of Rational Exponential implies Solution of Differential Equation

Let $\exp x$ be the real function defined as the extension of rational exponential.


Then we have:

\(\displaystyle D_x \left({\exp x}\right)\) \(=\) \(\displaystyle \lim_{h \mathop \to 0} \frac {\exp \left({x + h}\right) - \exp x} h\) $\quad$ Definition of Derivative $\quad$
\(\displaystyle \) \(=\) \(\displaystyle \lim_{h \mathop \to 0} \frac {\exp x \cdot \exp h - \exp x} h\) $\quad$ Exponent of Sum $\quad$
\(\displaystyle \) \(=\) \(\displaystyle \lim_{h \mathop \to 0} \frac {\exp x \left({\exp h - 1}\right)} h\) $\quad$ $\quad$
\(\displaystyle \) \(=\) \(\displaystyle \exp x \left({\lim_{h \mathop \to 0} \frac {\exp h - 1} h}\right)\) $\quad$ Multiple Rule for Limits of Functions, as $\exp x$ is constant $\quad$
\(\displaystyle \) \(=\) \(\displaystyle \exp x\) $\quad$ Derivative of Exponential at Zero: Proof 2 $\quad$


The application of Derivative of Exponential at Zero is not circular as the referenced proof does not depend on $D_x \exp x = \exp x$.

$\Box$

\(\displaystyle \exp 0\) \(=\) \(\displaystyle \lim_{n \mathop \to +\infty} \left({1 + \frac 0 n}\right)^n\) $\quad$ $\quad$
\(\displaystyle \) \(=\) \(\displaystyle 1\) $\quad$ $\quad$

$\blacksquare$


Sum of Series equivalent to Solution of Differential Equation

Sum of Series implies Solution of Differential Equation

Let $\exp x$ be the real function defined as the sum of the power series:

$\exp x := \displaystyle \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}$


Let $y = \displaystyle \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}$.


Then:

\(\displaystyle \dfrac {\d y} {\d x}\) \(=\) \(\displaystyle \dfrac \d {\d x} \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}\) $\quad$ $\quad$
\(\displaystyle \) \(=\) \(\displaystyle \dfrac \d {\d x} \paren {\frac {x^0} {0!} + \sum_{n \mathop = 1}^\infty \frac {x^n} {n!} }\) $\quad$ extracting the zeroth term $\quad$
\(\displaystyle \) \(=\) \(\displaystyle 0 + \sum_{n \mathop = 1}^\infty \frac {n x^{n - 1} } {n!}\) $\quad$ Power Rule for Derivatives and Derivative of Constant $\quad$
\(\displaystyle \) \(=\) \(\displaystyle \sum_{n \mathop = 1}^\infty \frac {x^{n - 1} } {\paren {n - 1}!}\) $\quad$ simplifying $\quad$
\(\displaystyle \) \(=\) \(\displaystyle \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}\) $\quad$ Translation of Index Variable of Summation $\quad$
\(\displaystyle \) \(=\) \(\displaystyle y\) $\quad$ $\quad$


Setting $x = 0$ we find:

\(\displaystyle y \paren 0\) \(=\) \(\displaystyle \sum_{n \mathop = 0}^\infty \frac {0^n} {n!}\) $\quad$ $\quad$
\(\displaystyle \) \(=\) \(\displaystyle \frac {0^0} {0!} + \sum_{n \mathop = 1}^\infty \frac {0^n} {n!}\) $\quad$ $\quad$
\(\displaystyle \) \(=\) \(\displaystyle \frac {0^0} {0!}\) $\quad$ as $0^n = 0$ for all $n > 0$ $\quad$
\(\displaystyle \) \(=\) \(\displaystyle 1\) $\quad$ Definition of $0^0$ $\quad$

$\blacksquare$


That is:

$\exp x$ is the solution of the differential equation:

$\dfrac {\d y} {\d x} = y$

satisfying the initial condition $f \left({0}\right) = 1$.

$\Box$


Solution of Differential Equation implies Sum of Series

Let $\exp x$ be the real function defined as the solution of the differential equation:

$\dfrac {\d y} {\d x} = y$

satisfying the initial condition $f \left({0}\right) = 1$.


We have Taylor Series Expansion for Exponential Function:


From Higher Derivatives of Exponential Function, we have:

$\forall n \in \N: f^{\left({n}\right)} \left({\exp x}\right) = \exp x$


Since $\exp 0 = 1$, the Taylor series expansion for $\exp x$ about $0$ is given by:

$\displaystyle \exp x = \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}$


From Radius of Convergence of Power Series over Factorial, we know that this power series expansion converges for all $x \in \R$.

From Taylor's Theorem, we know that

$\displaystyle \exp x = 1 + \frac x {1!} + \frac {x^2} {2!} + \cdots + \frac {x^{n - 1}} {\left({n - 1}\right)!} + \frac {x^n} {n!} \exp \left({\eta}\right)$

where $0 \le \eta \le x$.

Hence:

\(\displaystyle \left \vert {\exp x - \left({1 + \frac x {1!} + \frac {x^2} {2!} + \cdots + \frac {x^{n - 1} } {\left({n - 1}\right)!} }\right)} \right \vert\) \(=\) \(\displaystyle \left \vert {\frac {x^n} {n!} \exp \left({\eta}\right)} \right \vert\) $\quad$ $\quad$
\(\displaystyle \) \(\le\) \(\displaystyle \frac {\left \vert {x^n} \right \vert} {n!} \exp \left({\left \vert {x} \right \vert}\right)\) $\quad$ Exponential is Strictly Increasing $\quad$
\(\displaystyle \) \(\to\) \(\displaystyle 0 \text { as } n \to \infty\) $\quad$ Series of Power over Factorial Converges $\quad$


So the partial sums of the power series converge to $\exp x$.

The result follows.

$\blacksquare$


Inverse of Natural Logarithm equivalent to Solution of Differential Equation

Inverse of Natural Logarithm implies Solution of Differential Equation

Let $\exp x$ be the real function defined as the inverse of the natural logarithm:

$y = \exp x \iff x = \ln y$


Then:

\(\displaystyle x\) \(=\) \(\displaystyle \ln y\) $\quad$ $\quad$
\(\displaystyle \) \(=\) \(\displaystyle \int_{t \mathop = 1}^{t \mathop = y} \frac 1 t \rd t\) $\quad$ Definition 1 of Natural Logarithm $\quad$
\(\displaystyle \leadsto \ \ \) \(\displaystyle D_y \left({x}\right)\) \(=\) \(\displaystyle D_y \int_{t \mathop = 1}^{t \mathop = y} \frac 1 t \rd t\) $\quad$ Differentiation with respect to $y$ $\quad$
\(\displaystyle \frac {\d x} {\d y}\) \(=\) \(\displaystyle \frac 1 y\) $\quad$ Fundamental Theorem of Calculus $\quad$
\(\displaystyle \iff \ \ \) \(\displaystyle \frac {\d y} {\d x}\) \(=\) \(\displaystyle y\) $\quad$ Derivative of Inverse Function $\quad$

This proves that $y$ is a solution of the differential equation.


It remains to be proven that $y$ fulfils the initial condition:

\(\displaystyle f \left({0}\right)\) \(=\) \(\displaystyle 1\) $\quad$ $\quad$
\(\displaystyle \iff \ \ \) \(\displaystyle f^{-1} \left({1}\right)\) \(=\) \(\displaystyle 0\) $\quad$ Image of Element under Inverse Mapping $\quad$
\(\displaystyle \ln y \Big \vert_{y \mathop = 1}\) \(=\) \(\displaystyle \int_{t \mathop = 1}^{t \mathop = 1} \frac 1 t \rd t\) $\quad$ $\quad$
\(\displaystyle \) \(=\) \(\displaystyle 0\) $\quad$ Integral on Zero Interval $\quad$

That is:

$\exp x$ is the solution of the differential equation:

$\dfrac {\d y} {\d x} = y$

satisfying the initial condition $f \left({0}\right) = 1$.

$\Box$


Solution of Differential Equation implies Inverse of Natural Logarithm

Let $\exp x$ be the real function defined as the solution of the differential equation:

$\dfrac {\d y} {\d x} = y$

satisfying the initial condition $f \left({0}\right) = 1$.


Thus:

\(\displaystyle \frac {\d y} {\d x}\) \(=\) \(\displaystyle y\) $\quad$ $\quad$
\(\displaystyle \leadsto \ \ \) \(\displaystyle \frac {\d x} {\d y}\) \(=\) \(\displaystyle \frac 1 y\) $\quad$ Derivative of Inverse Function $\quad$
\(\displaystyle \leadsto \ \ \) \(\displaystyle \int \rd x\) \(=\) \(\displaystyle \int \frac 1 y \rd y\) $\quad$ Separation of Variables $\quad$
\(\displaystyle \leadsto \ \ \) \(\displaystyle x + C\) \(=\) \(\displaystyle \int_{t \mathop = 1}^{t \mathop = y} \frac 1 t \rd t\) $\quad$ Fundamental Theorem of Calculus $\quad$
\(\displaystyle \) \(=\) \(\displaystyle \ln y\) $\quad$ Definition 1 of Natural Logarithm $\quad$


To solve for $C$, put $\left({x_0, y_0}\right) = \left({0, 1}\right)$:

\(\displaystyle 0 + C\) \(=\) \(\displaystyle \int_{t \mathop = 1}^{t \mathop = 1}\frac 1 t \rd t\) $\quad$ $\quad$
\(\displaystyle \leadsto \ \ \) \(\displaystyle C\) \(=\) \(\displaystyle 0\) $\quad$ Integral on Zero Interval $\quad$


That is:

$y = \exp x \iff x = \ln y$

$\blacksquare$


Also see