feat(Chebyshev/RootsExtrema): bound iterated derivatives of Chebyshev T on [-1, 1] (#34364)

Author: YuvalFilmus

Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean

@@ -21,10 +21,15 @@ import Mathlib.NumberTheory.Niven
 
 ## 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(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`
 -/
 
 public section
@@ -318,4 +323,23 @@ theorem irrational_of_isRoot_T_real {n : ℕ} {x : ℝ} (hroot : (T ℝ n).IsRoo
     Nat.eq_of_dvd_of_div_eq_one (Nat.gcd_dvd_left ..) (by grind [Rat.den_pos])) (by grind)
   rw_mod_cast [← hk₂, hn]; convert cos_pi_div_two using 2; push_cast; field_simp
 
+theorem abs_iterate_derivative_T_real_le (n : ℤ) (k : ℕ) {x : ℝ} (hx : |x| ≤ 1) :
+    |(derivative^[k] (T ℝ n)).eval x| ≤ (derivative^[k] (T ℝ n)).eval 1 := by
+  wlog hn : 0 ≤ n
+  · convert this (-n) k hx (by grind) using 1 <;> rw [T_neg]
+  lift n to ℕ using hn
+  have := T_iterate_derivative_mem_span_T (R := ℝ) n k
+  obtain ⟨f, hfsupp, hfderiv⟩ := Submodule.mem_span_set.mp this
+  replace hfderiv : ∑ p ∈ f.support, f p • p = derivative^[k] (T ℝ n) := by rw [← hfderiv]; rfl
+  have hf (y : ℝ) :
+      ∑ p ∈ f.support, f p • p.eval y = (derivative^[k] (T ℝ n)).eval y := by
+    rw [← hfderiv, Polynomial.eval_finset_sum]
+    simp_rw [Polynomial.eval_smul]
+  rw [← hf x, ← hf 1]
+  grw [Finset.abs_sum_le_sum_abs]
+  refine Finset.sum_le_sum (fun i hi => ?_)
+  obtain ⟨m, hm, hi⟩ := (Set.mem_image ..).mp (hfsupp hi)
+  grw [abs_nsmul, ← hi, abs_eval_T_real_le_one m hx]
+  simp
+
 end Polynomial.Chebyshev

Mathlib/RingTheory/Polynomial/Chebyshev.lean

@@ -10,6 +10,7 @@ public import Mathlib.Algebra.Polynomial.Derivative
 public import Mathlib.Algebra.Polynomial.Degree.Lemmas
 public import Mathlib.Algebra.Ring.NegOnePow
 public import Mathlib.Tactic.LinearCombination
+public import Mathlib.LinearAlgebra.Span.Basic
 
 /-!
 # Chebyshev polynomials
@@ -501,6 +502,24 @@ theorem T_eq_X_mul_U_sub_U (n : ℤ) : T R (n + 2) = X * U R (n + 1) - U R n :=
     show n + 2 + 1 - 2 = n + 1 by ring] at h
   linear_combination (norm := ring_nf) h
 
+theorem two_mul_T_eq_U_sub_U (n : ℤ) : 2 * T R (n + 2) = U R (n + 2) - U R n := by
+  linear_combination (norm := ring_nf) (T_eq_U_sub_X_mul_U R (n + 2)) + (T_eq_X_mul_U_sub_U R n)
+
+theorem U_eq_two_mul_T_add_U (n : ℤ) : U R (n + 2) = 2 * T R (n + 2) + U R n := by
+  linear_combination (norm := ring_nf) - (two_mul_T_eq_U_sub_U R n)
+
+theorem U_mem_span_T (n : ℕ) : U R n ∈ Submodule.span ℕ ((fun m : ℕ => T R m) '' Set.Icc 0 n) := by
+  induction n using Nat.twoStepInduction with
+  | zero => simp
+  | one =>
+    rw [show U R (1 : ℕ) = 2 * T R 1 by simp, ← smul_eq_mul]; norm_cast
+    exact Submodule.smul_of_tower_mem _ 2 (Submodule.mem_span_of_mem ⟨1, by simp⟩)
+  | more n h₀ _ =>
+    push_cast; rw [U_eq_two_mul_T_add_U, ← smul_eq_mul]; norm_cast
+    refine Submodule.add_mem _ ?_ ((Submodule.span_mono (by grind)) h₀)
+    · exact Submodule.smul_of_tower_mem _ 2
+        (Submodule.mem_span_of_mem ⟨n + 2, by simp⟩)
+
 /-- `C n` is the `n`th rescaled Chebyshev polynomial of the first kind (also known as a Vieta–Lucas
 polynomial), given by $C_n(2x) = 2T_n(x)$. See `Polynomial.Chebyshev.C_comp_two_mul_X`. -/
 noncomputable def C : ℤ → R[X]
@@ -865,6 +884,31 @@ theorem T_derivative_eq_U (n : ℤ) : derivative (T R n) = n * U R (n - 1) := by
     linear_combination (norm := (push_cast; ring_nf))
       -ih2 + 2 * (X : R[X]) * ih1 + h₁ + 2 * h₃ + (n + 1) * h₂
 
+theorem T_derivative_mem_span_T (n : ℕ) :
+    derivative (T R n) ∈ Submodule.span ℕ ((fun m : ℕ => T R m) '' Set.Ico 0 n) := by
+  by_cases! hn : n = 0
+  · simp [hn]
+  rw [T_derivative_eq_U, ← smul_eq_mul]; norm_cast
+  refine Submodule.smul_of_tower_mem _ n ?_
+  convert U_mem_span_T R (n - 1) using 2 <;> grind
+
+theorem T_iterate_derivative_mem_span_T (n k : ℕ) :
+    derivative^[k] (T R n) ∈ Submodule.span ℕ ((fun m : ℕ => T R m) '' Set.Icc 0 (n - k)) := by
+  induction k
+  case zero =>
+    rw [Function.iterate_zero_apply]
+    exact Submodule.mem_span_of_mem ⟨n, by simp⟩
+  case succ k ih =>
+    rw [Function.iterate_succ_apply']
+    suffices Submodule.span ℕ ((fun m : ℕ => derivative (T R m)) '' Set.Icc 0 (n - k)) ≤
+      Submodule.span ℕ ((fun m : ℕ => T R m) '' Set.Icc 0 (n - (k + 1))) by
+      apply this
+      convert Submodule.apply_mem_span_image_of_mem_span (derivative.restrictScalars ℕ) ih using 2
+      simp [Set.image]
+    refine Submodule.span_le.mpr (fun x hx => ?_)
+    obtain ⟨m, hm, rfl⟩ := hx
+    refine (Submodule.span_mono (by grind)) (T_derivative_mem_span_T (R := R) m)
+
 theorem one_sub_X_sq_mul_derivative_T_eq_poly_in_T (n : ℤ) :
     (1 - X ^ 2) * derivative (T R (n + 1)) = (n + 1 : R[X]) * (T R n - X * T R (n + 1)) := by
   have H₁ := one_sub_X_sq_mul_U_eq_pol_in_T R n