Polynomial.taylor_zero'
theorem Polynomial.taylor_zero' : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.taylor 0 = LinearMap.id
The theorem `Polynomial.taylor_zero'` states that for any type `R` equipped with a structure of semiring, the Taylor expansion of a polynomial at 0 is equivalent to the identity linear map. In other words, if you evaluate the Taylor series of any polynomial at the point zero, it acts as the identity on the polynomial.
More concisely: For any semiring `R`, the Taylor expansion of a polynomial `f` over `R` at `0` equals the identity polynomial.
|
Polynomial.sum_taylor_eq
theorem Polynomial.sum_taylor_eq :
∀ {R : Type u_2} [inst : CommRing R] (f : Polynomial R) (r : R),
(((Polynomial.taylor r) f).sum fun i a => Polynomial.C a * (Polynomial.X - Polynomial.C r) ^ i) = f
The theorem `Polynomial.sum_taylor_eq` states that for any commutative ring `R`, any polynomial `f` of `R`, and any element `r` of `R`, the sum of each term of the Taylor expansion of `f` at `r`, where each term is defined as the coefficient `a` times `(Polynomial.X - Polynomial.C r)` raised to the power `i`, is equal to `f` itself. In other words, this theorem states the Taylor's formula in the context of polynomials over a commutative ring, which is essentially the process of expanding a given polynomial around a particular point `r` in the ring.
More concisely: For any commutative ring R, polynomial f, and element r in R, the sum of the terms in the Taylor expansion of f around r is equal to f itself.
|
Polynomial.taylor_one
theorem Polynomial.taylor_one :
∀ {R : Type u_1} [inst : Semiring R] (r : R), (Polynomial.taylor r) 1 = Polynomial.C 1
This theorem states that for any semi-ring `R` and any element `r` from `R`, the Taylor expansion of the constant polynomial `1` at `r` is equal to the constant polynomial `1` itself. Here, `Polynomial.taylor r` represents the Taylor expansion at `r`, and `Polynomial.C 1` represents the constant polynomial `1`.
More concisely: For any semi-ring `R` and element `r` from `R`, the Taylor expansion of the constant polynomial `1` at `x = r` equals the constant polynomial `1` itself.
|
Polynomial.taylor_mul
theorem Polynomial.taylor_mul :
∀ {R : Type u_2} [inst : CommSemiring R] (r : R) (p q : Polynomial R),
(Polynomial.taylor r) (p * q) = (Polynomial.taylor r) p * (Polynomial.taylor r) q
This theorem, `Polynomial.taylor_mul`, states that for any given commutative semiring `R`, a value `r` in `R`, and two polynomials `p` and `q` over `R`, the Taylor expansion at `r` of the product of `p` and `q` is equal to the product of the Taylor expansion at `r` of `p` and the Taylor expansion at `r` of `q`. In mathematical terms, it means that the operation of taking the Taylor expansion at a point is compatible with polynomial multiplication.
More concisely: For any commutative semiring `R`, polynomials `p` and `q` over `R`, and value `r` in `R`, the Taylor expansions of `p` and `q` at `r` are multiplicatively compatible, that is, the Taylor expansion of their product equals the product of their individual Taylor expansions at `r`.
|
Polynomial.taylor_coeff
theorem Polynomial.taylor_coeff :
∀ {R : Type u_1} [inst : Semiring R] (r : R) (f : Polynomial R) (n : ℕ),
((Polynomial.taylor r) f).coeff n = Polynomial.eval r ((Polynomial.hasseDeriv n) f)
The theorem `Polynomial.taylor_coeff` asserts that for any semiring `R`, any element `r` of `R`, any polynomial `f` over `R`, and any natural number `n`, the `n`th coefficient of the Taylor expansion of `f` at `r` is equal to the evaluation at `r` of the `n`th Hasse derivative of `f`. In mathematical notation, this is saying that if `f` is a polynomial and `r` is a point, then the `n`th coefficient of the Taylor series of `f` around `r` is equal to the value at `r` of the `n`th Hasse derivative of `f`. The Hasse derivative is a variant of the derivative that incorporates binomial coefficients.
More concisely: For any semiring `R`, polynomial `f` over `R`, element `r` in `R`, and natural number `n`, the `n`th coefficient of the Taylor expansion of `f` at `r` equals the `n`th Hasse derivative of `f` evaluated at `r`.
|
Polynomial.taylor_taylor
theorem Polynomial.taylor_taylor :
∀ {R : Type u_2} [inst : CommSemiring R] (f : Polynomial R) (r s : R),
(Polynomial.taylor r) ((Polynomial.taylor s) f) = (Polynomial.taylor (r + s)) f
This theorem states that for any commutative semiring `R`, any polynomial `f` of `R`, and any two elements `r` and `s` of `R`, the Taylor expansion of `f` at `r` after the Taylor expansion at `s` is equal to the Taylor expansion of `f` at `r + s`. This implies that the order of Taylor expansions does not matter, and they can be combined into a single Taylor expansion at the sum of the original points.
More concisely: For any commutative semiring `R`, given polynomials `f` and elements `r` and `s` of `R`, the Taylor expansions of `f` at `r` after the Taylor expansion at `s` and at `r + s` are equal.
|