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.

noncomputable def PowerSeries.trunc {R : Type u_1} [Semiring R] (n : ℕ) : PowerSeries R →ₗ[R] Polynomial R

The nth truncation of a formal power series to a polynomial.

theorem PowerSeries.trunc_apply {R : Type u_1} [Semiring R] (n : ℕ) (φ : PowerSeries R) : (trunc n) φ = ∑ m ∈ Finset.Ico 0 n, (Polynomial.monomial m) ((coeff m) φ)

theorem PowerSeries.coeff_trunc {R : Type u_1} [Semiring R] (m n : ℕ) (φ : PowerSeries R) : ((trunc n) φ).coeff m = if m < n then (coeff m) φ else 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 a) = Polynomial.C a

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 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 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 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 * 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) = (trunc n) f * Polynomial.C r

theorem PowerSeries.eq_shift_mul_X_pow_add_trunc {R : Type u_1} [Semiring R] (n : ℕ) (f : PowerSeries R) : f = (mk fun (i : ℕ) => (coeff (i + n)) f) * X ^ n + ↑((trunc n) f)

Split off the first n coefficients.

theorem PowerSeries.eq_X_pow_mul_shift_add_trunc {R : Type u_1} [Semiring R] (n : ℕ) (f : PowerSeries R) : f = (X ^ n * mk fun (i : ℕ) => (coeff (i + n)) f) + ↑((trunc n) f)

Split off the first n coefficients.

theorem PowerSeries.monomial_eq_C_mul_X_pow {R : Type u_1} [Semiring R] (r : R) (n : ℕ) : (monomial n) r = C r * X ^ n

@[simp]

theorem PowerSeries.trunc_X_pow_self_mul {R : Type u_1} [Semiring R] (n : ℕ) (p : PowerSeries R) : (trunc n) (X ^ n * p) = 0

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 n) ↑((trunc m) f) = (coeff 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 n) (f * g) = (coeff 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 d) (f * g) = (coeff d) (↑((trunc n) f) * ↑((trunc n) g))

@[simp]

theorem PowerSeries.trunc_sub {R : Type u_1} [Ring R] (n : ℕ) (φ ψ : PowerSeries R) : (trunc n) (φ - ψ) = (trunc n) φ - (trunc n) ψ

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)