Definition of well-known power series

In this file we define the following power series:

• PowerSeries.invUnitsSub: given u : Rˣ, this is the series for 1 / (u - x). It is given by ∑ n, x ^ n /ₚ u ^ (n + 1).

• PowerSeries.sin, PowerSeries.cos, PowerSeries.exp : power series for sin, cosine, and exponential functions.

def PowerSeries.invUnitsSub {R : Type u_1} [Ring R] (u : Rˣ) : PowerSeries R

The power series for 1 / (u - x).

Equations

• PowerSeries.invUnitsSub u = PowerSeries.mk fun (n : ℕ) => 1 /ₚ u ^ (n + 1)

@[simp]

theorem PowerSeries.coeff_invUnitsSub {R : Type u_1} [Ring R] (u : Rˣ) (n : ℕ) : (PowerSeries.coeff R n) (PowerSeries.invUnitsSub u) = 1 /ₚ u ^ (n + 1)

@[simp]

theorem PowerSeries.constantCoeff_invUnitsSub {R : Type u_1} [Ring R] (u : Rˣ) : (PowerSeries.constantCoeff R) (PowerSeries.invUnitsSub u) = 1 /ₚ u

@[simp]

theorem PowerSeries.invUnitsSub_mul_X {R : Type u_1} [Ring R] (u : Rˣ) : PowerSeries.invUnitsSub u * PowerSeries.X = PowerSeries.invUnitsSub u * (PowerSeries.C R) ↑u - 1

@[simp]

theorem PowerSeries.invUnitsSub_mul_sub {R : Type u_1} [Ring R] (u : Rˣ) : PowerSeries.invUnitsSub u * ((PowerSeries.C R) ↑u - PowerSeries.X) = 1

theorem PowerSeries.map_invUnitsSub {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) (u : Rˣ) : (PowerSeries.map f) (PowerSeries.invUnitsSub u) = PowerSeries.invUnitsSub ((Units.map ↑f) u)

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

Power series for the exponential function at zero.

Equations

• PowerSeries.exp A = PowerSeries.mk fun (n : ℕ) => (algebraMap ℚ A) (1 / ↑(Nat.factorial n))

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

Power series for the sine function at zero.

Equations

• PowerSeries.sin A = PowerSeries.mk fun (n : ℕ) => if Even n then 0 else (algebraMap ℚ A) ((-1) ^ (n / 2) / ↑(Nat.factorial n))

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

Power series for the cosine function at zero.

Equations

• PowerSeries.cos A = PowerSeries.mk fun (n : ℕ) => if Even n then (algebraMap ℚ A) ((-1) ^ (n / 2) / ↑(Nat.factorial n)) else 0

@[simp]

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

@[simp]

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

@[simp]

theorem PowerSeries.coeff_sin_bit0 {A : Type u_1} [Ring A] [Algebra ℚ A] (n : ℕ) : (PowerSeries.coeff A (bit0 n)) (PowerSeries.sin A) = 0

@[simp]

theorem PowerSeries.coeff_sin_bit1 {A : Type u_1} [Ring A] [Algebra ℚ A] (n : ℕ) : (PowerSeries.coeff A (bit1 n)) (PowerSeries.sin A) = (-1) ^ n * (PowerSeries.coeff A (bit1 n)) (PowerSeries.exp A)

@[simp]

theorem PowerSeries.coeff_cos_bit0 {A : Type u_1} [Ring A] [Algebra ℚ A] (n : ℕ) : (PowerSeries.coeff A (bit0 n)) (PowerSeries.cos A) = (-1) ^ n * (PowerSeries.coeff A (bit0 n)) (PowerSeries.exp A)

@[simp]

theorem PowerSeries.coeff_cos_bit1 {A : Type u_1} [Ring A] [Algebra ℚ A] (n : ℕ) : (PowerSeries.coeff A (bit1 n)) (PowerSeries.cos A) = 0

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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$.