Proved fundamental theorems

Author: YuvalFilmus

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

@@ -15,179 +15,153 @@ public import Mathlib.Topology.Algebra.Polynomial
 
 * Chebyshev polynomials minimize deviation from zero,
   following proof in https://math.stackexchange.com/a/978145/1277
+  [SWITCH TO STATEMENT]
+* Chebyshev polynomials maximize iterated derivatives at 1 and beyond, using similar idea
 
 ## Main statements
 
-* `le_sup_abs_eval_of_monic` provides a lower bound on the maximum of |P(x)| on [-1, 1] for monic P
-* `sup_abs_eval_eq_iff_of_monic` characterizes the equality case
+[STATEMENTS]
 -/
-
+@[expose] public section
 namespace Polynomial.Chebyshev
 
 open Polynomial Real
 
-lemma mem_Icc {n j : ℕ} (hn : n ≠ 0) (hj : j ∈ Finset.range (n + 1)) : j * π / n ∈ Set.Icc 0 π := by
-  refine ⟨by positivity, ?_⟩
-  · replace hj : (j : ℝ) ≤ n := Finset.mem_range.mp hj |> Nat.le_of_lt_succ |> Nat.cast_le.mpr
-    linear_combination (norm := (field_simp; ring_nf; rfl)) (π / n) * hj
-
-lemma prod_pos {n : ℕ} {i : ℕ} (hi : i ∈ Finset.range (n + 1)) :
-    0 < (-1) ^ i * ∏ j ∈ (Finset.range (n + 1)).erase i, (cos (i * π / n) - cos (j * π / n)) := by
-  by_cases n = 0
-  case pos hn => aesop
-  case neg hn =>
-  have h₁ : 0 < ∏ j ∈ Finset.range i, ((-1) * (cos (i * π / n) - cos (j * π / n))) := by
-    apply Finset.prod_pos
-    intro j hj
-    have : cos (i * π / n) < cos (j * π / n) := by
-      apply Real.strictAntiOn_cos (mem_Icc hn (by grind)) (mem_Icc hn hi)
-      have : (j : ℝ) < i := by aesop
-      linear_combination (π / n) * this
-    linarith
+/-- For n ≠ 0 and i ≤ n, `chebyshevNode 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)
+
+lemma chebyshevNode_eq_one {n : ℕ} : chebyshevNode n 0 = 1 := by simp [chebyshevNode]
+
+lemma chebyshevNode_eq_neg_one {n : ℕ} (hn : n ≠ 0) : chebyshevNode n n = -1 := by
+  have : n * π / n = π := by aesop
+  simp [chebyshevNode, this]
+
+lemma chebyshevNode_mem_Icc {n i : ℕ} : chebyshevNode 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
+  have : (n : ℤ) * (i * π / n) = i * π := by norm_cast; field
+  rw [T_real_cos, this, cos_nat_mul_pi]
+
+lemma strictAntiOn_chebyshevNode (n : ℕ) :
+    StrictAntiOn (chebyshevNode n ·) (Finset.range (n + 1)) := by
+  wlog hn : n ≠ 0
+  · push_neg at hn
+    simp [hn]
+  refine strictAntiOn_cos.comp_strictMonoOn ?_ (fun x hx => Set.mem_Icc.mpr ⟨by positivity, ?_⟩)
+  · apply StrictMono.strictMonoOn
+    exact StrictMono.mul_const
+      (StrictMono.mul_const Nat.strictMono_cast (by positivity)) (by positivity)
+  rw [Finset.mem_coe, Finset.mem_range_succ_iff] at hx
+  rw [mul_div_assoc]
+  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))
+    (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) :=
+    by
+  wlog hn : n ≠ 0
+  · push_neg at hn
+    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)) :=
+    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))
   rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range] at h₁
-  have h₂ : 0 < ∏ j ∈ Finset.Ioc i n, (cos (i * π / n) - cos (j * π / n)) := by
-    apply Finset.prod_pos
-    intro j hj
-    have : cos (j * π / n) < cos (i * π / n) := by
-      apply Real.strictAntiOn_cos (mem_Icc hn hi) (mem_Icc hn (by grind))
-      have : (i : ℝ) < j := by aesop
-      linear_combination (π / n) * this
-    linarith
+  have h₂ : 0 < ∏ j ∈ Finset.Ioc i n, (chebyshevNode n i - chebyshevNode 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)
   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]
   exact mul_pos h₁ h₂
 
-lemma leadingCoeff_formula {n : ℕ} (hn : n ≠ 0) {P : ℝ[X]} (hP : P.degree = n) :
-    ∃ (c : ℕ → ℝ),
-    (∀ i ∈ Finset.range (n + 1), 0 < c i) ∧
-    (∑ i ∈ Finset.range (n + 1), c i = 2 ^ (n - 1)) ∧
-    (∑ i ∈ Finset.range (n + 1), (c i) * ((-1) ^ i * P.eval (cos (i * π / n))) = P.leadingCoeff) :=
-    by
-  have cos_inj : Set.InjOn (fun (i : ℕ) => cos (i * π / n)) (Finset.range (n + 1)) := by
-    refine injOn_cos.comp ?_ (fun i hi => mem_Icc hn hi)
-    intro i hi j hj hij
-    suffices (i : ℝ) = j by norm_cast at this
-    linear_combination (norm := field) (n / π) * hij
-  have deg {Q : ℝ[X]} (hQ : Q.degree = n) : (Finset.range (n + 1)).card = Q.degree + 1 := by
-    simp [Finset.card_range, hQ]
-  use fun i =>
-    ((-1) ^ i * ∏ j ∈ (Finset.range (n + 1)).erase i, (cos (i * π / n) - cos (j * π / n)))⁻¹
-  refine ⟨?_, ⟨?_, ?_⟩⟩
-  · exact fun i hi => prod_pos hi |> inv_pos.mpr
-  · have := Lagrange.leadingCoeff_eq_sum cos_inj (deg (degree_T ℝ n))
-    rw [leadingCoeff_T, Int.natAbs_natCast] at this
-    rw [this]
-    congr! 1 with i hi
-    dsimp
-    have : ((n : ℤ) : ℝ) * (i * π / n) = (i : ℤ) * π := by norm_cast; field_simp
-    rw [T_real_cos, this, cos_int_mul_pi, zpow_natCast, mul_inv, ← div_eq_mul_inv, ← inv_pow,
-      inv_neg_one]
-  · rw [Lagrange.leadingCoeff_eq_sum cos_inj (deg hP)]
-    congr! 1 with i hi
-    field
-
-theorem bddAbove (P : ℝ[X]) : BddAbove { |P.eval x| | x ∈ Set.Icc (-1) 1 } :=
-  have := P.continuous
-  have hcont : ContinuousOn (fun x => |P.eval x|) (Set.Icc (-1) 1) :=
-    Continuous.continuousOn (by continuity)
-  IsCompact.bddAbove_image isCompact_Icc hcont
-
-lemma P_eval_bound (P : ℝ[X]) (n i : ℕ) :
-    (-1) ^ i * P.eval (cos (i * π / n)) ≤ sSup { |P.eval x| | x ∈ Set.Icc (-1) 1 } := by
-  suffices |P.eval (cos (i * π / n))| ≤ sSup { |P.eval x| | x ∈ Set.Icc (-1) 1 } by
-    cases neg_one_pow_eq_or ℝ i with
-    | inl h => rw [h, one_mul]; exact (abs_le'.mp this).1
-    | inr h => rw [h, neg_one_mul]; exact (abs_le'.mp this).2
-  refine le_csSup (bddAbove P) (Set.mem_setOf.mpr ⟨cos (i * π / n), ⟨?_, rfl⟩⟩)
-  exact Set.mem_Icc.mpr <| abs_le.mp <| abs_cos_le_one _
-
-end Polynomial.Chebyshev
-
-@[expose] public section
-
-namespace Polynomial.Chebyshev
-
-open Polynomial Real
-
-theorem le_sup_abs_eval_of_monic {n : ℕ} (hn : n ≠ 0)
-    {P : ℝ[X]} (Pdeg : P.degree = n) (Pmonic : P.Monic) :
-    1 / 2 ^ (n - 1) ≤ sSup { |P.eval x| | x ∈ Set.Icc (-1) 1 } := by
-  suffices 1 ≤ 2 ^ (n - 1) * sSup { |P.eval x| | x ∈ Set.Icc (-1) 1 } by field_simp; assumption
-  obtain ⟨c, hpos, hsum, hform⟩ := leadingCoeff_formula hn Pdeg
-  calc 1 = P.leadingCoeff := Pmonic.symm
-    _ = ∑ i ∈ Finset.range (n + 1), (c i) * ((-1)^i * P.eval (cos (i * π / n))) := hform.symm
-    _ ≤ ∑ i ∈ Finset.range (n + 1), (c i) * sSup { |P.eval x| | x ∈ Set.Icc (-1) 1 } := by
-      gcongr with i hi
-      · exact le_of_lt (hpos i hi)
-      · exact P_eval_bound P n i
-    _ = 2 ^ (n - 1) * sSup { |P.eval x| | x ∈ Set.Icc (-1) 1 } := by
-      rw [← Finset.sum_mul, hsum]
-
-theorem sup_abs_eval_eq_iff_of_monic {n : ℕ} (hn : n ≠ 0) (P : ℝ[X])
-    (Pdeg : P.degree = n) (Pmonic : P.Monic) :
-     sSup { |P.eval x| | x ∈ Set.Icc (-1) 1 } = 1 / 2 ^ (n - 1) ↔
-     P = (1 / 2 ^ (n - 1) : ℝ) • (T ℝ n) :=
-    by
-  constructor
-  case mp =>
-    intro hsSup
-    let extrema := (Finset.range (n + 1)).image (fun (k : ℕ) => cos (k * π / n))
-    have card_extrema : extrema.card = n + 1 := by
-      rw [Finset.card_image_of_injOn, Finset.card_range]
-      apply injOn_cos.comp (by aesop)
-      intro k hk
-      apply Set.mem_Icc.mpr
-      constructor
-      · positivity
-      · field_simp
-        norm_cast
-        grind
-    apply eq_of_degrees_lt_of_eval_finset_eq extrema
-    · rw [Pdeg, card_extrema]; norm_cast; simp
-    · rw [smul_eq_C_mul, degree_C_mul (by positivity), degree_T, card_extrema]
-      norm_cast; simp
-    obtain ⟨c, hpos, hsum, hform⟩ := leadingCoeff_formula hn Pdeg
-    rw [Pmonic] at hform
-    let T' := (1 / 2 ^ (n - 1) : ℝ) • (T ℝ n)
-    have Tform (i : ℕ) :
-        (-1) ^ i * T'.eval (cos (i * π / n)) = 1 / 2 ^ (n - 1) := by
-      have : ((n : ℤ) : ℝ) * (i * π / n) = (i : ℤ) * π := by norm_cast; field_simp
-      rw [eval_smul, smul_eq_mul, T_real_cos, this, cos_int_mul_pi]
-      suffices ((-1) ^ i : ℝ) * (-1) ^ (i : ℤ) = 1 by grind
-      simp [← sq, ← pow_mul']
-    replace hform :
-      ∑ i ∈ Finset.range (n + 1), (c i) * ((-1) ^ i * P.eval (cos (i * π / n))) =
-      ∑ i ∈ Finset.range (n + 1), (c i) * ((-1) ^ i * T'.eval (cos (i * π / n))) := by
-      simp_rw [hform, Tform, ← Finset.sum_mul, hsum]
-      simp
-    replace hform := ge_of_eq hform
-    contrapose! hform
-    obtain ⟨θ, hθ, hPθ⟩ := hform
-    obtain ⟨i₀, hi₀, hi₀θ⟩ := Finset.mem_image.mp hθ
-    have h_le {i : ℕ} (hi : i ∈ Finset.range (n + 1)) :
-      c i * ((-1) ^ i * P.eval (cos (i * π / n))) ≤
-      c i * ((-1) ^ i * T'.eval (cos (i * π / n))) := by
-      rw [Tform i, ← hsSup]
-      exact mul_le_mul_of_nonneg_left (P_eval_bound P n i) (le_of_lt (hpos i hi))
-    have h_lt₀ :
-      c i₀ * ((-1) ^ i₀ * P.eval (cos (i₀ * π / n))) <
-      c i₀ * ((-1) ^ i₀ * T'.eval (cos (i₀ * π / n))) := by
-      apply lt_of_le_of_ne (h_le hi₀)
-      rw [hi₀θ]
-      contrapose! hPθ
-      rw [← mul_assoc, ← mul_assoc] at hPθ
-      refine mul_left_cancel₀ ?_ hPθ
-      have := hpos i₀ hi₀
-      positivity
-    exact Finset.sum_lt_sum (fun i hi => h_le hi) ⟨i₀, hi₀, h_lt₀⟩
-  case mpr =>
-    intro hP
-    apply eq_of_le_of_ge
-    · refine csSup_le (by use |P.eval 1|; grind) (fun x hx => ?_)
-      obtain ⟨θ, hθ, hx⟩ := Set.mem_setOf.mp hx
-      have := (abs_eval_T_real_le_one_iff (Int.ofNat_ne_zero.mpr hn) θ).mp (abs_le.mpr hθ)
-      aesop
-    · refine le_csSup (bddAbove P) ⟨1, ⟨by grind, by aesop⟩⟩
+private lemma negOnePow_mul_negOnePow_mul_cancel {α β : ℝ} {i : ℕ} :
+    ((-1) ^ i * α) * ((-1) ^ i * β) = α * β := calc
+  _ = ((-1) ^ i * (-1) ^ i) * α * β := by ring
+  _ = α * β := by simp [← mul_pow]
+
+private lemma negOnePow_mul_le {α : ℝ} {i : ℕ} (hα : α ∈ Set.Icc (-1) 1) : (-1) ^ i * α ≤ 1 := by
+  apply le_of_abs_le
+  rw [abs_mul, abs_neg_one_pow, one_mul]
+  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))
+    (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
+  · push_neg at hn
+    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,
+      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
+      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)) :=
+          negOnePow_mul_negOnePow_mul_cancel.symm
+        _ ≤ 1 * ((-1) ^ i * (c i)) :=
+          mul_le_mul_of_nonneg_right (negOnePow_mul_le (hPbnd _ chebyshevNode_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]
+    _ = 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))
+    (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
+  · push_neg at hn
+    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,
+      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,
+      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_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
+    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
+    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)
+  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
 
 end Polynomial.Chebyshev