Chebyshev polynomials over the reals: some extremal properties

• Chebyshev polynomials have largest leading coefficient, following proof in https://math.stackexchange.com/a/978145/1277
• Chebyshev polynomials maximize iterated derivatives at 1 and beyond

Main statements

• leadingCoeff_le_of_forall_abs_le_one: If P is a real polynomial of degree at most n and |P (x)| ≤ 1 for all x ∈ [-1, 1] then the leading coefficient of P is at most 2 ^ (n - 1)
• leadingCoeff_eq_iff_of_forall_abs_le_one: When n ≥ 2, equality holds iff P = T_n
• eval_iterate_derivative_le_of_forall_abs_le_one: If P is a real polynomial of degree at most n and |P (x)| ≤ 1 for all x ∈ [-1, 1] then for all x ≥ 1, P ^ (k) (x) ≤ T_n ^ (k)(x)
• eval_iterate_derivative_eq_iff_of_forall_abs_le_one: If 0 < k ≤ n then equality holds iff P = T_n

Implementation

We describe the proof for the leading coefficient; the proof for iterated derivatives uses a similar approach.

By monotonicity of 2 ^ (n - 1), we can assume that P has degree exactly n. Using Lagrange interpolation, we can give a formula for the leading coefficient of P as a linear combination of the values of P on the Chebyshev nodes (sumNodes_eq_coeff). The Chebyshev polynomial T_n has value ±1 on the nodes, with the same signs as the coefficients of the linear combination (negOnePow_mul_leadingCoeffC_pos). Since |P (x)| ≤ 1 on the nodes, this implies that the leading coefficient of P is bounded by that of T_n, which is known to equal 2 ^ (n - 1). Moreover, equality holds iff P and T_n agree on the nodes, which implies that they coincide.

noncomputable def Polynomial.Chebyshev.node (n i : ℕ) : ℝ

For n ≠ 0 and i ≤ n, node n i is one of the extremal points of the Chebyshev T polynomial over the interval [-1, 1].

Equations

• Polynomial.Chebyshev.node n i = Real.cos (↑i * Real.pi / ↑n)

theorem Polynomial.Chebyshev.node_eq_one {n : ℕ} : node n 0 = 1

theorem Polynomial.Chebyshev.node_eq_neg_one {n : ℕ} (hn : n ≠ 0) : node n n = -1

theorem Polynomial.Chebyshev.node_mem_Icc {n i : ℕ} : node n i ∈ Set.Icc (-1) 1

theorem Polynomial.Chebyshev.eval_T_real_node {n i : ℕ} (hi : i ∈ Finset.Iic n) : eval (node n i) (T ℝ ↑n) = (-1) ^ i

theorem Polynomial.Chebyshev.strictAntiOn_node (n : ℕ) : StrictAntiOn (fun (x : ℕ) => node n x) ↑(Finset.range (n + 1))

theorem Polynomial.Chebyshev.node_lt {n i j : ℕ} (hj : j ≤ n) (hij : i < j) : node n j < node n i

theorem Polynomial.Chebyshev.zero_lt_prod_node_sub_node {n i : ℕ} (hi : i ≤ n) : 0 < (-1) ^ i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)

noncomputable def Polynomial.Chebyshev.sumNodes (n : ℕ) (c : ℕ → ℝ) (P : Polynomial ℝ) : ℝ

For a polynomial P and coefficient function c, sumNodes n c P is a linear combination of P evaluated at the n'th order Chebyshev nodes, with coefficients taken from c.

Equations

• Polynomial.Chebyshev.sumNodes n c P = ∑ i ≤ n, Polynomial.eval (Polynomial.Chebyshev.node n i) P * c i

theorem Polynomial.Chebyshev.sumNodes_le_sumNodes_T {n : ℕ} {c : ℕ → ℝ} (hcnonneg : ∀ i ≤ n, 0 ≤ (-1) ^ i * c i) {P : Polynomial ℝ} (hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1) : sumNodes n c P ≤ sumNodes n c (T ℝ ↑n)

theorem Polynomial.Chebyshev.sumNodes_eq_sumNodes_T_iff {n : ℕ} {c : ℕ → ℝ} (hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i) {P : Polynomial ℝ} (hPdeg : P.degree ≤ ↑n) (hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1) : sumNodes n c P = sumNodes n c (T ℝ ↑n) ↔ P = T ℝ ↑n

theorem Polynomial.Chebyshev.coeff_le_of_forall_abs_le_one {n : ℕ} {P : Polynomial ℝ} (hPdeg : P.degree ≤ ↑n) (hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1) : P.coeff n ≤ 2 ^ (n - 1)

theorem Polynomial.Chebyshev.leadingCoeff_le_of_forall_abs_le_one {n : ℕ} {P : Polynomial ℝ} (hPdeg : P.degree ≤ ↑n) (hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1) : P.leadingCoeff ≤ 2 ^ (n - 1)

theorem Polynomial.Chebyshev.coeff_eq_iff_of_forall_abs_le_one {n : ℕ} {P : Polynomial ℝ} (hPdeg : P.degree ≤ ↑n) (hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1) : P.coeff n = 2 ^ (n - 1) ↔ P = T ℝ ↑n

theorem Polynomial.Chebyshev.leadingCoeff_eq_iff_of_forall_abs_le_one {n : ℕ} {P : Polynomial ℝ} (hn : 2 ≤ n) (hPdeg : P.degree ≤ ↑n) (hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1) : P.leadingCoeff = 2 ^ (n - 1) ↔ P = T ℝ ↑n

theorem Polynomial.Chebyshev.eval_iterate_derivative_le_of_forall_abs_le_one {n : ℕ} {P : Polynomial ℝ} {k : ℕ} {x : ℝ} (hx : 1 ≤ x) (hPdeg : P.degree ≤ ↑n) (hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1) : eval x ((⇑derivative)^[k] P) ≤ eval x ((⇑derivative)^[k] (T ℝ ↑n))

theorem Polynomial.Chebyshev.eval_iterate_derivative_eq_iff_of_bounded {n : ℕ} {P : Polynomial ℝ} {k : ℕ} (hk₁ : 0 < k) (hk₂ : k ≤ n) {x : ℝ} (hx : 1 ≤ x) (hPdeg : P.degree ≤ ↑n) (hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1) : eval x ((⇑derivative)^[k] P) = eval x ((⇑derivative)^[k] (T ℝ ↑n)) ↔ P = T ℝ ↑n