The exponential function is its own derivative
Builds on Exponential functionExponential of a sumDerivative
Statement
The exponential function is differentiable on , and for all real .
Remarks
By the sum rule, . The series gives as .
Term-by-term differentiation of the power series gives the same result.
The exponential function is the only solution of with . Mathlib states the derivative as Real.hasDerivAt_exp.
Reading path
To understand this page from the ground up, read these 32 pages in order. The foundations come first.
Show the path as a graph
- no evidence level
- Limit point of a set definition
- Sequence definition
- Limit of a function definition
- Real sequence definition
- Derivative definition
- Bounded sequence definition
- Geometric sequence definition
- Limit of a sequence definition
- Monotone sequence definition
- Series definition
- Sum of a finite geometric series statement
- Monotone convergence theorem for sequences statement
- Convergent sequence definition
- Squeeze theorem statement
- Cauchy product definition
- Partial sum definition
- Power series definition
- The sequence r^n tends to zero for |r| < 1 example
- Radius of convergence definition
- Convergent series definition
- A series of nonnegative terms converges iff its partial sums are bounded statement
- Absolute convergence definition
- Sum of a series definition
- Comparison test statement
- Geometric series example
- Cauchy product of absolutely convergent series statement
- Ratio test statement
- Ratio formula for the radius of convergence statement
- The exponential series has infinite radius of convergence statement
- Exponential function definition
- Exponential of a sum statement
- The exponential function is its own derivative statement
Where this leads
37 pages build on this one.
- Natural logarithm
- Euler–Mascheroni constant
- The logarithm grows slower than any power
- 1 + x is at most exp x
- Integral of exp(-x) over the half line
- log x is at most x - 1
- Inverse hyperbolic functions
- Harmonic numbers grow like log n
- Integral of the exponential function
- Power series of the exponential function
- Derivatives of the hyperbolic functions
- Derivative of the logarithm
- The exponential function is convex
- The gamma function extends the factorial
- Logarithm of a quotient
- Integral of 1/x
- Logarithm of a product
- The exponential function is strictly increasing
- Derivative of x^a
- Logarithm is the inverse of the exponential
- Real exponentiation
- Logarithm of a power
- Improper integral of x^p on an unbounded interval
- Integration by partial fractions
- Mercator series
- The logarithm is strictly concave
- Weierstrass product for the gamma function
- Bertrand's test
- Mertens' theorems
- Frullani integral
- Gauss's test
- Log-convexity of the gamma function
- Logarithmically convex function
- Bohr–Mollerup theorem
- An infinite product converges iff its series of logarithms converges
- Trigonometric integrals
- Barnes G-function
Further reading
- Web https://en.wikipedia.org/wiki/Exponential_function, Differential equation
About this page
| Tag | 0EX9GFJ0B3 |
|---|---|
| URI | m2://0EX9GFJ0B3 |
| Kind | statement, theorem |
| Writing | W0 stub |
| MSC | 33B10, 26A24 |
| Status | This copy of the site has no build data. Run m2 status 0EX9GFJ0B3. |
| Uses | Exponential function, Exponential of a sum, Derivative |
Markdown · JSON · Edit on GitHub
What this page needs for W1
- an inventory row: the row of the inventory that the node accounts for (0 of 1)
The writing levels say how complete the text of a page is. They do not measure its truth.