Exponential Power Series

This file defines the exponential power series exp A = ∑ Xⁿ/n! over ℚ-algebras and develops its key properties, including the fundamental differential equation (exp A)' = exp A, a uniqueness characterization, and the functional equation for multiplication.

Main definitions

• PowerSeries.exp: The exponential power series exp A = ∑ Xⁿ/n! over a ℚ-algebra A.

Main results

• PowerSeries.coeff_exp: The coefficient of exp A at n is 1/n!.
• PowerSeries.constantCoeff_exp: The constant term of exp A is 1.
• PowerSeries.map_exp: exp is preserved by ring homomorphisms between ℚ-algebras.
• PowerSeries.derivative_exp: The derivative of exp equals exp: d⁄dX A (exp A) = exp A.
• PowerSeries.exp_unique_of_derivative_eq_self: A power series with derivative equal to itself and constant term 1 must be exp.
• PowerSeries.isUnit_exp: exp A is a unit (invertible).
• PowerSeries.order_exp: The order of exp A is 0.
• PowerSeries.exp_mul_exp_eq_exp_add: The functional equation e^{aX} * e^{bX} = e^{(a+b)X}.
• PowerSeries.exp_mul_exp_neg_eq_one: The identity e^X * e^{-X} = 1.
• PowerSeries.exp_pow_eq_rescale_exp: Powers of exp satisfy (e^X)^k = e^{kX}.
• PowerSeries.exp_pow_sum: Formula for the sum of powers of exp.

def PowerSeries.exp (A : Type u_1) [Ring A] [Algebra ℚ A] : PowerSeries A

Power series for the exponential function at zero.

@[simp]

theorem PowerSeries.coeff_exp {A : Type u_1} [Ring A] [Algebra ℚ A] (n : ℕ) : (coeff n) (exp A) = (algebraMap ℚ A) (1 / ↑n.factorial)

@[simp]

theorem PowerSeries.constantCoeff_exp {A : Type u_1} [Ring A] [Algebra ℚ A] : constantCoeff (exp A) = 1

@[simp]

theorem PowerSeries.map_exp {A : Type u_1} {A' : Type u_2} [Ring A] [Ring A'] [Algebra ℚ A] [Algebra ℚ A'] (f : A →+* A') : (map f) (exp A) = exp A'

Derivative of exp

theorem PowerSeries.derivative_exp (A : Type u_3) [CommRing A] [Algebra ℚ A] : (derivative A) (exp A) = exp A

Uniqueness characterization

theorem PowerSeries.exp_unique_of_derivative_eq_self {A : Type u_3} [CommRing A] [Algebra ℚ A] [IsAddTorsionFree A] {f : PowerSeries A} (hd : (derivative A) f = f) (hc : constantCoeff f = 1) : f = exp A

A power series with derivative equal to itself and constant term 1 must be exp.

The proof uses induction on coefficients: if f' = f and f(0) = 1, then coeff (n+1) f * (n+1) = coeff n f, which determines all coefficients uniquely.

Order and invertibility

theorem PowerSeries.isUnit_exp (A : Type u_4) [Ring A] [Algebra ℚ A] : IsUnit (exp A)

@[simp]

theorem PowerSeries.order_exp (A : Type u_4) [Ring A] [Algebra ℚ A] [Nontrivial A] : (exp A).order = 0

theorem PowerSeries.exp_mul_exp_eq_exp_add {A : Type u_4} [CommRing A] [Algebra ℚ A] (a b : A) : (rescale a) (exp A) * (rescale b) (exp A) = (rescale (a + b)) (exp A)

Shows that $e^{aX} * e^{bX} = e^{(a + b)X}$

theorem PowerSeries.exp_mul_exp_neg_eq_one {A : Type u_4} [CommRing A] [Algebra ℚ A] : exp A * evalNegHom (exp A) = 1

Shows that $e^{x} * e^{-x} = 1$

theorem PowerSeries.exp_pow_eq_rescale_exp {A : Type u_4} [CommRing A] [Algebra ℚ A] (k : ℕ) : exp A ^ k = (rescale ↑k) (exp A)

Shows that $(e^{X})^k = e^{kX}$.

theorem PowerSeries.exp_pow_sum {A : Type u_4} [CommRing A] [Algebra ℚ A] (n : ℕ) : ∑ k ∈ Finset.range n, exp A ^ k = mk fun (p : ℕ) => ∑ k ∈ Finset.range n, ↑k ^ p * (algebraMap ℚ A) (↑p.factorial)⁻¹

Shows that $\sum_{k = 0}^{n - 1} (e^{X})^k = \sum_{p = 0}^{\infty} \sum_{k = 0}^{n - 1} \frac{k^p}{p!}X^p$.