markov_inequality
Provedanalysisapproximation-theoryproved
Markov brothers inequality: If |f(x)| ≤ 1 on [-1,1] for a polynomial f of degree n, then |f'(x)| ≤ n² on [-1,1]. Proved by Andrei Markov (1889). Sharp with equality at Chebyshev polynomials.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem markov_inequality (f : ℝ → ℝ) (n : ℕ) (hn : 1 ≤ n)
(hf : ∀ x, |x| ≤ 1 → |f x| ≤ 1)
(hpoly : ∃ p : Polynomial ℝ, p.natDegree = n ∧ ∀ x, p.eval x = f x) :
∀ x : ℝ, |x| ≤ 1 → |deriv f x| ≤ n ^ 2 := by
sorrySource