Documentation

Mathlib.RingTheory.PowerSeries.Trunc

Formal power series in one variable - Truncation #

PowerSeries.trunc n φ truncates a (univariate) formal power series to the polynomial that has the same coefficients as φ, for all m < n, and 0 otherwise.

def PowerSeries.trunc {R : Type u_1} [Semiring R] (n : ) (φ : PowerSeries R) :

The nth truncation of a formal power series to a polynomial

Equations
Instances For
    theorem PowerSeries.coeff_trunc {R : Type u_1} [Semiring R] (m : ) (n : ) (φ : PowerSeries R) :
    (PowerSeries.trunc n φ).coeff m = if m < n then (PowerSeries.coeff R m) φ else 0
    @[simp]
    theorem PowerSeries.trunc_zero {R : Type u_1} [Semiring R] (n : ) :
    @[simp]
    theorem PowerSeries.trunc_one {R : Type u_1} [Semiring R] (n : ) :
    @[simp]
    theorem PowerSeries.trunc_C {R : Type u_1} [Semiring R] (n : ) (a : R) :
    PowerSeries.trunc (n + 1) ((PowerSeries.C R) a) = Polynomial.C a
    @[simp]
    theorem PowerSeries.trunc_add {R : Type u_1} [Semiring R] (n : ) (φ : PowerSeries R) (ψ : PowerSeries R) :
    theorem PowerSeries.natDegree_trunc_lt {R : Type u_1} [Semiring R] (f : PowerSeries R) (n : ) :
    (PowerSeries.trunc (n + 1) f).natDegree < n + 1
    @[simp]
    theorem PowerSeries.degree_trunc_lt {R : Type u_1} [Semiring R] (f : PowerSeries R) (n : ) :
    (PowerSeries.trunc n f).degree < n
    theorem PowerSeries.eval₂_trunc_eq_sum_range {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] (s : S) (G : R →+* S) (n : ) (f : PowerSeries R) :
    Polynomial.eval₂ G s (PowerSeries.trunc n f) = iFinset.range n, G ((PowerSeries.coeff R i) f) * s ^ i
    @[simp]
    theorem PowerSeries.trunc_X {R : Type u_1} [Semiring R] (n : ) :
    PowerSeries.trunc (n + 2) PowerSeries.X = Polynomial.X
    theorem PowerSeries.trunc_X_of {R : Type u_1} [Semiring R] {n : } (hn : 2 n) :
    PowerSeries.trunc n PowerSeries.X = Polynomial.X
    @[simp]
    @[simp]
    @[simp]
    theorem PowerSeries.trunc_trunc_pow {R : Type u_2} [CommSemiring R] (f : PowerSeries R) (n : ) (a : ) :
    theorem PowerSeries.trunc_coe_eq_self {R : Type u_2} [CommSemiring R] {n : } {f : Polynomial R} (hn : f.natDegree < n) :
    theorem PowerSeries.coeff_coe_trunc_of_lt {R : Type u_2} [CommSemiring R] {n : } {m : } {f : PowerSeries R} (h : n < m) :

    The function coeff n : R⟦X⟧ → R is continuous. I.e. coeff n f depends only on a sufficiently long truncation of the power series f.

    theorem PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc₂ {R : Type u_2} [CommSemiring R] {n : } {a : } {b : } (f : PowerSeries R) (g : PowerSeries R) (ha : n < a) (hb : n < b) :

    The n-th coefficient of f*g may be calculated from the truncations of f and g.

    theorem PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc {R : Type u_2} [CommSemiring R] {d : } {n : } (f : PowerSeries R) (g : PowerSeries R) (h : d < n) :