The Markov brothers' inequality

A real polynomial p of degree at most n with |p| ≤ M on [-1, 1] has |p'| ≤ n² M on [-1, 1] (Polynomial.abs_eval_derivative_le), the inequality of A. A. Markov ([BE95], [Riv90]). The proof combines two classical inequalities.

• Schur's inequality: a polynomial q of degree less than n ≥ 1 with √(1 - x²) |q(x)| ≤ M on [-1, 1] has |q| ≤ n M there (Polynomial.abs_eval_le_mul_of_sqrt_mul_abs_eval_le). Where √(1 - x²) ≥ sin (π / 2n) ≥ 1 / n this is immediate. Beyond the largest zero cos (π / 2n) of the Chebyshev polynomial T n, interpolate q at the n zeros ηₖ of T n. There every Lagrange basis polynomial is T n(x) / ((x - ηₖ) T n'(ηₖ)) with T n(x) / (x - ηₖ) ≥ 0, the identity |T n'(ηₖ)| √(1 - ηₖ²) = n turns the bound on √(1 - ηₖ²) |q(ηₖ)| into a bound on each term, and the terms add up to M T n'(x) / n ≤ M T n'(1) / n = n M.
• Bernstein's inequality: √(1 - x²) |p'(x)| ≤ n M on [-1, 1] (Polynomial.sqrt_mul_abs_eval_derivative_le). For a ∈ [-1, 1] and b = √(1 - a²), the odd part (p(ac + bs) - p(ac - bs)) / 2 of p along the circle c² + s² = 1 is s r(c) for a polynomial r of degree less than n with r(1) = b p'(a), read off the Taylor expansion of p at ac. Since |ac ± bs| ≤ 1, Schur's inequality at 1 bounds r(1).

Schur's inequality applied to p' with Bernstein's bound gives Markov's.

Rescaled to an interval [a, b], Markov's inequality reads (b - a) |p'| ≤ 2 n² M (Polynomial.sub_mul_abs_eval_derivative_le). A polynomial of degree at most d whose values at the integers 0, …, N lie in [b₁, b₂] therefore has (N - d²) |q'| ≤ d² (b₂ - b₁) on [0, N] (Polynomial.sub_mul_abs_eval_derivative_le_of_forall_nat): every point of [0, N] is within 1/2 of an integer, so the largest value c of |q'| on [0, N] keeps q within c / 2 of [b₁, b₂], and Markov's inequality gives N c ≤ d² (b₂ - b₁ + c). The same argument bounds q itself, (N - d²) |q| ≤ N max |q(k)| (Polynomial.sub_mul_abs_eval_le_of_forall_nat), the bound of Ehlich and Zeller [EZ64] (see also [CR92]), and gives the lemma behind the degree bounds of Nisan and Szegedy [NS94] (Polynomial.mul_le_sq_mul_of_le_abs_eval_derivative).

Main results

• Polynomial.abs_eval_le_mul_of_sqrt_mul_abs_eval_le: Schur's inequality.
• Polynomial.sqrt_mul_abs_eval_derivative_le: Bernstein's inequality.
• Polynomial.abs_eval_derivative_le: the Markov brothers' inequality, |p'| ≤ n² M.
• Polynomial.sub_mul_abs_eval_derivative_le: Markov's inequality on an interval [a, b].
• Polynomial.sub_mul_abs_eval_derivative_le_of_forall_nat, Polynomial.sub_mul_abs_eval_le_of_forall_nat: polynomials bounded at the integers of [0, N].
• Polynomial.mul_le_sq_mul_of_le_abs_eval_derivative: the Nisan–Szegedy lemma: if moreover |q'(ξ)| ≥ c ≥ 0 at some ξ ∈ [0, N], then c N ≤ d² (c + b₂ - b₁).

References

• P. Borwein, T. Erdélyi, Polynomials and Polynomial Inequalities
• T. J. Rivlin, Chebyshev Polynomials
• H. Ehlich, K. Zeller, Schwankung von Polynomen zwischen Gitterpunkten
• D. Coppersmith, T. J. Rivlin, The growth of polynomials bounded at equally spaced points
• N. Nisan, M. Szegedy, On the degree of Boolean functions as real polynomials

Schur's inequality

theorem Polynomial.abs_eval_le_mul_of_sqrt_mul_abs_eval_le {n : ℕ} (hn : 0 < n) {q : Polynomial ℝ} (hq : q.natDegree < n) {M : ℝ} (hM : ∀ y ∈ Set.Icc (-1) 1, √(1 - y ^ 2) * |eval y q| ≤ M) {x : ℝ} (hx : x ∈ Set.Icc (-1) 1) : |eval x q| ≤ ↑n * M

