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.

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

The nth truncation of a formal power series to a polynomial

Equations
Instances For
    source
    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
    source
    @[simp]
    theorem PowerSeries.trunc_zero {R : Type u_1} [Semiring R] (n : ℕ) :
    PowerSeries.trunc n 0 = 0
    source
    @[simp]
    theorem PowerSeries.trunc_one {R : Type u_1} [Semiring R] (n : ℕ) :
    PowerSeries.trunc (n + 1) 1 = 1
    source
    @[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
    source
    @[simp]
    theorem PowerSeries.trunc_add {R : Type u_1} [Semiring R] (n : ℕ) (φ : PowerSeries R) (ψ : PowerSeries R) :
    PowerSeries.trunc n (φ + ψ) = PowerSeries.trunc n φ + PowerSeries.trunc n ψ
    source
    theorem PowerSeries.trunc_succ {R : Type u_1} [Semiring R] (f : PowerSeries R) (n : ℕ) :
    PowerSeries.trunc n.succ f = PowerSeries.trunc n f + (Polynomial.monomial n) ((PowerSeries.coeff R n) f)
    source
    theorem PowerSeries.natDegree_trunc_lt {R : Type u_1} [Semiring R] (f : PowerSeries R) (n : ℕ) :
    (PowerSeries.trunc (n + 1) f).natDegree < n + 1
    source
    @[simp]
    theorem PowerSeries.trunc_zero' {R : Type u_1} [Semiring R] {f : PowerSeries R} :
    PowerSeries.trunc 0 f = 0
    source
    theorem PowerSeries.degree_trunc_lt {R : Type u_1} [Semiring R] (f : PowerSeries R) (n : ℕ) :
    (PowerSeries.trunc n f).degree < ↑n
    source
    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) = (Finset.range n).sum fun (i : ℕ) => G ((PowerSeries.coeff R i) f) * s ^ i
    source
    @[simp]
    theorem PowerSeries.trunc_X {R : Type u_1} [Semiring R] (n : ℕ) :
    PowerSeries.trunc (n + 2) PowerSeries.X = Polynomial.X
    source
    theorem PowerSeries.trunc_X_of {R : Type u_1} [Semiring R] {n : ℕ} (hn : 2 ≤ n) :
    PowerSeries.trunc n PowerSeries.X = Polynomial.X
    source
    theorem PowerSeries.trunc_trunc_of_le {R : Type u_2} [CommSemiring R] {n : ℕ} {m : ℕ} (f : PowerSeries R) (hnm : autoParam (n ≤ m) _auto✝) :
    PowerSeries.trunc n ↑(PowerSeries.trunc m f) = PowerSeries.trunc n f
    source
    @[simp]
    theorem PowerSeries.trunc_trunc {R : Type u_2} [CommSemiring R] {n : ℕ} (f : PowerSeries R) :
    PowerSeries.trunc n ↑(PowerSeries.trunc n f) = PowerSeries.trunc n f
    source
    @[simp]
    theorem PowerSeries.trunc_trunc_mul {R : Type u_2} [CommSemiring R] {n : ℕ} (f : PowerSeries R) (g : PowerSeries R) :
    PowerSeries.trunc n (↑(PowerSeries.trunc n f) * g) = PowerSeries.trunc n (f * g)
    source
    @[simp]
    theorem PowerSeries.trunc_mul_trunc {R : Type u_2} [CommSemiring R] {n : ℕ} (f : PowerSeries R) (g : PowerSeries R) :
    PowerSeries.trunc n (f * ↑(PowerSeries.trunc n g)) = PowerSeries.trunc n (f * g)
    source
    theorem PowerSeries.trunc_trunc_mul_trunc {R : Type u_2} [CommSemiring R] {n : ℕ} (f : PowerSeries R) (g : PowerSeries R) :
    PowerSeries.trunc n (↑(PowerSeries.trunc n f) * ↑(PowerSeries.trunc n g)) = PowerSeries.trunc n (f * g)
    source
    @[simp]
    theorem PowerSeries.trunc_trunc_pow {R : Type u_2} [CommSemiring R] (f : PowerSeries R) (n : ℕ) (a : ℕ) :
    PowerSeries.trunc n (↑(PowerSeries.trunc n f) ^ a) = PowerSeries.trunc n (f ^ a)
    source
    theorem PowerSeries.trunc_coe_eq_self {R : Type u_2} [CommSemiring R] {n : ℕ} {f : Polynomial R} (hn : f.natDegree < n) :
    PowerSeries.trunc n ↑f = f
    source
    theorem PowerSeries.coeff_coe_trunc_of_lt {R : Type u_2} [CommSemiring R] {n : ℕ} {m : ℕ} {f : PowerSeries R} (h : n < m) :
    (PowerSeries.coeff R n) ↑(PowerSeries.trunc m f) = (PowerSeries.coeff R n) f

    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.

    source
    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) :
    (PowerSeries.coeff R n) (f * g) = (PowerSeries.coeff R n) (↑(PowerSeries.trunc a f) * ↑(PowerSeries.trunc b g))

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

    source
    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) :
    (PowerSeries.coeff R d) (f * g) = (PowerSeries.coeff R d) (↑(PowerSeries.trunc n f) * ↑(PowerSeries.trunc n g))