Truncations and finite expansions of power series

This file collects facts used to compare power series to a finite order m:

• the truncation trunc m φ vanishes exactly when φ has order at least m,
• two power series have equal m-truncations if and only if their coefficients agree below m,
• the m-truncations of inv.aux a φ, invOfUnit φ u, φ⁻¹, integer powers u ^ k, and products (u ^ k) * d⁄dX u of a unit u : R⟦X⟧ˣ depend only on a finite truncation of the input,
• the coefficients of a finite expansion ∑_{i < m} aᵢ Xⁱ are the aᵢ, read as zero from degree m on,
• the coefficients of a polynomial times a power series expand along the polynomial monomials, and
• evaluating the n-truncation at an element with x ^ n = 0 sees only the coefficients below n.

Main results

• PowerSeries.trunc_eq_zero_iff_le_order: trunc m φ = 0 ↔ m ≤ order φ.
• PowerSeries.trunc_eq_trunc_iff: trunc m φ = trunc m ψ ↔ ∀ n < m, coeff n φ = coeff n ψ.
• PowerSeries.coe_trunc_eq_self_of_coeff_eq_zero: a series vanishing from degree m on is its m-truncation.
• PowerSeries.trunc_inv_aux_eq_of_trunc_eq, PowerSeries.trunc_invOfUnit_eq_of_trunc_eq, PowerSeries.trunc_inv_eq_of_trunc_eq, PowerSeries.trunc_val_inv_eq_of_trunc_eq: the m-th truncation of an inverse power series depends only on trunc m.
• PowerSeries.trunc_val_zpow_eq_of_trunc_eq and PowerSeries.trunc_val_zpow_mul_derivative_eq_of_trunc_eq: the finite jets of u ^ k and (u ^ k) * d⁄dX u for a unit u : R⟦X⟧ˣ depend only on trunc m u and trunc (m + 1) u.
• PowerSeries.coeff_sum_C_mul_X_pow: the coefficients of ∑ i : Fin m, C (a i) * X ^ i.
• PowerSeries.coeff_coe_mul_eq_sum: coeff n (p * g) = ∑_{i < N} pᵢ coeff n (Xⁱ g) for a polynomial p of degree less than N.
• PowerSeries.aeval_trunc_eq_aeval_of_pow_eq_zero: at an element with a vanishing nth power, the truncation below n evaluates like any polynomial with the same coefficients below n.

theorem PowerSeries.trunc_eq_zero_iff_le_order {R : Type u_1} [Semiring R] {m : ℕ} {φ : PowerSeries R} : (trunc m) φ = 0 ↔ ↑m ≤ φ.order

The truncation below degree m of a power series vanishes exactly when the series has order at least m.

theorem PowerSeries.coeff_eq_of_trunc_eq {R : Type u_1} [Semiring R] {n m : ℕ} {φ ψ : PowerSeries R} (h : (trunc m) φ = (trunc m) ψ) (hn : n < m) : (coeff n) φ = (coeff n) ψ

Two power series with the same m-truncation have the same n-th coefficient for every n < m.

theorem PowerSeries.trunc_eq_trunc_iff {R : Type u_1} [Semiring R] {m : ℕ} {φ ψ : PowerSeries R} : (trunc m) φ = (trunc m) ψ ↔ ∀ n < m, (coeff n) φ = (coeff n) ψ

Two power series have the same m-truncation if and only if their coefficients agree in all degrees < m.

theorem PowerSeries.coe_trunc_eq_self_of_coeff_eq_zero {R : Type u_1} [Semiring R] {m : ℕ} {φ : PowerSeries R} (h : ∀ (n : ℕ), m ≤ n → (coeff n) φ = 0) : ↑((trunc m) φ) = φ

A power series whose coefficients vanish from degree m on is its m-truncation.

theorem PowerSeries.trunc_eq_of_trunc_eq_of_le {R : Type u_1} [Semiring R] {n m : ℕ} {φ ψ : PowerSeries R} (h : (trunc m) φ = (trunc m) ψ) (hnm : n ≤ m) : (trunc n) φ = (trunc n) ψ

Equality of truncations at m implies equality of truncations at any n ≤ m.

theorem PowerSeries.trunc_mul_eq_of_trunc_eq {R : Type u_1} [Semiring R] {m : ℕ} {f₁ f₂ g₁ g₂ : PowerSeries R} (hf : (trunc m) f₁ = (trunc m) f₂) (hg : (trunc m) g₁ = (trunc m) g₂) : (trunc m) (f₁ * g₁) = (trunc m) (f₂ * g₂)

The m-truncation of a product depends only on the m-truncations of the factors.

theorem PowerSeries.trunc_pow_eq_of_trunc_eq {R : Type u_1} [Semiring R] {m : ℕ} {f g : PowerSeries R} (h : (trunc m) f = (trunc m) g) (k : ℕ) : (trunc m) (f ^ k) = (trunc m) (g ^ k)

