Theory of univariate polynomials
The main def is binom_expansion.
Equations
- polynomial.pow_add_expansion x y (n + 2) = (polynomial.pow_add_expansion x y n.succ).cases_on (λ (z : R) (hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2), ⟨x * z + (↑n + 1) * x ^ n + z * y, _⟩)
- polynomial.pow_add_expansion x y 1 = ⟨0, _⟩
- polynomial.pow_add_expansion x y 0 = ⟨0, _⟩
theorem
polynomial.derivative_eval
{R : Type u}
[comm_ring R]
(p : polynomial R)
(x : R) :
polynomial.eval x p.derivative = finsupp.sum p (λ (n : ℕ) (a : R), a * ↑n * x ^ (n - 1))
def
polynomial.binom_expansion
{R : Type u}
[comm_ring R]
(f : polynomial R)
(x y : R) :
{k // polynomial.eval (x + y) f = polynomial.eval x f + polynomial.eval x f.derivative * y + k * y ^ 2}
Equations
- f.binom_expansion x y = ⟨finsupp.sum f (λ (e : ℕ) (a : R), a * (poly_binom_aux1 x y e a).val), _⟩
def
polynomial.eval_sub_factor
{R : Type u}
[comm_ring R]
(f : polynomial R)
(x y : R) :
{z // polynomial.eval x f - polynomial.eval y f = z * (x - y)}
Equations
- f.eval_sub_factor x y = ⟨finsupp.sum f (λ (i : ℕ) (r : R), r * (polynomial.pow_sub_pow_factor x y i).val), _⟩