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:

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

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


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

\(\displaystyle \map f 0\) \(=\) \(\displaystyle 1\)
\(\displaystyle \iff \ \ \) \(\displaystyle \map {f^{-1} } 1\) \(=\) \(\displaystyle 0\) Image of Element under Inverse Mapping
\(\displaystyle \bigintlimits {\ln y} {y \mathop = 1} {}\) \(=\) \(\displaystyle \int_{t \mathop = 1}^{t \mathop = 1} \frac 1 t \rd t\)
\(\displaystyle \) \(=\) \(\displaystyle 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:

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


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

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


That is:

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

$\blacksquare$