Documentation

Mathlib.RingTheory.PowerSeries.WellKnown

Definition of well-known power series #

In this file we define the following power series:

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 : ) :
    @[simp]
    theorem PowerSeries.invUnitsSub_mul_X {R : Type u_1} [Ring R] (u : Rˣ) :
    @[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.mk_one_mul_one_sub_eq_one {S : Type u_1} [CommRing S] :
    PowerSeries.mk 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} [CommRing S] (d : ) :
    PowerSeries.mk 1 ^ (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} [CommRing S] (d : ) :

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

    Equations
    Instances For
      theorem PowerSeries.invOneSubPow_val_eq_mk_choose_add {S : Type u_1} [CommRing S] (d : ) :
      (PowerSeries.invOneSubPow d) = PowerSeries.mk fun (n : ) => ((d + n).choose 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 d is equal to (1 - X)⁻¹ ^ (d + 1).

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

      Power series for the exponential function at zero.

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

        Power series for the sine function at zero.

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

          Power series for the cosine function at zero.

          Equations
          Instances For
            @[simp]
            theorem PowerSeries.coeff_exp {A : Type u_1} [Ring A] [Algebra A] (n : ) :
            (PowerSeries.coeff A n) (PowerSeries.exp A) = (algebraMap A) (1 / n.factorial)
            @[simp]
            theorem PowerSeries.map_exp {A : Type u_1} {A' : Type u_2} [Ring A] [Ring A'] [Algebra 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] [Algebra A'] (f : A →+* 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') :

            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$

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

            theorem PowerSeries.exp_pow_sum {A : Type u_1} [CommRing A] [Algebra A] (n : ) :
            kFinset.range n, PowerSeries.exp A ^ k = PowerSeries.mk fun (p : ) => kFinset.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$.