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.invOneSubPow: given a commutative ring S and a number d : ℕ, PowerSeries.invOneSubPow d : S⟦X⟧ˣ is the power series ∑ n, Nat.choose (d + n) d whose multiplicative inverse is (1 - X) ^ (d + 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ˣ) :

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

Equations
Instances For
@[simp]
theorem PowerSeries.coeff_invUnitsSub {R : Type u_1} [Ring R] (u : Rˣ) (n : ) :
() = 1 /ₚ u ^ (n + 1)
@[simp]
theorem PowerSeries.constantCoeff_invUnitsSub {R : Type u_1} [Ring R] (u : Rˣ) :
= 1 /ₚ u
@[simp]
theorem PowerSeries.invUnitsSub_mul_X {R : Type u_1} [Ring R] (u : Rˣ) :
* PowerSeries.X = - 1
@[simp]
theorem PowerSeries.invUnitsSub_mul_sub {R : Type u_1} [Ring R] (u : 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ˣ) :
theorem PowerSeries.mk_one_mul_one_sub_eq_one {S : Type u_1} [] :
* (1 - PowerSeries.X) = 1

(1 + X + X^2 + ...) * (1 - X) = 1.

Note that the power series 1 + X + X^2 + ... is written as mk 1 where 1 is the constant function so that mk 1 is the power series with all coefficients equal to one.

theorem PowerSeries.mk_one_pow_eq_mk_choose_add {S : Type u_1} [] (d : ) :
^ (d + 1) = PowerSeries.mk fun (n : ) => ((d + n).choose d)

Note that mk 1 is the constant function 1 so the power series 1 + X + X^2 + .... This theorem states that for any d : ℕ, (1 + X + X^2 + ... : S⟦X⟧) ^ (d + 1) is equal to the power series mk fun n => Nat.choose (d + n) d : S⟦X⟧.

noncomputable def PowerSeries.invOneSubPow {S : Type u_1} [] (d : ) :
()ˣ

The power series mk fun n => Nat.choose (d + n) d, whose multiplicative inverse is (1 - X) ^ (d + 1).

Equations
• = { val := PowerSeries.mk fun (n : ) => ((d + n).choose d), inv := (1 - PowerSeries.X) ^ (d + 1), val_inv := , inv_val := }
Instances For
theorem PowerSeries.invOneSubPow_val_eq_mk_choose_add {S : Type u_1} [] (d : ) :
= PowerSeries.mk fun (n : ) => ((d + n).choose d)
theorem PowerSeries.invOneSubPow_eq_inv_one_sub_pow {S : Type u_1} [] (d : ) :
= (Units.mkOfMulEqOne (1 - PowerSeries.X) () )⁻¹ ^ (d + 1)

The theorem PowerSeries.mk_one_mul_one_sub_eq_one implies that 1 - X is a unit in S⟦X⟧ whose inverse is the power series 1 + X + X^2 + .... This theorem states that for any d : ℕ, PowerSeries.invOneSubPow d is equal to (1 - X)⁻¹ ^ (d + 1).

theorem PowerSeries.invOneSubPow_inv_eq_one_sub_pow {S : Type u_1} [] (d : ) :
.inv = (1 - PowerSeries.X) ^ (d + 1)
def PowerSeries.exp (A : Type u_1) [Ring A] [] :

Power series for the exponential function at zero.

Equations
Instances For
def PowerSeries.sin (A : Type u_1) [Ring A] [] :

Power series for the sine function at zero.

Equations
Instances For
def PowerSeries.cos (A : Type u_1) [Ring A] [] :

Power series for the cosine function at zero.

Equations
Instances For
@[simp]
theorem PowerSeries.coeff_exp {A : Type u_1} [Ring A] [] (n : ) :
() () = () (1 / n.factorial)
@[simp]
theorem PowerSeries.constantCoeff_exp {A : Type u_1} [Ring A] [] :
@[simp]
theorem PowerSeries.coeff_sin_bit0 {A : Type u_1} [Ring A] [] (n : ) :
() () = 0
@[simp]
theorem PowerSeries.coeff_sin_bit1 {A : Type u_1} [Ring A] [] (n : ) :
() () = (-1) ^ n * () ()
@[simp]
theorem PowerSeries.coeff_cos_bit0 {A : Type u_1} [Ring A] [] (n : ) :
() () = (-1) ^ n * () ()
@[simp]
theorem PowerSeries.coeff_cos_bit1 {A : Type u_1} [Ring A] [] (n : ) :
() () = 0
@[simp]
theorem PowerSeries.map_exp {A : Type u_1} {A' : Type u_2} [Ring A] [Ring A'] [] [Algebra A'] (f : A →+* A') :
() () =
@[simp]
theorem PowerSeries.map_sin {A : Type u_1} {A' : Type u_2} [Ring A] [Ring A'] [] [Algebra A'] (f : A →+* A') :
() () =
@[simp]
theorem PowerSeries.map_cos {A : Type u_1} {A' : Type u_2} [Ring A] [Ring A'] [] [Algebra A'] (f : A →+* A') :
() () =
theorem PowerSeries.exp_mul_exp_eq_exp_add {A : Type u_1} [] [] (a : A) (b : A) :
* = (PowerSeries.rescale (a + b)) ()

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

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

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

theorem PowerSeries.exp_pow_eq_rescale_exp {A : Type u_1} [] [] (k : ) :
= () ()

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

theorem PowerSeries.exp_pow_sum {A : Type u_1} [] [] (n : ) :
(().sum fun (k : ) => ) = PowerSeries.mk fun (p : ) => ().sum fun (k : ) => k ^ p * () (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$.