User:Keith.U/Exposition of the Natural Logarithm Function/Real

Preamble

The (real) natural logarithm function is a real function and is denoted $\ln$.

Approach 1: Integral Definition

Definition

$\ln: \R_{>0} \to \R$ can be defined by the following definite integral:

$\ln x := \ds \int_1^x \frac 1 t \rd t$

Approach 2: Inverse of $\exp$

Definition

$\ln: \R_{>0} \to \R$ can be defined as the inverse mapping of the natural exponential $\exp$, where $\exp$ is defined as:

$\ds \exp x := \sum_{n \mathop = 0}^\infty \frac {x^n} {n!} = \lim_{n \mathop \to \infty} \paren {1 + \frac x n}^n = e^x = $ "the unique solution to $D \exp = \exp \land \exp 0 = 1$"

Approach 3: Limit of Sequence

Definition

$\ln: \R_{>0} \to \R$ can be defined as the limit of the following sequence:

$\ln x := \ds \lim_{n \mathop \to \infty} n \paren {\sqrt [n] x - 1}$