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) : Polynomial R

The nth truncation of a formal power series to a polynomial

Equations

• PowerSeries.trunc n φ = ∑ m ∈ Finset.Ico 0 n, (Polynomial.monomial m) ((PowerSeries.coeff R m) φ)

theorem PowerSeries.coeff_trunc {R : Type u_1} [Semiring R] (m n : ℕ) (φ : PowerSeries R) : (trunc n φ).coeff m = if m < n then (coeff R m) φ else 0

@[simp]

theorem PowerSeries.trunc_zero {R : Type u_1} [Semiring R] (n : ℕ) : trunc n 0 = 0

@[simp]

theorem PowerSeries.trunc_one {R : Type u_1} [Semiring R] (n : ℕ) : trunc (n + 1) 1 = 1

@[simp]

theorem PowerSeries.trunc_C {R : Type u_1} [Semiring R] (n : ℕ) (a : R) : trunc (n + 1) ((C R) a) = Polynomial.C a

@[simp]

theorem PowerSeries.trunc_add {R : Type u_1} [Semiring R] (n : ℕ) (φ ψ : PowerSeries R) : trunc n (φ + ψ) = trunc n φ + trunc n ψ

theorem PowerSeries.trunc_succ {R : Type u_1} [Semiring R] (f : PowerSeries R) (n : ℕ) : trunc n.succ f = trunc n f + (Polynomial.monomial n) ((coeff R n) f)

theorem PowerSeries.natDegree_trunc_lt {R : Type u_1} [Semiring R] (f : PowerSeries R) (n : ℕ) : (trunc (n + 1) f).natDegree < n + 1

@[simp]

theorem PowerSeries.trunc_zero' {R : Type u_1} [Semiring R] {f : PowerSeries R} : trunc 0 f = 0

theorem PowerSeries.degree_trunc_lt {R : Type u_1} [Semiring R] (f : PowerSeries R) (n : ℕ) : (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 (trunc n f) = ∑ i ∈ Finset.range n, G ((coeff R i) f) * s ^ i

@[simp]

theorem PowerSeries.trunc_X {R : Type u_1} [Semiring R] (n : ℕ) : trunc (n + 2) X = Polynomial.X

theorem PowerSeries.trunc_X_of {R : Type u_1} [Semiring R] {n : ℕ} (hn : 2 ≤ n) : trunc n X = Polynomial.X

@[simp]

theorem PowerSeries.trunc_one_left {R : Type u_1} [Semiring R] (p : PowerSeries R) : trunc 1 p = Polynomial.C ((coeff R 0) p)

theorem PowerSeries.trunc_one_X {R : Type u_1} [Semiring R] : trunc 1 X = 0

@[simp]

theorem PowerSeries.trunc_C_mul {R : Type u_1} [Semiring R] (n : ℕ) (r : R) (f : PowerSeries R) : trunc n ((C R) r * f) = Polynomial.C r * trunc n f

@[simp]

theorem PowerSeries.trunc_mul_C {R : Type u_1} [Semiring R] (n : ℕ) (f : PowerSeries R) (r : R) : trunc n (f * (C R) r) = trunc n f * Polynomial.C r

theorem PowerSeries.trunc_trunc_of_le {R : Type u_2} [CommSemiring R] {n m : ℕ} (f : PowerSeries R) (hnm : n ≤ m := by rfl) : trunc n ↑(trunc m f) = trunc n f

@[simp]

theorem PowerSeries.trunc_trunc {R : Type u_2} [CommSemiring R] {n : ℕ} (f : PowerSeries R) : trunc n ↑(trunc n f) = trunc n f

@[simp]

theorem PowerSeries.trunc_trunc_mul {R : Type u_2} [CommSemiring R] {n : ℕ} (f g : PowerSeries R) : trunc n (↑(trunc n f) * g) = trunc n (f * g)

@[simp]

theorem PowerSeries.trunc_mul_trunc {R : Type u_2} [CommSemiring R] {n : ℕ} (f g : PowerSeries R) : trunc n (f * ↑(trunc n g)) = trunc n (f * g)

theorem PowerSeries.trunc_trunc_mul_trunc {R : Type u_2} [CommSemiring R] {n : ℕ} (f g : PowerSeries R) : trunc n (↑(trunc n f) * ↑(trunc n g)) = trunc n (f * g)

@[simp]

theorem PowerSeries.trunc_trunc_pow {R : Type u_2} [CommSemiring R] (f : PowerSeries R) (n a : ℕ) : trunc n (↑(trunc n f) ^ a) = trunc n (f ^ a)

theorem PowerSeries.trunc_coe_eq_self {R : Type u_2} [CommSemiring R] {n : ℕ} {f : Polynomial R} (hn : f.natDegree < n) : trunc n ↑f = f

theorem PowerSeries.coeff_coe_trunc_of_lt {R : Type u_2} [CommSemiring R] {n m : ℕ} {f : PowerSeries R} (h : n < m) : (coeff R n) ↑(trunc m f) = (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.

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

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

theorem PowerSeries.trunc_map {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (p : PowerSeries R) (n : ℕ) : trunc n ((map f) p) = Polynomial.map f (trunc n p)