Chebyshev polynomials over the reals: roots and extrema

Main statements

• T_n(x) ∈ [-1, 1] iff x ∈ [-1, 1]: abs_eval_T_real_le_one_iff
• Zeroes of T and U: roots_T_real, roots_U_real
• Local extrema of T: isLocalExtr_T_real_iff, isExtrOn_T_real_iff
• Irrationality of zeroes of T other than zero: irrational_of_isRoot_T_real
• |T_n^{(k)} (x)| ≤ T_n^{(k)} (1) for x ∈ [-1, 1]: abs_iterate_derivative_T_real_le

TODO

Show that the bound on T_n^{(k)} (x) is achieved only at x = ±1

theorem Polynomial.Chebyshev.eval_T_real_mem_Icc (n : ℤ) {x : ℝ} (hx : x ∈ Set.Icc (-1) 1) : eval x (T ℝ n) ∈ Set.Icc (-1) 1

theorem Polynomial.Chebyshev.abs_eval_T_real_le_one (n : ℤ) {x : ℝ} (hx : |x| ≤ 1) : |eval x (T ℝ n)| ≤ 1

theorem Polynomial.Chebyshev.one_le_eval_T_real (n : ℤ) {x : ℝ} (hx : 1 ≤ x) : 1 ≤ eval x (T ℝ n)

theorem Polynomial.Chebyshev.one_lt_eval_T_real {n : ℤ} (hn : n ≠ 0) {x : ℝ} (hx : 1 < x) : 1 < eval x (T ℝ n)

theorem Polynomial.Chebyshev.one_le_negOnePow_mul_eval_T_real (n : ℤ) {x : ℝ} (hx : x ≤ -1) : 1 ≤ ↑↑n.negOnePow * eval x (T ℝ n)

theorem Polynomial.Chebyshev.one_lt_negOnePow_mul_eval_T_real {n : ℤ} (hn : n ≠ 0) {x : ℝ} (hx : x < -1) : 1 < ↑↑n.negOnePow * eval x (T ℝ n)

theorem Polynomial.Chebyshev.one_le_abs_eval_T_real (n : ℤ) {x : ℝ} (hx : 1 ≤ |x|) : 1 ≤ |eval x (T ℝ n)|

theorem Polynomial.Chebyshev.one_lt_abs_eval_T_real {n : ℤ} (hn : n ≠ 0) {x : ℝ} (hx : 1 < |x|) : 1 < |eval x (T ℝ n)|

theorem Polynomial.Chebyshev.abs_eval_T_real_le_one_iff {n : ℤ} (hn : n ≠ 0) (x : ℝ) : |x| ≤ 1 ↔ |eval x (T ℝ n)| ≤ 1

theorem Polynomial.Chebyshev.abs_eval_T_real_eq_one_iff {n : ℕ} (hn : n ≠ 0) (x : ℝ) : |eval x (T ℝ ↑n)| = 1 ↔ ∃ k ≤ n, x = Real.cos (↑k * Real.pi / ↑n)

theorem Polynomial.Chebyshev.eval_T_real_cos_int_mul_pi_div {k n : ℕ} (hn : n ≠ 0) : eval (Real.cos (↑k * Real.pi / ↑n)) (T ℝ ↑n) = ↑↑(↑k).negOnePow

theorem Polynomial.Chebyshev.eval_T_real_eq_one_iff {n : ℕ} (hn : n ≠ 0) (x : ℝ) : eval x (T ℝ ↑n) = 1 ↔ ∃ k ≤ n, Even k ∧ x = Real.cos (↑k * Real.pi / ↑n)

theorem Polynomial.Chebyshev.eval_T_real_eq_neg_one_iff {n : ℕ} (hn : n ≠ 0) (x : ℝ) : eval x (T ℝ ↑n) = -1 ↔ ∃ k ≤ n, Odd k ∧ x = Real.cos (↑k * Real.pi / ↑n)

theorem Polynomial.Chebyshev.roots_T_real_nodup (n : ℕ) : (Multiset.map (fun (k : ℕ) => Real.cos ((2 * ↑k + 1) * Real.pi / (2 * ↑n))) (Multiset.range n)).Nodup

theorem Polynomial.Chebyshev.roots_T_real (n : ℕ) : (T ℝ ↑n).roots = (Finset.image (fun (k : ℕ) => Real.cos ((2 * ↑k + 1) * Real.pi / (2 * ↑n))) (Finset.range n)).val

