Updated name of chebyshevNode and removed hypothesis from node_lt

Author: YuvalFilmus

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

@@ -30,26 +30,26 @@ namespace Polynomial.Chebyshev
 
 open Polynomial Real
 
-/-- For `n ≠ 0` and `i ≤ n`, chebyshevNode n i is one of the extremal points of the Chebyhsev T
+/-- For `n ≠ 0` and `i ≤ n`, node n i is one of the extremal points of the Chebyhsev T
 polynomial over the interval `[-1, 1]`. -/
-noncomputable abbrev chebyshevNode (n i : ℕ) : ℝ := cos (i * π / n)
+noncomputable def node (n i : ℕ) : ℝ := cos (i * π / n)
 
-lemma chebyshevNode_eq_one {n : ℕ} : chebyshevNode n 0 = 1 := by simp [chebyshevNode]
+lemma node_eq_one {n : ℕ} : node n 0 = 1 := by simp [node]
 
-lemma chebyshevNode_eq_neg_one {n : ℕ} (hn : n ≠ 0) : chebyshevNode n n = -1 := by
+lemma node_eq_neg_one {n : ℕ} (hn : n ≠ 0) : node n n = -1 := by
   have : n * π / n = π := by aesop
-  simp [chebyshevNode, this]
+  simp [node, this]
 
-lemma chebyshevNode_mem_Icc {n i : ℕ} : chebyshevNode n i ∈ Set.Icc (-1) 1 :=
+lemma node_mem_Icc {n i : ℕ} : node n i ∈ Set.Icc (-1) 1 :=
   Set.mem_Icc.mpr ⟨neg_one_le_cos _, cos_le_one _⟩
 
-lemma eval_T_real_chebyshevNode {n i : ℕ} (hn : n ≠ 0) :
-    (T ℝ n).eval (chebyshevNode n i) = (-1) ^ i := by
+lemma eval_T_real_node {n i : ℕ} (hn : n ≠ 0) :
+    (T ℝ n).eval (node n i) = (-1) ^ i := by
   have : (n : ℤ) * (i * π / n) = i * π := by norm_cast; field
-  rw [T_real_cos, this, cos_nat_mul_pi]
+  rw [node, T_real_cos, this, cos_nat_mul_pi]
 
-lemma strictAntiOn_chebyshevNode (n : ℕ) :
-    StrictAntiOn (chebyshevNode n ·) (Finset.range (n + 1)) := by
+lemma strictAntiOn_node (n : ℕ) :
+    StrictAntiOn (node n ·) (Finset.range (n + 1)) := by
   wlog! hn : n ≠ 0
   · simp [hn]
   refine strictAntiOn_cos.comp_strictMonoOn ?_ (fun x hx => Set.mem_Icc.mpr ⟨by positivity, ?_⟩)
@@ -61,25 +61,24 @@ lemma strictAntiOn_chebyshevNode (n : ℕ) :
   nth_rewrite 2 [← mul_div_cancel₀ π (Nat.cast_ne_zero.mpr hn)]
   exact mul_le_mul_of_nonneg_right (Nat.cast_le.mpr hx) (by positivity)
 
-lemma chebyshevNode_lt {n i j : ℕ} (hi : i ≤ n) (hj : j ≤ n) (hij : i < j) :
-    chebyshevNode n j < chebyshevNode n i :=
-  (strictAntiOn_chebyshevNode n) (Finset.mem_coe.mpr (Finset.mem_range_succ_iff.mpr hi))
+lemma node_lt {n i j : ℕ} (hj : j ≤ n) (hij : i < j) :
+    node n j < node n i :=
+  (strictAntiOn_node n) (Finset.mem_coe.mpr (Finset.mem_range_succ_iff.mpr (by grind)))
     (Finset.mem_coe.mpr (Finset.mem_range_succ_iff.mpr hj)) hij
 
-lemma zero_lt_prod_chebyshevNode_sub_chebyshevNode {n i : ℕ} (hi : i ≤ n) :
-    0 < (-1) ^ i * ∏ j ∈ (Finset.range (n + 1)).erase i, (chebyshevNode n i - chebyshevNode n j) :=
+lemma 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) :=
     by
   wlog! hn : n ≠ 0
   · replace hi : i = 0 := Nat.le_zero.mp (le_of_le_of_eq hi hn)
     simp [hn, hi]
