PowerSeries.trunc_trunc_mul
theorem PowerSeries.trunc_trunc_mul :
∀ {R : Type u_2} [inst : CommSemiring R] {n : ℕ} (f g : PowerSeries R),
PowerSeries.trunc n (↑(PowerSeries.trunc n f) * g) = PowerSeries.trunc n (f * g)
The theorem `PowerSeries.trunc_trunc_mul` states that for any commutative semiring `R`, and for any natural number `n`, and for any two formal power series `f` and `g` over `R`, the `n`th truncation of the product of the `n`th truncation of `f` and `g` is equal to the `n`th truncation of the product of `f` and `g`. This essentially means that truncating a power series before multiplication gives the same result as truncating after multiplication.
More concisely: For any commutative semiring R and natural numbers n, the n-th truncation of the product of the n-th truncations of formal power series f and g over R equals the n-th truncation of the product of f and g.
|
PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc₂
theorem PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc₂ :
∀ {R : Type u_2} [inst : CommSemiring R] {n a b : ℕ} (f g : PowerSeries R),
n < a →
n < b →
(PowerSeries.coeff R n) (f * g) =
(PowerSeries.coeff R n) (↑(PowerSeries.trunc a f) * ↑(PowerSeries.trunc b g))
The theorem `PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc₂` states that for any commutative semiring `R`, and any natural numbers `n`, `a`, `b` and power series `f` and `g` over `R`, if `n` is less than `a` and `n` is also less than `b`, then the `n`-th coefficient of the product of `f` and `g` is equal to the `n`-th coefficient of the product of the truncations of `f` and `g` at `a` and `b` respectively. In other words, for the given conditions, the `n`-th coefficient of the product of two power series can be calculated by truncating the two series at certain points and then multiplying the truncated series.
More concisely: For any commutative semiring `R`, and power series `f` and `g` over `R`, if `n` is less than the degrees `a` and `b` of `f` and `g` respectively, then the `n`-th coefficient of the product of `f` and `g` equals the `n`-th coefficient of the product of the truncations of `f` and `g` at degrees `a` and `b`.
|
PowerSeries.coeff_trunc
theorem PowerSeries.coeff_trunc :
∀ {R : Type u_1} [inst : Semiring R] (m n : ℕ) (φ : PowerSeries R),
(PowerSeries.trunc n φ).coeff m = if m < n then (PowerSeries.coeff R m) φ else 0
The theorem `PowerSeries.coeff_trunc` states that for any type `R` under a semiring, for any natural numbers `m` and `n`, and for any power series `φ` over `R`, the `m`-th coefficient of the `n`-th truncation of the power series is equal to the `m`-th coefficient of the power series if `m` is less than `n`. Otherwise, it is `0`. In other words, it determines the `m`-th coefficient of the polynomial obtained from truncating the power series at the `n`-th term.
More concisely: For any semiring `R`, power series `φ` over `R`, and natural numbers `m` and `n` with `m < n`, the `m`-th coefficient of the `n`-th truncation of `φ` equals the `m`-th coefficient of `φ`. Otherwise, it is `0`.
|
PowerSeries.coeff_coe_trunc_of_lt
theorem PowerSeries.coeff_coe_trunc_of_lt :
∀ {R : Type u_2} [inst : CommSemiring R] {n m : ℕ} {f : PowerSeries R},
n < m → (PowerSeries.coeff R n) ↑(PowerSeries.trunc m f) = (PowerSeries.coeff R n) f
This theorem states that the nth coefficient function `coeff n : R⟦X⟧ → R` for a power series `f` over a commutative semiring `R` is continuous. Specifically, if `n` is less than `m`, then the nth coefficient of the mth truncation of `f` to a polynomial is the same as the nth coefficient of `f` itself. In other words, the value of `coeff n f` depends only on a sufficiently long truncation of the power series `f`.
More concisely: The nth coefficient function of a power series over a commutative semiring is continuous and equals the nth coefficient of any truncation of sufficient degree.
|