Cotes' harmonic means theorem

Let f(x, y) = 0 be a plane algebraic curve, p a point not on it, and L = {p + t v} a line through p meeting the curve in d real points p + tᵢ v, i.e. g(t) = f(p + t v) splits with roots tᵢ. The harmonic-mean point p + t* v, d / t* = Σ 1/tᵢ, lies on the line ∇f(p) · (x - p) = -d f(p) (the polar of p), which does not depend on L (Cotes, 1722). The proof computes g(0) = f(p) and g'(0) = ∇f(p) · v by induction on f, and Σ 1/tᵢ = -g'(0)/g(0) from Mathlib's logarithmic-derivative formula for split polynomials (Splits.eval_derivative_div_eval_of_ne_zero).

Main results

• Cotes.sum_inv_roots_eq: sum of reciprocal roots of the restriction g(t) = f(p + t v) is -g'(0)/g(0)
• Cotes.harmonic_mean_polar: the harmonic mean point of the intersections lies on the polar line of p

References

• R. Cotes, Harmonia Mensurarum, Cambridge, 1722 (published by R. Smith).
• C. Maclaurin, De linearum geometricarum proprietatibus generalibus, 1748.

theorem Cotes.sum_inv_roots_eq (g : Polynomial ℝ) (hsplit : g.roots.card = g.natDegree) (h0 : Polynomial.eval 0 g ≠ 0) : (Multiset.map (fun (r : ℝ) => r⁻¹) g.roots).sum = -(Polynomial.eval 0 (Polynomial.derivative g) / Polynomial.eval 0 g)

For a split polynomial g with g(0) ≠ 0: Σ 1/rᵢ = -g'(0)/g(0) over its roots.

theorem Cotes.line_value_deriv (p v : Fin 2 → ℝ) (f : MvPolynomial (Fin 2) ℝ) : Polynomial.eval 0 ((MvPolynomial.aeval fun (i : Fin 2) => Polynomial.C (p i) + Polynomial.C (v i) * Polynomial.X) f) = (MvPolynomial.eval p) f ∧ Polynomial.eval 0 (Polynomial.derivative ((MvPolynomial.aeval fun (i : Fin 2) => Polynomial.C (p i) + Polynomial.C (v i) * Polynomial.X) f)) = ∑ i : Fin 2, (MvPolynomial.eval p) ((MvPolynomial.pderiv i) f) * v i

Value and derivative at t = 0 of the restriction of f to the line p + t v.

theorem Cotes.harmonic_mean_polar (f : MvPolynomial (Fin 2) ℝ) (p v : Fin 2 → ℝ) (hp : (MvPolynomial.eval p) f ≠ 0) (g : Polynomial ℝ) (hg : g = (MvPolynomial.aeval fun (i : Fin 2) => Polynomial.C (p i) + Polynomial.C (v i) * Polynomial.X) f) (hsplit : g.roots.card = g.natDegree) (hd : 1 ≤ g.natDegree) (hH : (Multiset.map (fun (r : ℝ) => r⁻¹) g.roots).sum ≠ 0) : ∑ i : Fin 2, (MvPolynomial.eval p) ((MvPolynomial.pderiv i) f) * (↑g.natDegree / (Multiset.map (fun (r : ℝ) => r⁻¹) g.roots).sum * v i) = -↑g.natDegree * (MvPolynomial.eval p) f

Cotes' harmonic means theorem.