Interval integrals of polynomial derivatives

For a polynomial w : ℝ[X], the second-order operator p ↦ derivative (w * derivative p) on ℝ[X] is symmetric under the interval integral on [a, b] whenever its leading coefficient w vanishes at both endpoints: integrating it applied to p against q gives the same value as integrating p against it applied to q. This is the Sturm–Liouville symmetry, with weight 1, for an operator whose leading coefficient vanishes at the endpoints, so that the boundary term of the integration by parts drops. Combined with an eigenfunction equation it makes the polynomial eigenfunctions for distinct eigenvalues orthogonal: the Legendre polynomials are the eigenfunctions of the case w = 1 - X ^ 2 on [-1, 1], and the Gegenbauer polynomials of index 3/2 of Mathematics/SpecialFunctions/Gegenbauer/Basic.lean (applied in Mathematics/SpecialFunctions/Gegenbauer/Measure.lean) those of the case w = (1 - X ^ 2) ^ 2, an operator symmetric for the weight 1 - X ^ 2.

Main statements

• Polynomial.integral_derivative_mul_derivative_mul_comm: the symmetry of p ↦ derivative (w * derivative p) under the interval integral on [a, b] when w vanishes at a and b.

theorem Polynomial.integral_derivative_mul_derivative_mul_comm (w p q : Polynomial ℝ) {a b : ℝ} (ha : eval a w = 0) (hb : eval b w = 0) : ∫ (x : ℝ) in a..b, eval x (derivative (w * derivative p) * q) = ∫ (x : ℝ) in a..b, eval x (p * derivative (w * derivative q))

The operator p ↦ derivative (w * derivative p) is symmetric under the interval integral on [a, b] when its leading coefficient w vanishes at both endpoints: pairing it applied to p with q gives the same integral as pairing p with it applied to q. This is the Sturm–Liouville symmetry (with weight 1); combined with the eigenfunction equation it makes the eigenfunctions for distinct eigenvalues orthogonal.