Equivalence of Definitions of Real Exponential Function/Inverse of Natural Logarithm equivalent to Differential Equation

From ProofWiki
Jump to navigation Jump to search

Theorem

The following definitions of the concept of real exponential function are equivalent:

As the Inverse of the Natural Logarithm

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

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 = \map f x$ to the first order ODE:

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

satisfying the initial condition $\map f 0 = 1$.


Proof

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:

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

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


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

\(\ds \map f 0\) \(=\) \(\ds 1\)
\(\ds \leadstoandfrom \ \ \) \(\ds \map {f^{-1} } 1\) \(=\) \(\ds 0\) Image of Element under Inverse Mapping
\(\ds \bigintlimits {\ln y} {y \mathop = 1} {}\) \(=\) \(\ds \int_{t \mathop = 1}^{t \mathop = 1} \frac 1 t \rd t\)
\(\ds \) \(=\) \(\ds 0\) Integral on Zero Interval

That is:

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

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

satisfying the initial condition $\map f 0 = 1$.

$\Box$


Solution of Differential Equation implies Inverse of Natural Logarithm

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

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

satisfying the initial condition $\map f = 1$.


Thus:

\(\ds \frac {\d y} {\d x}\) \(=\) \(\ds y\)
\(\ds \leadsto \ \ \) \(\ds \frac {\d x} {\d y}\) \(=\) \(\ds \frac 1 y\) Derivative of Inverse Function
\(\ds \leadsto \ \ \) \(\ds \int \rd x\) \(=\) \(\ds \int \frac 1 y \rd y\) Solution to Separable Differential Equation
\(\ds \leadsto \ \ \) \(\ds x + C\) \(=\) \(\ds \int_{t \mathop = 1}^{t \mathop = y} \frac 1 t \rd t\) Fundamental Theorem of Calculus
\(\ds \) \(=\) \(\ds \ln y\) Definition 1 of Natural Logarithm


To solve for $C$, put $\tuple {x_0, y_0} = \tuple {0, 1}$:

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


That is:

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

$\blacksquare$