Binomial Power Series

We introduce formal power series of the form (1 + X) ^ r, where r is an element of a commutative binomial ring R.

Main Definitions

• PowerSeries.binomialSeries: A power series expansion of (1 + X) ^ r, where r is an element of a commutative binomial ring R.

Main Results

• PowerSeries.binomial_add: Adding exponents yields multiplication of series.
• PowerSeries.binomialSeries_nat: when r is a natural number, we get (1 + X) ^ r.
• PowerSeries.rescale_neg_one_invOneSubPow: The image of (1 - X) ^ (-d) under the map X ↦ (-X) is (1 + X) ^ (-d)

TODO

• When A is a commutative R-algebra, the exponentiation action makes the multiplicative group 1 + XA[[X]] into an R-module.

noncomputable def PowerSeries.binomialSeries {R : Type u_1} [CommRing R] [BinomialRing R] (A : Type u_3) [One A] [SMul R A] (r : R) : PowerSeries A

The power series for (1 + X) ^ r.

Equations

• PowerSeries.binomialSeries A r = PowerSeries.mk fun (n : ℕ) => Ring.choose r n • 1

@[simp]

theorem PowerSeries.binomialSeries_coeff {R : Type u_1} {A : Type u_2} [CommRing R] [BinomialRing R] [Semiring A] [SMul R A] (r : R) (n : ℕ) : (coeff A n) (binomialSeries A r) = Ring.choose r n • 1

@[simp]

theorem PowerSeries.binomialSeries_add {R : Type u_1} {A : Type u_2} [CommRing R] [BinomialRing R] [Semiring A] [Algebra R A] (r s : R) : binomialSeries A (r + s) = binomialSeries A r * binomialSeries A s

@[simp]

theorem PowerSeries.binomialSeries_nat {A : Type u_2} [CommRing A] (d : ℕ) : binomialSeries A ↑d = (1 + X) ^ d

theorem PowerSeries.rescale_neg_one_invOneSubPow {A : Type u_2} [CommRing A] (d : ℕ) : (rescale (-1)) ↑(invOneSubPow A d) = binomialSeries A (-↑d)