theorem Polynomial.Chebyshev.rootMultiplicity_T_real {n k : ℕ} (hk : k < n) : rootMultiplicity (Real.cos ((2 * ↑k + 1) * Real.pi / (2 * ↑n))) (T ℝ ↑n) = 1

theorem Polynomial.Chebyshev.roots_U_real_nodup (n : ℕ) : (Multiset.map (fun (k : ℕ) => Real.cos ((↑k + 1) * Real.pi / (↑n + 1))) (Multiset.range n)).Nodup

theorem Polynomial.Chebyshev.roots_U_real (n : ℕ) : (U ℝ ↑n).roots = (Finset.image (fun (k : ℕ) => Real.cos ((↑k + 1) * Real.pi / (↑n + 1))) (Finset.range n)).val

theorem Polynomial.Chebyshev.rootMultiplicity_U_real {n k : ℕ} (hk : k < n) : rootMultiplicity (Real.cos ((↑k + 1) * Real.pi / (↑n + 1))) (U ℝ ↑n) = 1

theorem Polynomial.Chebyshev.isLocalMax_T_real {n k : ℕ} (hn : n ≠ 0) (hk₀ : 0 < k) (hk₁ : k < n) (hk₂ : Even k) : IsLocalMax (fun (x : ℝ) => eval x (T ℝ ↑n)) (Real.cos (↑k * Real.pi / ↑n))

theorem Polynomial.Chebyshev.isLocalMin_T_real {n k : ℕ} (hn : n ≠ 0) (hk₁ : k < n) (hk₂ : Odd k) : IsLocalMin (fun (x : ℝ) => eval x (T ℝ ↑n)) (Real.cos (↑k * Real.pi / ↑n))

theorem Polynomial.Chebyshev.isLocalExtr_T_real {n k : ℕ} (hn : n ≠ 0) (hk₀ : 0 < k) (hk₁ : k < n) : IsLocalExtr (fun (x : ℝ) => eval x (T ℝ ↑n)) (Real.cos (↑k * Real.pi / ↑n))

theorem Polynomial.Chebyshev.isLocalExtr_T_real_iff {n : ℕ} (hn : 2 ≤ n) (x : ℝ) : IsLocalExtr (fun (x : ℝ) => eval x (T ℝ ↑n)) x ↔ ∃ k ∈ Finset.Ioo 0 n, x = Real.cos (↑k * Real.pi / ↑n)

theorem Polynomial.Chebyshev.isMaxOn_T_real {n k : ℕ} (hn : n ≠ 0) (hk₁ : k ≤ n) (hk₂ : Even k) : IsMaxOn (fun (x : ℝ) => eval x (T ℝ ↑n)) (Set.Icc (-1) 1) (Real.cos (↑k * Real.pi / ↑n))

theorem Polynomial.Chebyshev.isMinOn_T_real {n k : ℕ} (hn : n ≠ 0) (hk₁ : k ≤ n) (hk₂ : Odd k) : IsMinOn (fun (x : ℝ) => eval x (T ℝ ↑n)) (Set.Icc (-1) 1) (Real.cos (↑k * Real.pi / ↑n))

theorem Polynomial.Chebyshev.isExtrOn_T_real {n k : ℕ} (hn : n ≠ 0) (hk : k ≤ n) : IsExtrOn (fun (x : ℝ) => eval x (T ℝ ↑n)) (Set.Icc (-1) 1) (Real.cos (↑k * Real.pi / ↑n))

theorem Polynomial.Chebyshev.isExtrOn_T_real_iff {n : ℕ} (hn : n ≠ 0) {x : ℝ} (hx : x ∈ Set.Icc (-1) 1) : IsExtrOn (fun (x : ℝ) => eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x ↔ ∃ k ≤ n, x = Real.cos (↑k * Real.pi / ↑n)

theorem Polynomial.Chebyshev.irrational_of_isRoot_T_real {n : ℕ} {x : ℝ} (hroot : (T ℝ ↑n).IsRoot x) (hnz : x ≠ 0) : Irrational x

theorem Polynomial.Chebyshev.abs_iterate_derivative_T_real_le (n : ℤ) (k : ℕ) {x : ℝ} (hx : |x| ≤ 1) : |eval x ((⇑derivative)^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ n))