Definition of well-known power series #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define the following power series:

power_series.inv_units_sub: given u : Rˣ, this is the series for 1 / (u - x). It is given by ∑ n, x ^ n /ₚ u ^ (n + 1).
power_series.sin, power_series.cos, power_series.exp : power series for sin, cosine, and exponential functions.

source

def power_series.inv_units_sub {R : Type u_1} [ring R] (u : Rˣ) :

power_series R

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

Equations

power_series.inv_units_sub u = power_series.mk (λ (n : ℕ), 1 /ₚ u ^ (n + 1))

source

@[simp]

theorem power_series.coeff_inv_units_sub {R : Type u_1} [ring R] (u : Rˣ) (n : ℕ) :

⇑(power_series.coeff R n) (power_series.inv_units_sub u) = 1 /ₚ u ^ (n + 1)

source

@[simp]

theorem power_series.constant_coeff_inv_units_sub {R : Type u_1} [ring R] (u : Rˣ) :

⇑(power_series.constant_coeff R) (power_series.inv_units_sub u) = 1 /ₚ u

source

@[simp]

theorem power_series.inv_units_sub_mul_X {R : Type u_1} [ring R] (u : Rˣ) :

power_series.inv_units_sub u * power_series.X = power_series.inv_units_sub u * ⇑(power_series.C R) ↑u - 1

source

@[simp]

theorem power_series.inv_units_sub_mul_sub {R : Type u_1} [ring R] (u : Rˣ) :

power_series.inv_units_sub u * (⇑(power_series.C R) ↑u - power_series.X) = 1

source

theorem power_series.map_inv_units_sub {R : Type u_1} {S : Type u_2} [ring R] [ring S] (f : R →+* S) (u : Rˣ) :

⇑(power_series.map f) (power_series.inv_units_sub u) = power_series.inv_units_sub (⇑(units.map ↑f) u)

source

def power_series.exp (A : Type u_1) [ring A] [algebra ℚ A] :

power_series A

Power series for the exponential function at zero.

Equations

power_series.exp A = power_series.mk (λ (n : ℕ), ⇑(algebra_map ℚ A) (1 / ↑(n.factorial)))

source

def power_series.sin (A : Type u_1) [ring A] [algebra ℚ A] :

power_series A

Power series for the sine function at zero.

Equations

power_series.sin A = power_series.mk (λ (n : ℕ), ite (even n) 0 (⇑(algebra_map ℚ A) ((-1) ^ (n / 2) / ↑(n.factorial))))

source

def power_series.cos (A : Type u_1) [ring A] [algebra ℚ A] :

power_series A

Power series for the cosine function at zero.

Equations

power_series.cos A = power_series.mk (λ (n : ℕ), ite (even n) (⇑(algebra_map ℚ A) ((-1) ^ (n / 2) / ↑(n.factorial))) 0)

source

@[simp]

theorem power_series.coeff_exp {A : Type u_1} [ring A] [algebra ℚ A] (n : ℕ) :

⇑(power_series.coeff A n) (power_series.exp A) = ⇑(algebra_map ℚ A) (1 / ↑(n.factorial))

source

@[simp]

theorem power_series.constant_coeff_exp {A : Type u_1} [ring A] [algebra ℚ A] :

⇑(power_series.constant_coeff A) (power_series.exp A) = 1

source

@[simp]

theorem power_series.coeff_sin_bit0 {A : Type u_1} [ring A] [algebra ℚ A] (n : ℕ) :

⇑(power_series.coeff A (bit0 n)) (power_series.sin A) = 0

source

@[simp]

theorem power_series.coeff_sin_bit1 {A : Type u_1} [ring A] [algebra ℚ A] (n : ℕ) :

⇑(power_series.coeff A (bit1 n)) (power_series.sin A) = (-1) ^ n * ⇑(power_series.coeff A (bit1 n)) (power_series.exp A)

source

@[simp]

theorem power_series.coeff_cos_bit0 {A : Type u_1} [ring A] [algebra ℚ A] (n : ℕ) :

⇑(power_series.coeff A (bit0 n)) (power_series.cos A) = (-1) ^ n * ⇑(power_series.coeff A (bit0 n)) (power_series.exp A)

source

@[simp]

theorem power_series.coeff_cos_bit1 {A : Type u_1} [ring A] [algebra ℚ A] (n : ℕ) :

⇑(power_series.coeff A (bit1 n)) (power_series.cos A) = 0

source

@[simp]

theorem power_series.map_exp {A : Type u_1} {A' : Type u_2} [ring A] [ring A'] [algebra ℚ A] [algebra ℚ A'] (f : A →+* A') :

⇑(power_series.map f) (power_series.exp A) = power_series.exp A'

source

@[simp]

theorem power_series.map_sin {A : Type u_1} {A' : Type u_2} [ring A] [ring A'] [algebra ℚ A] [algebra ℚ A'] (f : A →+* A') :

⇑(power_series.map f) (power_series.sin A) = power_series.sin A'

source

@[simp]

theorem power_series.map_cos {A : Type u_1} {A' : Type u_2} [ring A] [ring A'] [algebra ℚ A] [algebra ℚ A'] (f : A →+* A') :

⇑(power_series.map f) (power_series.cos A) = power_series.cos A'

source

theorem power_series.exp_mul_exp_eq_exp_add {A : Type u_1} [comm_ring A] [algebra ℚ A] (a b : A) :

⇑(power_series.rescale a) (power_series.exp A) * ⇑(power_series.rescale b) (power_series.exp A) = ⇑(power_series.rescale (a + b)) (power_series.exp A)

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

source

theorem power_series.exp_mul_exp_neg_eq_one {A : Type u_1} [comm_ring A] [algebra ℚ A] :

power_series.exp A * ⇑power_series.eval_neg_hom (power_series.exp A) = 1

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

source

theorem power_series.exp_pow_eq_rescale_exp {A : Type u_1} [comm_ring A] [algebra ℚ A] (k : ℕ) :

power_series.exp A ^ k = ⇑(power_series.rescale ↑k) (power_series.exp A)

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

source

theorem power_series.exp_pow_sum {A : Type u_1} [comm_ring A] [algebra ℚ A] (n : ℕ) :

(finset.range n).sum (λ (k : ℕ), power_series.exp A ^ k) = power_series.mk (λ (p : ℕ), (finset.range n).sum (λ (k : ℕ), ↑k ^ p * ⇑(algebra_map ℚ 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$.