Markov's inequality at an endpoint

This file proves markovEndpoint : MarkovEndpoint: a real polynomial p of degree at most D with |p| ≤ 1 on [0,2] satisfies |p'(0)| ≤ D². This is the second assertion of Lemma 6.1 of the paper. The paper proves the lemma directly, by interpolation at the points cos (k π / D); here the assertion is deduced from Mathlib's extremal property of the Chebyshev polynomials (Polynomial.Chebyshev.eval_iterate_derivative_le_of_forall_abs_le_one, with k = 1, x = 1), applied to p.comp (1 - X) and to its negative.

theorem AaronsonAmbainis.Row.neg_derivative_eval_zero_le (D : ℕ) (p : Polynomial ℝ) (hdeg : p.natDegree ≤ D) (hbnd : ∀ (s : ℝ), 0 ≤ s → s ≤ 2 → |Polynomial.eval s p| ≤ 1) : -Polynomial.eval 0 (Polynomial.derivative p) ≤ ↑D ^ 2

One-sided form: -p'(0) ≤ D² if |p| ≤ 1 on [0,2] and natDegree p ≤ D.

theorem AaronsonAmbainis.markovEndpoint : MarkovEndpoint

Markov's inequality at the endpoint 0 of [0,2].