Wronskian of a pair of polynomial

This file defines Wronskian of a pair of polynomials, which is W(a, b) = ab' - a'b. We also prove basic properties of it.

Main declarations

• Polynomial.wronskian_eq_of_sum_zero: We have W(a, b) = W(b, c) when a + b + c = 0.
• Polynomial.degree_wronskian_lt_add: Degree of Wronskian W(a, b) is strictly smaller than the sum of degrees of a and b
• Polynomial.natDegree_wronskian_lt_add: natDegree version of the above theorem. We need to assume that the Wronskian is nonzero. (Otherwise, a = b = 1 gives a counterexample.)

TODO

• Define Wronskian for n-tuple of polynomials, not necessarily two.

def Polynomial.wronskian {R : Type u_1} [CommRing R] (a : Polynomial R) (b : Polynomial R) : Polynomial R

Wronskian of a pair of polynomials, W(a, b) = ab' - a'b.

Equations

• a.wronskian b = a * Polynomial.derivative b - Polynomial.derivative a * b

def Polynomial.wronskianBilin (R : Type u_1) [CommRing R] : Polynomial R →ₗ[R] Polynomial R →ₗ[R] Polynomial R

Polynomial.wronskian as a bilinear map.

Equations

• Polynomial.wronskianBilin R = (LinearMap.mul R (Polynomial R)).compl₂ Polynomial.derivative - LinearMap.mul R (Polynomial R) ∘ₗ Polynomial.derivative

@[simp]

theorem Polynomial.wronskianBilin_apply {R : Type u_1} [CommRing R] (a : Polynomial R) (b : Polynomial R) : ((Polynomial.wronskianBilin R) a) b = a.wronskian b

@[simp]

theorem Polynomial.wronskian_zero_left {R : Type u_1} [CommRing R] (a : Polynomial R) : Polynomial.wronskian 0 a = 0

@[simp]

theorem Polynomial.wronskian_zero_right {R : Type u_1} [CommRing R] (a : Polynomial R) : a.wronskian 0 = 0

theorem Polynomial.wronskian_neg_left {R : Type u_1} [CommRing R] (a : Polynomial R) (b : Polynomial R) : (-a).wronskian b = -a.wronskian b

theorem Polynomial.wronskian_neg_right {R : Type u_1} [CommRing R] (a : Polynomial R) (b : Polynomial R) : a.wronskian (-b) = -a.wronskian b

theorem Polynomial.wronskian_add_right {R : Type u_1} [CommRing R] (a : Polynomial R) (b : Polynomial R) (c : Polynomial R) : a.wronskian (b + c) = a.wronskian b + a.wronskian c

theorem Polynomial.wronskian_add_left {R : Type u_1} [CommRing R] (a : Polynomial R) (b : Polynomial R) (c : Polynomial R) : (a + b).wronskian c = a.wronskian c + b.wronskian c

theorem Polynomial.wronskian_self_eq_zero {R : Type u_1} [CommRing R] (a : Polynomial R) : a.wronskian a = 0

theorem Polynomial.isAlt_wronskianBilin {R : Type u_1} [CommRing R] : (Polynomial.wronskianBilin R).IsAlt

theorem Polynomial.wronskian_neg_eq {R : Type u_1} [CommRing R] (a : Polynomial R) (b : Polynomial R) : -a.wronskian b = b.wronskian a

theorem Polynomial.wronskian_eq_of_sum_zero {R : Type u_1} [CommRing R] {a : Polynomial R} {b : Polynomial R} {c : Polynomial R} (hAdd : a + b + c = 0) : a.wronskian b = b.wronskian c

theorem Polynomial.degree_wronskian_lt_add {R : Type u_1} [CommRing R] {a : Polynomial R} {b : Polynomial R} (ha : a ≠ 0) (hb : b ≠ 0) : (a.wronskian b).degree < a.degree + b.degree

Degree of W(a,b) is strictly less than the sum of degrees of a and b (both nonzero).

theorem Polynomial.natDegree_wronskian_lt_add {R : Type u_1} [CommRing R] {a : Polynomial R} {b : Polynomial R} (hw : a.wronskian b ≠ 0) : (a.wronskian b).natDegree < a.natDegree + b.natDegree

natDegree version of the above theorem. Note this would be false with just (ha : a ≠ 0) (hb : b ≠ 0), as when a = b = 1we have(wronskian a b).natDegree = a.natDegree = b.natDegree = 0`.