Finished results regarding eval_iterate_derivative

Author: YuvalFilmus

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

@@ -20,10 +20,14 @@ public import Mathlib.Topology.Algebra.Polynomial
 
 ## Main statements
 
-* `leadingCoeff_le_of_bounded`: If P is a degree n polynomial and |P(x)|≤1 for all |x|≤ 1 then
+* `leadingCoeff_le_of_bounded`: If P is a degree n polynomial and |P(x)|≤1 for all |x|≤1 then
   the leading coefficient of P is at most 2^(n-1)
-* `leadingCoeff_eq_iff_of_bounded`: If P is a degree n polynomial and |P(x)|≤1 for all |x|≤ 1 then
-  the leading coefficient of P equals 2^(n-1) iff it is the n'th Chebyshev polynomial
+* `leadingCoeff_eq_iff_of_bounded`: If P is a degree n polynomial and |P(x)|≤1 for all |x|≤1 then
+  the leading coefficient of P equals 2^(n-1) iff P = T_n, the n'th Chebyshev polynomial
+* `eval_iterate_derivative_le_of_bounded`: If P is a degree n polynomial and |P(x)|≤1 for all |x|≤1
+  then for all x≥1 and all 0≠k≤n, P^(k)(x) ≤ T_n^(k)(x)
+* `eval_iterate_derivative_eq_iff_of_bounded`: If P is a degree n polynomial and |P(x)|≤1 for all
+  |x|≤1 then for all 0≠k≤n, P^(k)(x) = T_n^(k)(x) iff P = T_n
 -/
 @[expose] public section
 namespace Polynomial.Chebyshev
@@ -190,15 +194,61 @@ theorem leadingCoeff_eq_iff_of_bounded {n : ℕ} {P : ℝ[X]}
     (fun i hi => leadingCoeff_eq_sum_chebyshevNode_coeff_pos hi) hPdeg hPbnd
   simp
 
-theorem eval_iterate_derivative_eq_sum_chebshevNode {n k : ℕ} (hk : k ≤ n) (x : ℝ)
+theorem eval_iterate_derivative_eq_sum_chebyshevNode {n k : ℕ} (hk : k ≤ n) (x : ℝ)
     (P : ℝ[X]) (hP : P.degree = n) :
-    (derivative^[k] P).eval x = k.factorial *
+    (derivative^[k] P).eval x =
       ∑ i ≤ n, P.eval (chebyshevNode n i) *
-        ((∏ j ∈ (Finset.range (n + 1)).erase i, ((chebyshevNode n i) - (chebyshevNode n j)))⁻¹ *
+        (k.factorial *
+        (∏ j ∈ (Finset.range (n + 1)).erase i, ((chebyshevNode n i) - (chebyshevNode n j)))⁻¹ *
         ∑ t ∈ ((Finset.range (n + 1)).erase i).powerset with t.card = n - k,
         ∏ a ∈ t, (x - chebyshevNode n a)) := by
   rw [Lagrange.eval_iterate_derivative_eq_sum (strictAntiOn_chebyshevNode n).injOn (by simp [hP])
-    hk x]
-  sorry
+    (le_of_le_of_eq (Nat.cast_le.mpr hk) hP.symm) x, Finset.mul_sum, Finset.card_range,
+    Nat.add_sub_add_right, show Finset.range (n + 1) = Finset.Iic n by grind]
+  congr! 1 with i hi
+  ring
+
+theorem eval_iterate_derivative_eq_sum_chebyshevNode_coeff_pos
+    {n k i : ℕ} (hk₁ : 0 < k) (hk₂ : k ≤ n) (hi : i ≤ n) {x : ℝ} (hx : 1 ≤ x) :
+    0 < (-1) ^ i *
+      (k.factorial *
+      (∏ j ∈ (Finset.range (n + 1)).erase i, ((chebyshevNode n i) - (chebyshevNode n j)))⁻¹ *
+      ∑ t ∈ ((Finset.range (n + 1)).erase i).powerset with t.card = n - k,
+      ∏ a ∈ t, (x - chebyshevNode n a)) := by
+  rw [← mul_assoc]
+  refine mul_pos ?_ (Finset.sum_pos' ?_ ?_)
+  · rw [← mul_assoc, mul_comm (a := (-1) ^ i), mul_assoc]
+    exact mul_pos (Nat.cast_pos.mpr <| Nat.factorial_pos k)
+      (leadingCoeff_eq_sum_chebyshevNode_coeff_pos hi)
+  · refine fun t _ => Finset.prod_nonneg (fun a _ => ?_)
+    have : chebyshevNode n a ≤ 1 := cos_le_one _
+    linarith
+  · have : ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s := by
+      by_cases 1 ≤ i ∧ i ≤ n - k
+      case neg => exact ⟨Finset.Icc 1 (n - k), by grind, by grind [Nat.card_Icc], by simp⟩
+      case pos => exact ⟨(Finset.Icc 1 (n - k + 1)).erase i, by grind, by grind [Nat.card_Icc],
+        by simp⟩
+    obtain ⟨s, hs, hscard, hsn⟩ := this
+    refine ⟨s, by simp [hs, hscard], Finset.prod_pos (fun a ha => ?_)⟩
+    have : chebyshevNode n a < 1 := by
+      rw [← chebyshevNode_eq_one (n := n)]
+      apply chebyshevNode_lt (Nat.zero_le _) (by grind) (by grind)
+    linarith
+
+theorem eval_iterate_derivative_le_of_bounded {n : ℕ} {P : ℝ[X]}
+    {k : ℕ} (hk₁ : 0 < k) (hk₂ : k ≤ n) {x : ℝ} (hx : 1 ≤ x)
+    (hPdeg : P.degree = n) (hPbnd : ∀ x ∈ Set.Icc (-1) 1, P.eval x ∈ Set.Icc (-1) 1) :
+    (derivative^[k] P).eval x ≤ (derivative^[k] (T ℝ n)).eval x :=
+  apply_le_apply_T_real (eval_iterate_derivative_eq_sum_chebyshevNode hk₂ x)
+    (fun _ hi => le_of_lt <| eval_iterate_derivative_eq_sum_chebyshevNode_coeff_pos hk₁ hk₂ hi hx)
+    hPdeg hPbnd
+
+theorem eval_iterate_derivative_eq_iff_of_bounded {n : ℕ} {P : ℝ[X]}
+    {k : ℕ} (hk₁ : 0 < k) (hk₂ : k ≤ n) {x : ℝ} (hx : 1 ≤ x)
+    (hPdeg : P.degree = n) (hPbnd : ∀ x ∈ Set.Icc (-1) 1, P.eval x ∈ Set.Icc (-1) 1) :
+    (derivative^[k] P).eval x = (derivative^[k] (T ℝ n)).eval x ↔ P = T ℝ n :=
+  apply_eq_apply_T_real_iff (eval_iterate_derivative_eq_sum_chebyshevNode hk₂ x)
+    (fun _ hi => eval_iterate_derivative_eq_sum_chebyshevNode_coeff_pos hk₁ hk₂ hi hx)
+    hPdeg hPbnd
 
 end Polynomial.Chebyshev