Schur's inequality: a real polynomial q of degree less than n ≥ 1 with √(1 - x²) |q(x)| ≤ M on [-1, 1] satisfies |q(x)| ≤ n M on [-1, 1].

Bernstein's inequality

theorem Polynomial.sqrt_mul_abs_eval_derivative_le {n : ℕ} {p : Polynomial ℝ} (hp : p.natDegree ≤ n) {M : ℝ} (hM : ∀ y ∈ Set.Icc (-1) 1, |eval y p| ≤ M) {x : ℝ} (hx : x ∈ Set.Icc (-1) 1) : √(1 - x ^ 2) * |eval x (derivative p)| ≤ ↑n * M

Bernstein's inequality: a real polynomial p of degree at most n with |p| ≤ M on [-1, 1] satisfies √(1 - x²) |p'(x)| ≤ n M on [-1, 1].

Markov's inequality

theorem Polynomial.abs_eval_derivative_le {n : ℕ} {p : Polynomial ℝ} (hp : p.natDegree ≤ n) {M : ℝ} (hM : ∀ y ∈ Set.Icc (-1) 1, |eval y p| ≤ M) {x : ℝ} (hx : x ∈ Set.Icc (-1) 1) : |eval x (derivative p)| ≤ ↑n ^ 2 * M

The Markov brothers' inequality: a real polynomial p of degree at most n with |p| ≤ M on [-1, 1] satisfies |p'| ≤ n² M on [-1, 1].

theorem Polynomial.sub_mul_abs_eval_derivative_le {n : ℕ} {p : Polynomial ℝ} (hp : p.natDegree ≤ n) {a b M : ℝ} (hab : a < b) (hM : ∀ y ∈ Set.Icc a b, |eval y p| ≤ M) {x : ℝ} (hx : x ∈ Set.Icc a b) : (b - a) * |eval x (derivative p)| ≤ 2 * ↑n ^ 2 * M

Markov's inequality on an interval: a real polynomial p of degree at most n with |p| ≤ M on [a, b] satisfies (b - a) |p'| ≤ 2 n² M on [a, b].

Polynomials bounded at the integers

theorem Polynomial.sub_mul_abs_eval_derivative_le_of_forall_nat {d N : ℕ} {q : Polynomial ℝ} (hq : q.natDegree ≤ d) (hN : 0 < N) {b₁ b₂ : ℝ} (hb : ∀ k ≤ N, eval (↑k) q ∈ Set.Icc b₁ b₂) {x : ℝ} (hx : x ∈ Set.Icc 0 ↑N) : (↑N - ↑d ^ 2) * |eval x (derivative q)| ≤ ↑d ^ 2 * (b₂ - b₁)

Polynomials bounded at the integers, derivative form: a real polynomial q of degree at most d whose values at the integers 0, …, N lie in [b₁, b₂] satisfies (N - d²) |q'| ≤ d² (b₂ - b₁) on [0, N].

theorem Polynomial.sub_mul_abs_eval_le_of_forall_nat {d N : ℕ} {q : Polynomial ℝ} (hq : q.natDegree ≤ d) (hN : 0 < N) {B : ℝ} (hb : ∀ k ≤ N, |eval (↑k) q| ≤ B) {x : ℝ} (hx : x ∈ Set.Icc 0 ↑N) : (↑N - ↑d ^ 2) * |eval x q| ≤ ↑N * B

The Ehlich–Zeller bound: a real polynomial q of degree at most d with |q| ≤ B at the integers 0, …, N satisfies (N - d²) |q| ≤ N B on [0, N]; for d² < N this bounds q on the whole interval [EZ64], [CR92].

theorem Polynomial.mul_le_sq_mul_of_le_abs_eval_derivative {d N : ℕ} {q : Polynomial ℝ} (hq : q.natDegree ≤ d) (hN : 0 < N) {b₁ b₂ : ℝ} (hb : ∀ k ≤ N, eval (↑k) q ∈ Set.Icc b₁ b₂) {ξ c : ℝ} (hξ : ξ ∈ Set.Icc 0 ↑N) (hc : 0 ≤ c) (hcξ : c ≤ |eval ξ (derivative q)|) : c * ↑N ≤ ↑d ^ 2 * (c + (b₂ - b₁))

The Nisan–Szegedy lemma: a real polynomial q of degree at most d whose values at the integers 0, …, N lie in [b₁, b₂], and with |q'(ξ)| ≥ c ≥ 0 at some ξ ∈ [0, N], satisfies c N ≤ d² (c + (b₂ - b₁)) [NS94].