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 S d is the multiplicative inverse of (1 - X) ^ d in S⟦X⟧ˣ. When d is 0, PowerSeries.invOneSubPow S d will just be 1. When d is positive, PowerSeries.invOneSubPow S d will be ∑ n, Nat.choose (d - 1 + n) (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ˣ) : PowerSeries R

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem PowerSeries.mk_one_mul_one_sub_eq_one (S : Type u_1) [CommRing S] : mk 1 * (1 - 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) [CommRing S] (d : ℕ) : mk 1 ^ (d + 1) = 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) [CommRing S] : ℕ → (PowerSeries S)ˣ

Given a natural number d : ℕ and a commutative ring S, PowerSeries.invOneSubPow S d is the multiplicative inverse of (1 - X) ^ d in S⟦X⟧ˣ. When d is 0, PowerSeries.invOneSubPow S d will just be 1. When d is positive, PowerSeries.invOneSubPow S d will be the power series mk fun n => Nat.choose (d - 1 + n) (d - 1).

theorem PowerSeries.invOneSubPow_zero (S : Type u_1) [CommRing S] : invOneSubPow S 0 = 1

theorem PowerSeries.invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos (S : Type u_1) [CommRing S] (d : ℕ) (h : 0 < d) : ↑(invOneSubPow S d) = mk fun (n : ℕ) => ↑((d - 1 + n).choose (d - 1))

theorem PowerSeries.invOneSubPow_val_succ_eq_mk_add_choose (S : Type u_1) [CommRing S] (d : ℕ) : ↑(invOneSubPow S (d + 1)) = mk fun (n : ℕ) => ↑((d + n).choose d)

theorem PowerSeries.invOneSubPow_val_one_eq_invUnitSub_one (S : Type u_1) [CommRing S] : ↑(invOneSubPow S 1) = invUnitsSub 1

theorem PowerSeries.invOneSubPow_eq_inv_one_sub_pow (S : Type u_1) [CommRing S] (d : ℕ) : invOneSubPow S d = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ d

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 S d is equal to (1 - X)⁻¹ ^ d.

theorem PowerSeries.invOneSubPow_inv_eq_one_sub_pow (S : Type u_1) [CommRing S] (d : ℕ) : (invOneSubPow S d).inv = (1 - X) ^ d

theorem PowerSeries.invOneSubPow_inv_zero_eq_one (S : Type u_1) [CommRing S] : (invOneSubPow S 0).inv = 1

theorem PowerSeries.mk_add_choose_mul_one_sub_pow_eq_one (S : Type u_1) [CommRing S] (d : ℕ) : (mk fun (n : ℕ) => ↑((d + n).choose d)) * (1 - X) ^ (d + 1) = 1

theorem PowerSeries.invOneSubPow_add (S : Type u_1) [CommRing S] (d e : ℕ) : invOneSubPow S (d + e) = invOneSubPow S d * invOneSubPow S e

theorem PowerSeries.one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val (S : Type u_1) [CommRing S] (d e : ℕ) : (1 - X) ^ e * ↑(invOneSubPow S (d + e)) = ↑(invOneSubPow S d)

theorem PowerSeries.one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow (S : Type u_1) [CommRing S] (d e : ℕ) : (1 - X) ^ (d + e) * ↑(invOneSubPow S e) = (1 - X) ^ d

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

Power series for the exponential function at zero.

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

Power series for the sine function at zero.

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

Power series for the cosine function at zero.

@[simp]

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

@[simp]

theorem PowerSeries.constantCoeff_exp {A : Type u_1} [Ring A] [Algebra ℚ A] : (constantCoeff A) (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'

@[simp]

theorem PowerSeries.map_sin {A : Type u_1} {A' : Type u_2} [Ring A] [Ring A'] [Algebra ℚ A] [Algebra ℚ A'] (f : A →+* A') : (map f) (sin A) = 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') : (map f) (cos A) = cos A'

theorem PowerSeries.exp_mul_exp_eq_exp_add {A : Type u_1} [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_1} [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_1} [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_1} [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$.