Real Exponentiation#
The Real Exponential Function#
Theorem: The Real Exponential Function
The real power series \(\displaystyle \sum_{n = 0}^\infty \frac{x^n}{n!}\) converges for all \(x \in \mathbb{R}\).
Proof
TODO
Definition: The Real Exponential Function
The real exponential function is the real analytic function \(\exp: \mathbb{R} \to \mathbb{R}\) defined by this real power series.
Notation
Theorem: Image of the Real Exponential Function
The image of the real exponential function is the open interval \((0;+\infty)\).
Proof
TODO
Theorem: Monotony of the Real Exponential Function
The real exponential function is strictly increasing.
Proof
TODO
Addition Theorem for the Real Exponential Function
The real exponential function has the following property for all \(x,y \in \mathbb{R}\):
Proof
TODO
Theorem: Derivative of the Real Exponential Function
The real exponential function is differentiable with
Proof
TODO
Theorem: Antiderivatives of the Real Exponential Function and Variations
The real exponential function \(e^{x}\) is antidifferentiable on \(\mathbb{R}\):
The function \(\mathrm{e}^{\alpha x}\) is antidifferentiable on \(\mathbb{R}\) for all \(\alpha \ne 0\):
If a real function \(f\) is differentiable on some open interval \(I\), then \(f'(x)\mathrm{e}^{f(x)}\) is antidifferentiable on \(I\):
If a real function \(f\) is differentiable on some open interval \(I\), then \(\mathrm{e}^x(f(x) + f'(x))\) is antidifferentiable on \(I\):
Proof
TODO
Theorem: The Real Exponential through Convergent Sequences
The real exponential function \(e^x\) is equal to the limit of the following real sequence:
Proof
TODO
Theorem: Real Exponentiation in Bachmann-Landau
The real exponential \(\mathrm{e}^x\) can be expressed in Bachmann-Landau notation for \(x \to 0\) as follows:
Proof
TODO
Exponentiation#
Definition: Exponentiation
Let \(a\) and \(b\) be real numbers.
We define the exponentiation \(a^b\) as
Theorem: Antidifferentiability of Exponentiation
The exponential \(a^x\) is antidifferentiable on \(\mathbb{R}\) for all \(a \gt 0\) and for \(a \ne 1\) its antiderivatives can be constructed via the real natural logarithm:
Proof
TODO