-  have h₁ : 0 < ∏ j ∈ Finset.range i, ((-1) * (chebyshevNode n i - chebyshevNode n j)) :=
+  have h₁ : 0 < ∏ j ∈ Finset.range i, ((-1) * (node n i - node n j)) :=
     Finset.prod_pos (fun j hj => mul_pos_of_neg_of_neg neg_one_lt_zero <| sub_neg.mpr <|
-    chebyshevNode_lt (le_trans (le_of_lt <| Finset.mem_range.mp hj) hi) hi
-    (Finset.mem_range.mp hj))
+    node_lt hi (Finset.mem_range.mp hj))
   rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range] at h₁
-  have h₂ : 0 < ∏ j ∈ Finset.Ioc i n, (chebyshevNode n i - chebyshevNode n j) :=
+  have h₂ : 0 < ∏ j ∈ Finset.Ioc i n, (node n i - node n j) :=
     Finset.prod_pos (fun j hj => sub_pos.mpr <|
-      chebyshevNode_lt hi (Finset.mem_Ioc.mp hj).2 (Finset.mem_Ioc.mp hj).1)
+      node_lt (Finset.mem_Ioc.mp hj).2 (Finset.mem_Ioc.mp hj).1)
   have union : (Finset.range (n + 1)).erase i = (Finset.range i) ∪ Finset.Ioc i n := by grind
   have disjoint : Disjoint (Finset.range i) (Finset.Ioc i n) := by grind [Finset.disjoint_iff_ne]
   rw [union, Finset.prod_union disjoint, ← mul_assoc]
