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
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.

Instances For
    source
    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) φ)
    source
    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
    source
    @[simp]
    theorem PowerSeries.trunc_one {R : Type u_1} [Semiring R] (n : ℕ) :
    (trunc (n + 1)) 1 = 1
    source
    @[simp]
    theorem PowerSeries.trunc_C {R : Type u_1} [Semiring R] (n : ℕ) (a : R) :
    (trunc (n + 1)) (C a) = Polynomial.C a
    source
    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)
    source
    theorem PowerSeries.natDegree_trunc_lt {R : Type u_1} [Semiring R] (f : PowerSeries R) (n : ℕ) :
    ((trunc (n + 1)) f).natDegree < n + 1
    source
    @[simp]
    theorem PowerSeries.trunc_zero' {R : Type u_1} [Semiring R] {f : PowerSeries R} :
    (trunc 0) f = 0
    source
    theorem PowerSeries.degree_trunc_lt {R : Type u_1} [Semiring R] (f : PowerSeries R) (n : ℕ) :
    ((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 ((trunc n) f) = ∑ i ∈ Finset.range n, G ((coeff i) f) * s ^ i
    source
    @[simp]
    theorem PowerSeries.trunc_X {R : Type u_1} [Semiring R] (n : ℕ) :
    (trunc (n + 2)) X = Polynomial.X
    source
    theorem PowerSeries.trunc_X_of {R : Type u_1} [Semiring R] {n : ℕ} (hn : 2 ≤ n) :
    (trunc n) X = Polynomial.X
    source
    @[simp]
    theorem PowerSeries.trunc_one_left {R : Type u_1} [Semiring R] (p : PowerSeries R) :
    (trunc 1) p = Polynomial.C ((coeff 0) p)
    source
    theorem PowerSeries.trunc_one_X {R : Type u_1} [Semiring R] :
    (trunc 1) X = 0
    source
    @[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
    source
    @[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
    source
    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.

    source
    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.

    source
    theorem PowerSeries.monomial_eq_C_mul_X_pow {R : Type u_1} [Semiring R] (r : R) (n : ℕ) :
    (monomial n) r = C r * X ^ n
    source
    @[simp]
    theorem PowerSeries.trunc_X_pow_self_mul {R : Type u_1} [Semiring R] (n : ℕ) (p : PowerSeries R) :
    (trunc n) (X ^ n * p) = 0
    source
    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
    source
    @[simp]
    theorem PowerSeries.trunc_trunc {R : Type u_2} [CommSemiring R] {n : ℕ} (f : PowerSeries R) :
    (trunc n) ↑((trunc n) f) = (trunc n) f
    source
    @[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)
    source
    @[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)
    source
    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)
    source
    @[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)
    source
    theorem PowerSeries.trunc_coe_eq_self {R : Type u_2} [CommSemiring R] {n : ℕ} {f : Polynomial R} (hn : f.natDegree < n) :
    (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) :
    (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.

    source
    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.

    source
    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))
    source
    @[simp]
    theorem PowerSeries.trunc_sub {R : Type u_1} [Ring R] (n : ℕ) (φ ψ : PowerSeries R) :
    (trunc n) (φ - ψ) = (trunc n) φ - (trunc n) ψ
    source
    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)