The m-truncation of a power depends only on the m-truncation of the base.

theorem PowerSeries.coeff_sum_C_mul_X_pow {R : Type u_1} [Semiring R] {m : ℕ} (a : Fin m → R) (n : ℕ) : (coeff n) (∑ i : Fin m, C (a i) * X ^ ↑i) = if h : n < m then a ⟨n, h⟩ else 0

The coefficients of the finite expansion ∑_{i < m} aᵢ Xⁱ are the aᵢ, and vanish from degree m on.

theorem PowerSeries.coeff_coe_mul_eq_sum {R : Type u_1} [Semiring R] (p : Polynomial R) (g : PowerSeries R) {N : ℕ} (hN : p.natDegree < N) (n : ℕ) : (coeff n) (↑p * g) = ∑ i ∈ Finset.range N, p.coeff i * (coeff n) (X ^ i * g)

The coefficients of the product of a polynomial p and a power series g, expanded along the monomials of p below any bound N on its degree.

theorem PowerSeries.coeff_inv_aux_eq_of_trunc_eq {R : Type u_1} [Ring R] {n m : ℕ} (a : R) {φ ψ : PowerSeries R} (h : (trunc m) φ = (trunc m) ψ) (hn : n < m) : (coeff n) (inv.aux a φ) = (coeff n) (inv.aux a ψ)

For n < m, the n-th coefficient of PowerSeries.inv.aux a φ depends only on trunc m φ.

theorem PowerSeries.trunc_inv_aux_eq_of_trunc_eq {R : Type u_1} [Ring R] {m : ℕ} (a : R) {φ ψ : PowerSeries R} (h : (trunc m) φ = (trunc m) ψ) : (trunc m) (inv.aux a φ) = (trunc m) (inv.aux a ψ)

The m-truncation of PowerSeries.inv.aux a φ depends only on trunc m φ.

theorem PowerSeries.trunc_invOfUnit_eq_of_trunc_eq {R : Type u_1} [Ring R] {m : ℕ} {φ ψ : PowerSeries R} (u : Rˣ) (h : (trunc m) φ = (trunc m) ψ) : (trunc m) (φ.invOfUnit u) = (trunc m) (ψ.invOfUnit u)

The m-truncation of invOfUnit φ u depends only on trunc m φ.

theorem PowerSeries.trunc_val_inv_eq_of_trunc_eq {R : Type u_1} [Ring R] {m : ℕ} {u v : (PowerSeries R)ˣ} (h : (trunc m) ↑u = (trunc m) ↑v) : (trunc m) ↑u⁻¹ = (trunc m) ↑v⁻¹

The m-truncation of the inverse of a unit power series depends only on the m-truncation of the unit.

theorem PowerSeries.trunc_val_zpow_eq_of_trunc_eq {R : Type u_1} [Ring R] {m : ℕ} {u v : (PowerSeries R)ˣ} (h : (trunc m) ↑u = (trunc m) ↑v) (k : ℤ) : (trunc m) ↑(u ^ k) = (trunc m) ↑(v ^ k)

The m-truncation of an integer power u ^ k of a unit u : R⟦X⟧ˣ depends only on trunc m u.

theorem PowerSeries.trunc_val_zpow_mul_derivative_eq_of_trunc_eq {R : Type u_1} [CommRing R] {m : ℕ} {u v : (PowerSeries R)ˣ} (h : (trunc (m + 1)) ↑u = (trunc (m + 1)) ↑v) (k : ℤ) : (trunc m) (↑(u ^ k) * derivative ↑u) = (trunc m) (↑(v ^ k) * derivative ↑v)

The m-truncation of (u ^ k) * d⁄dX u for a unit u : R⟦X⟧ˣ depends only on trunc (m + 1) u.

theorem PowerSeries.aeval_trunc_eq_aeval_of_pow_eq_zero {R : Type u_1} [CommRing R] {A : Type u_2} [Ring A] [Algebra R A] {x : A} {n : ℕ} (hx : x ^ n = 0) {f : PowerSeries R} {p : Polynomial R} (h : ∀ d < n, (coeff d) f = p.coeff d) : (Polynomial.aeval x) ((trunc n) f) = (Polynomial.aeval x) p

Evaluation at an element x of a possibly noncommutative R-algebra with x ^ n = 0 sees a power series only through its coefficients below n: any polynomial with the same coefficients below n has the same value as the truncation.

theorem PowerSeries.trunc_inv_eq_of_trunc_eq {k : Type u_1} [Field k] {m : ℕ} {φ ψ : PowerSeries k} (h : (trunc m) φ = (trunc m) ψ) : (trunc m) φ⁻¹ = (trunc m) ψ⁻¹

Over a field, the m-truncation of φ⁻¹ depends only on trunc m φ.