Exponential of a sum
Builds on Exponential functionCauchy product of absolutely convergent series
Statement
For all real numbers and ,
Remarks
Multiply the two series by the Cauchy product. The binomial theorem gives .
In particular, .
So is a group homomorphism from to the multiplicative group . Mathlib states the formula as Real.exp_add.
Reading path
To understand this page from the ground up, read these 28 pages in order. The foundations come first.
Show the path as a graph
- no evidence level
- Sequence definition
- Real sequence 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
Where this leads
40 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 exponential function is its own derivative
- The gamma function extends the factorial
- Addition formulas for hyperbolic functions
- Logarithm of a quotient
- Integral of 1/x
- Logarithm of a product
- The exponential function is strictly increasing
- Derivative of x^a
- The exponential function is positive
- 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, Functional equation
About this page
| Tag | 0E8HNVBCSP |
|---|---|
| URI | m2://0E8HNVBCSP |
| Kind | statement, theorem |
| Writing | W0 stub |
| MSC | 33B10 |
| Status | This copy of the site has no build data. Run m2 status 0E8HNVBCSP. |
| Uses | Exponential function, Cauchy product of absolutely convergent series |
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.