@@ -96,98 +95,98 @@ private lemma negOnePow_mul_le {α : ℝ} {i : ℕ} (hα : α ∈ Set.Icc (-1) 1
   exact abs_le.mpr hα
 
 theorem apply_le_apply_T_real {n : ℕ} {param : ℝ[X] → ℝ} {c : ℕ → ℝ}
-    (hparam : (P : ℝ[X]) → P.degree = n → param P = ∑ i ≤ n, P.eval (chebyshevNode n i) * (c i))
+    (hparam : (P : ℝ[X]) → P.degree = n → param P = ∑ i ≤ n, P.eval (node n i) * (c i))
     (hcnonneg : ∀ i ≤ n, 0 ≤ (-1) ^ i * (c i))
     {P : ℝ[X]} (hPdeg : P.degree = n) (hPbnd : ∀ x ∈ Set.Icc (-1) 1, P.eval x ∈ Set.Icc (-1) 1) :
     param P ≤ param (T ℝ n) := by
   wlog! hn : n ≠ 0
   · rw [hparam P hPdeg, hparam (T ℝ n) (degree_T ℝ n), hn, show Finset.Iic 0 = {0} by rfl,
-      Nat.cast_zero, T_zero, Finset.sum_singleton, Finset.sum_singleton, chebyshevNode_eq_one,
+      Nat.cast_zero, T_zero, Finset.sum_singleton, Finset.sum_singleton, node_eq_one,
       eval_one]
     exact mul_le_mul_of_nonneg_right (hPbnd 1 (by simp) |> Set.mem_Icc.mp).2
       (le_of_le_of_eq (hcnonneg 0 n.zero_le) (one_mul _))
   calc
-    param P = ∑ i ≤ n, P.eval (chebyshevNode n i) * (c i) := hparam P hPdeg
-    _ ≤ ∑ i ≤ n, (T ℝ n).eval (chebyshevNode n i) * (c i) := by
+    param P = ∑ i ≤ n, P.eval (node n i) * (c i) := hparam P hPdeg
+    _ ≤ ∑ i ≤ n, (T ℝ n).eval (node n i) * (c i) := by
       refine Finset.sum_le_sum (fun i hi => ?_)
       calc
-        P.eval (chebyshevNode n i) * (c i) =
-          ((-1) ^ i * P.eval (chebyshevNode n i)) * ((-1) ^ i * (c i)) :=
+        P.eval (node n i) * (c i) =
+          ((-1) ^ i * P.eval (node n i)) * ((-1) ^ i * (c i)) :=
           negOnePow_mul_negOnePow_mul_cancel.symm
         _ ≤ 1 * ((-1) ^ i * (c i)) :=
-          mul_le_mul_of_nonneg_right (negOnePow_mul_le (hPbnd _ chebyshevNode_mem_Icc))
+          mul_le_mul_of_nonneg_right (negOnePow_mul_le (hPbnd _ node_mem_Icc))
           (hcnonneg i (Finset.mem_Iic.mp hi))
-        _ = (T ℝ n).eval (chebyshevNode n i) * (c i) := by
-          rw [eval_T_real_chebyshevNode hn, one_mul]
+        _ = (T ℝ n).eval (node n i) * (c i) := by
+          rw [eval_T_real_node hn, one_mul]
     _ = param (T ℝ n) := (hparam (T ℝ n) (degree_T ℝ n)).symm
 
 theorem apply_eq_apply_T_real_iff {n : ℕ} {param : ℝ[X] → ℝ} {c : ℕ → ℝ}
-    (hparam : (P : ℝ[X]) → P.degree = n → param P = ∑ i ≤ n, P.eval (chebyshevNode n i) * (c i))
+    (hparam : (P : ℝ[X]) → P.degree = n → param P = ∑ i ≤ n, P.eval (node n i) * (c i))
     (hcpos : ∀ i ≤ n, 0 < (-1) ^ i * (c i))
     {P : ℝ[X]} (hPdeg : P.degree = n) (hPbnd : ∀ x ∈ Set.Icc (-1) 1, P.eval x ∈ Set.Icc (-1) 1) :
     (param P = param (T ℝ n)) ↔ P = T ℝ n := by
   refine ⟨fun h => ?_, by intro h; rw [h]⟩
   wlog! hn : n ≠ 0
   · rw [hparam P hPdeg, hparam (T ℝ n) (degree_T ℝ n), hn, show Finset.Iic 0 = {0} by rfl,
-      Nat.cast_zero, T_zero, Finset.sum_singleton, Finset.sum_singleton, chebyshevNode_eq_one,
+      Nat.cast_zero, T_zero, Finset.sum_singleton, Finset.sum_singleton, node_eq_one,
       eval_one, one_mul] at h
     rw [hn, Nat.cast_zero] at hPdeg
     rw [hn, Nat.cast_zero, T_zero]
     have eval_P_one : P.eval 1 = 1 :=
       (mul_eq_right₀ (ne_of_lt <| lt_of_lt_of_eq (hcpos 0 n.zero_le) (one_mul _)).symm).mp h
     rw [eq_C_of_degree_eq_zero hPdeg, eval_C] at eval_P_one
     rw [eq_C_of_degree_eq_zero hPdeg, eval_P_one, C_1]
-  apply eq_of_degrees_lt_of_eval_finset_eq ((Finset.range (n + 1)).image (chebyshevNode n ·))
-  · rw [hPdeg, Nat.cast_lt, Finset.card_image_of_injOn (strictAntiOn_chebyshevNode n).injOn,
+  apply eq_of_degrees_lt_of_eval_finset_eq ((Finset.range (n + 1)).image (node n ·))
+  · rw [hPdeg, Nat.cast_lt, Finset.card_image_of_injOn (strictAntiOn_node n).injOn,
       Finset.card_range, Nat.lt_succ_iff]
   · rw [degree_T, Int.natAbs_natCast, Nat.cast_lt,
-      Finset.card_image_of_injOn (strictAntiOn_chebyshevNode n).injOn,
+      Finset.card_image_of_injOn (strictAntiOn_node n).injOn,
       Finset.card_range, Nat.lt_succ_iff]
   rw [hparam P hPdeg, hparam (T ℝ n) (degree_T ℝ n)] at h
   replace h := ge_of_eq h
   contrapose! h
   obtain ⟨x, hx, hPx⟩ := h
   obtain ⟨i, hi, hix⟩ := Finset.mem_image.mp hx
   replace hi := Finset.mem_Iic.mpr (Finset.mem_range_succ_iff.mp hi)
-  suffices  ∑ i ≤ n, ((-1) ^ i * P.eval (chebyshevNode n i)) * ((-1) ^ i * c i) <
-    ∑ i≤ n, ((-1) ^ i * (T ℝ n).eval (chebyshevNode n i)) * ((-1) ^ i * c i) by
+  suffices  ∑ i ≤ n, ((-1) ^ i * P.eval (node n i)) * ((-1) ^ i * c i) <
+    ∑ i≤ n, ((-1) ^ i * (T ℝ n).eval (node n i)) * ((-1) ^ i * c i) by
     simp_rw [negOnePow_mul_negOnePow_mul_cancel] at this
     exact this
   have h_le {i : ℕ} (hi : i ∈ Finset.Iic n) :
-    (-1) ^ i * P.eval (chebyshevNode n i) * ((-1) ^ i * c i) ≤
-    (-1) ^ i * (T ℝ n).eval (chebyshevNode n i)  * ((-1) ^ i * c i) := by
+    (-1) ^ i * P.eval (node n i) * ((-1) ^ i * c i) ≤
+    (-1) ^ i * (T ℝ n).eval (node n i)  * ((-1) ^ i * c i) := by
     refine mul_le_mul_of_nonneg_right ?_ (le_of_lt (hcpos i (Finset.mem_Iic.mp hi)))
-    rw [eval_T_real_chebyshevNode hn, ← neg_pow', neg_neg, one_pow]
-    exact negOnePow_mul_le (hPbnd _ chebyshevNode_mem_Icc)
+    rw [eval_T_real_node hn, ← neg_pow', neg_neg, one_pow]
+    exact negOnePow_mul_le (hPbnd _ node_mem_Icc)
   refine Finset.sum_lt_sum (fun i hi => h_le hi) ⟨i, hi, lt_of_le_of_ne (h_le hi) ?_⟩
   have := ne_of_lt (hcpos i (Finset.mem_Iic.mp hi))
   grind => ring
 
-theorem leadingCoeff_eq_sum_chebyshevNode (n : ℕ) (P : ℝ[X]) (hP : P.degree = n) :
-    P.leadingCoeff = ∑ i ≤ n, (P.eval (chebyshevNode n i)) *
-    (∏ j ∈ (Finset.range (n + 1)).erase i, (chebyshevNode n i - chebyshevNode n j))⁻¹ := by
-  rw [Lagrange.leadingCoeff_eq_sum (strictAntiOn_chebyshevNode n).injOn (by simp [hP]),
+theorem leadingCoeff_eq_sum_node (n : ℕ) (P : ℝ[X]) (hP : P.degree = n) :
+    P.leadingCoeff = ∑ i ≤ n, (P.eval (node n i)) *
+    (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ := by
+  rw [Lagrange.leadingCoeff_eq_sum (strictAntiOn_node n).injOn (by simp [hP]),
     show Finset.range (n + 1) = Finset.Iic n by grind]
   rfl
 
-theorem leadingCoeff_eq_sum_chebyshevNode_coeff_pos {n i : ℕ} (hi : i ≤ n) :
+theorem leadingCoeff_eq_sum_node_coeff_pos {n i : ℕ} (hi : i ≤ n) :
     0 < (-1) ^ i *
-    (∏ j ∈ (Finset.range (n + 1)).erase i, (chebyshevNode n i - chebyshevNode n j))⁻¹ := by
-  have := inv_pos_of_pos <| zero_lt_prod_chebyshevNode_sub_chebyshevNode hi
+    (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ := by
+  have := inv_pos_of_pos <| zero_lt_prod_node_sub_node hi
   rwa [mul_inv, ← inv_pow, inv_neg_one] at this
 
 theorem leadingCoeff_le_of_bounded {n : ℕ} {P : ℝ[X]}
     (hPdeg : P.degree = n) (hPbnd : ∀ x ∈ Set.Icc (-1) 1, P.eval x ∈ Set.Icc (-1) 1) :
     P.leadingCoeff ≤ 2 ^ (n - 1) := by
-  convert apply_le_apply_T_real (leadingCoeff_eq_sum_chebyshevNode n)
-    (fun i hi => le_of_lt <| leadingCoeff_eq_sum_chebyshevNode_coeff_pos hi) hPdeg hPbnd
+  convert apply_le_apply_T_real (leadingCoeff_eq_sum_node n)
+    (fun i hi => le_of_lt <| leadingCoeff_eq_sum_node_coeff_pos hi) hPdeg hPbnd
   simp
 
 theorem leadingCoeff_eq_iff_of_bounded {n : ℕ} {P : ℝ[X]}
     (hPdeg : P.degree = n) (hPbnd : ∀ x ∈ Set.Icc (-1) 1, P.eval x ∈ Set.Icc (-1) 1) :
     P.leadingCoeff = 2 ^ (n - 1) ↔ P = T ℝ n := by
-  convert apply_eq_apply_T_real_iff (leadingCoeff_eq_sum_chebyshevNode n)
-    (fun i hi => leadingCoeff_eq_sum_chebyshevNode_coeff_pos hi) hPdeg hPbnd
+  convert apply_eq_apply_T_real_iff (leadingCoeff_eq_sum_node n)
+    (fun i hi => leadingCoeff_eq_sum_node_coeff_pos hi) hPdeg hPbnd
   simp
 
 end Polynomial.Chebyshev