Skip to content

Commit d4a03cf

Browse files
YuvalFilmusYuvalFilmus
committed
Part of file only involving leadingCoeff
1 parent 9fc4084 commit d4a03cf

2 files changed

Lines changed: 193 additions & 0 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2160,6 +2160,7 @@ public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
21602160
public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
21612161
public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev
21622162
public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
2163+
public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
21632164
public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
21642165
public import Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
21652166
public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

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

Lines changed: 192 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,192 @@
1+
/-
2+
Copyright (c) 2025 Yuval Filmus. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Yuval Filmus
5+
-/
6+
module
7+
8+
public import Mathlib.RingTheory.Polynomial.Chebyshev
9+
public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
10+
public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
11+
public import Mathlib.LinearAlgebra.Lagrange
12+
public import Mathlib.Topology.Algebra.Polynomial
13+
14+
/-!
15+
# Chebyshev polynomials over the reals: some extremal properties
16+
17+
* Chebyshev polynomials have largest leading coefficient,
18+
following proof in https://math.stackexchange.com/a/978145/1277
19+
20+
## Main statements
21+
22+
* `leadingCoeff_le_of_bounded`: If P is a degree n polynomial and |P(x)|≤1 for all |x|≤1 then
23+
the leading coefficient of P is at most 2^(n-1)
24+
* `leadingCoeff_eq_iff_of_bounded`: If P is a degree n polynomial and |P(x)|≤1 for all |x|≤1 then
25+
the leading coefficient of P equals 2^(n-1) iff P = T_n, the n'th Chebyshev polynomial
26+
-/
27+
@[expose] public section
28+
namespace Polynomial.Chebyshev
29+
30+
open Polynomial Real
31+
32+
/-- For n ≠ 0 and i ≤ n, `chebyshevNode n i` is one of the extremal points of the Chebyhsev T
33+
polynomial over the interval [-1, 1]. -/
34+
noncomputable abbrev chebyshevNode (n i : ℕ) : ℝ := cos (i * π / n)
35+
36+
lemma chebyshevNode_eq_one {n : ℕ} : chebyshevNode n 0 = 1 := by simp [chebyshevNode]
37+
38+
lemma chebyshevNode_eq_neg_one {n : ℕ} (hn : n ≠ 0) : chebyshevNode n n = -1 := by
39+
have : n * π / n = π := by aesop
40+
simp [chebyshevNode, this]
41+
42+
lemma chebyshevNode_mem_Icc {n i : ℕ} : chebyshevNode n i ∈ Set.Icc (-1) 1 :=
43+
Set.mem_Icc.mpr ⟨neg_one_le_cos _, cos_le_one _⟩
44+
45+
lemma eval_T_real_chebyshevNode {n i : ℕ} (hn : n ≠ 0) :
46+
(T ℝ n).eval (chebyshevNode n i) = (-1) ^ i := by
47+
have : (n : ℤ) * (i * π / n) = i * π := by norm_cast; field
48+
rw [T_real_cos, this, cos_nat_mul_pi]
49+
50+
lemma strictAntiOn_chebyshevNode (n : ℕ) :
51+
StrictAntiOn (chebyshevNode n ·) (Finset.range (n + 1)) := by
52+
wlog! hn : n ≠ 0
53+
· simp [hn]
54+
refine strictAntiOn_cos.comp_strictMonoOn ?_ (fun x hx => Set.mem_Icc.mpr ⟨by positivity, ?_⟩)
55+
· apply StrictMono.strictMonoOn
56+
exact StrictMono.mul_const
57+
(StrictMono.mul_const Nat.strictMono_cast (by positivity)) (by positivity)
58+
rw [Finset.mem_coe, Finset.mem_range_succ_iff] at hx
59+
rw [mul_div_assoc]
60+
nth_rewrite 2 [← mul_div_cancel₀ π (Nat.cast_ne_zero.mpr hn)]
61+
exact mul_le_mul_of_nonneg_right (Nat.cast_le.mpr hx) (by positivity)
62+
63+
lemma chebyshevNode_lt {n i j : ℕ} (hi : i ≤ n) (hj : j ≤ n) (hij : i < j) :
64+
chebyshevNode n j < chebyshevNode n i :=
65+
(strictAntiOn_chebyshevNode n) (Finset.mem_coe.mpr (Finset.mem_range_succ_iff.mpr hi))
66+
(Finset.mem_coe.mpr (Finset.mem_range_succ_iff.mpr hj)) hij
67+
68+
lemma zero_lt_prod_chebyshevNode_sub_chebyshevNode {n i : ℕ} (hi : i ≤ n) :
69+
0 < (-1) ^ i * ∏ j ∈ (Finset.range (n + 1)).erase i, (chebyshevNode n i - chebyshevNode n j) :=
70+
by
71+
wlog! hn : n ≠ 0
72+
· replace hi : i = 0 := Nat.le_zero.mp (le_of_le_of_eq hi hn)
73+
simp [hn, hi]
74+
have h₁ : 0 < ∏ j ∈ Finset.range i, ((-1) * (chebyshevNode n i - chebyshevNode n j)) :=
75+
Finset.prod_pos (fun j hj => mul_pos_of_neg_of_neg neg_one_lt_zero <| sub_neg.mpr <|
76+
chebyshevNode_lt (le_trans (le_of_lt <| Finset.mem_range.mp hj) hi) hi
77+
(Finset.mem_range.mp hj))
78+
rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range] at h₁
79+
have h₂ : 0 < ∏ j ∈ Finset.Ioc i n, (chebyshevNode n i - chebyshevNode n j) :=
80+
Finset.prod_pos (fun j hj => sub_pos.mpr <|
81+
chebyshevNode_lt hi (Finset.mem_Ioc.mp hj).2 (Finset.mem_Ioc.mp hj).1)
82+
have union : (Finset.range (n + 1)).erase i = (Finset.range i) ∪ Finset.Ioc i n := by grind
83+
have disjoint : Disjoint (Finset.range i) (Finset.Ioc i n) := by grind [Finset.disjoint_iff_ne]
84+
rw [union, Finset.prod_union disjoint, ← mul_assoc]
85+
exact mul_pos h₁ h₂
86+
87+
private lemma negOnePow_mul_negOnePow_mul_cancel {α β : ℝ} {i : ℕ} :
88+
((-1) ^ i * α) * ((-1) ^ i * β) = α * β := calc
89+
_ = ((-1) ^ i * (-1) ^ i) * α * β := by ring
90+
_ = α * β := by simp [← mul_pow]
91+
92+
private lemma negOnePow_mul_le {α : ℝ} {i : ℕ} (hα : α ∈ Set.Icc (-1) 1) : (-1) ^ i * α ≤ 1 := by
93+
apply le_of_abs_le
94+
rw [abs_mul, abs_neg_one_pow, one_mul]
95+
exact abs_le.mpr hα
96+
97+
theorem apply_le_apply_T_real {n : ℕ} {param : ℝ[X] → ℝ} {c : ℕ → ℝ}
98+
(hparam : (P : ℝ[X]) → P.degree = n → param P = ∑ i ≤ n, P.eval (chebyshevNode n i) * (c i))
99+
(hcnonneg : ∀ i ≤ n, 0 ≤ (-1) ^ i * (c i))
100+
{P : ℝ[X]} (hPdeg : P.degree = n) (hPbnd : ∀ x ∈ Set.Icc (-1) 1, P.eval x ∈ Set.Icc (-1) 1) :
101+
param P ≤ param (T ℝ n) := by
102+
wlog! hn : n ≠ 0
103+
· rw [hparam P hPdeg, hparam (T ℝ n) (degree_T ℝ n), hn, show Finset.Iic 0 = {0} by rfl,
104+
Nat.cast_zero, T_zero, Finset.sum_singleton, Finset.sum_singleton, chebyshevNode_eq_one,
105+
eval_one]
106+
exact mul_le_mul_of_nonneg_right (hPbnd 1 (by simp) |> Set.mem_Icc.mp).2
107+
(le_of_le_of_eq (hcnonneg 0 n.zero_le) (one_mul _))
108+
calc
109+
param P = ∑ i ≤ n, P.eval (chebyshevNode n i) * (c i) := hparam P hPdeg
110+
_ ≤ ∑ i ≤ n, (T ℝ n).eval (chebyshevNode n i) * (c i) := by
111+
refine Finset.sum_le_sum (fun i hi => ?_)
112+
calc
113+
P.eval (chebyshevNode n i) * (c i) =
114+
((-1) ^ i * P.eval (chebyshevNode n i)) * ((-1) ^ i * (c i)) :=
115+
negOnePow_mul_negOnePow_mul_cancel.symm
116+
_ ≤ 1 * ((-1) ^ i * (c i)) :=
117+
mul_le_mul_of_nonneg_right (negOnePow_mul_le (hPbnd _ chebyshevNode_mem_Icc))
118+
(hcnonneg i (Finset.mem_Iic.mp hi))
119+
_ = (T ℝ n).eval (chebyshevNode n i) * (c i) := by
120+
rw [eval_T_real_chebyshevNode hn, one_mul]
121+
_ = param (T ℝ n) := (hparam (T ℝ n) (degree_T ℝ n)).symm
122+
123+
theorem apply_eq_apply_T_real_iff {n : ℕ} {param : ℝ[X] → ℝ} {c : ℕ → ℝ}
124+
(hparam : (P : ℝ[X]) → P.degree = n → param P = ∑ i ≤ n, P.eval (chebyshevNode n i) * (c i))
125+
(hcpos : ∀ i ≤ n, 0 < (-1) ^ i * (c i))
126+
{P : ℝ[X]} (hPdeg : P.degree = n) (hPbnd : ∀ x ∈ Set.Icc (-1) 1, P.eval x ∈ Set.Icc (-1) 1) :
127+
(param P = param (T ℝ n)) ↔ P = T ℝ n := by
128+
refine ⟨fun h => ?_, by intro h; rw [h]⟩
129+
wlog! hn : n ≠ 0
130+
· rw [hparam P hPdeg, hparam (T ℝ n) (degree_T ℝ n), hn, show Finset.Iic 0 = {0} by rfl,
131+
Nat.cast_zero, T_zero, Finset.sum_singleton, Finset.sum_singleton, chebyshevNode_eq_one,
132+
eval_one, one_mul] at h
133+
rw [hn, Nat.cast_zero] at hPdeg
134+
rw [hn, Nat.cast_zero, T_zero]
135+
have eval_P_one : P.eval 1 = 1 :=
136+
(mul_eq_right₀ (ne_of_lt <| lt_of_lt_of_eq (hcpos 0 n.zero_le) (one_mul _)).symm).mp h
137+
rw [eq_C_of_degree_eq_zero hPdeg, eval_C] at eval_P_one
138+
rw [eq_C_of_degree_eq_zero hPdeg, eval_P_one, C_1]
139+
apply eq_of_degrees_lt_of_eval_finset_eq ((Finset.range (n + 1)).image (chebyshevNode n ·))
140+
· rw [hPdeg, Nat.cast_lt, Finset.card_image_of_injOn (strictAntiOn_chebyshevNode n).injOn,
141+
Finset.card_range, Nat.lt_succ_iff]
142+
· rw [degree_T, Int.natAbs_natCast, Nat.cast_lt,
143+
Finset.card_image_of_injOn (strictAntiOn_chebyshevNode n).injOn,
144+
Finset.card_range, Nat.lt_succ_iff]
145+
rw [hparam P hPdeg, hparam (T ℝ n) (degree_T ℝ n)] at h
146+
replace h := ge_of_eq h
147+
contrapose! h
148+
obtain ⟨x, hx, hPx⟩ := h
149+
obtain ⟨i, hi, hix⟩ := Finset.mem_image.mp hx
150+
replace hi := Finset.mem_Iic.mpr (Finset.mem_range_succ_iff.mp hi)
151+
suffices ∑ i ≤ n, ((-1) ^ i * P.eval (chebyshevNode n i)) * ((-1) ^ i * c i) <
152+
∑ i≤ n, ((-1) ^ i * (T ℝ n).eval (chebyshevNode n i)) * ((-1) ^ i * c i) by
153+
simp_rw [negOnePow_mul_negOnePow_mul_cancel] at this
154+
exact this
155+
have h_le {i : ℕ} (hi : i ∈ Finset.Iic n) :
156+
(-1) ^ i * P.eval (chebyshevNode n i) * ((-1) ^ i * c i) ≤
157+
(-1) ^ i * (T ℝ n).eval (chebyshevNode n i) * ((-1) ^ i * c i) := by
158+
refine mul_le_mul_of_nonneg_right ?_ (le_of_lt (hcpos i (Finset.mem_Iic.mp hi)))
159+
rw [eval_T_real_chebyshevNode hn, ← neg_pow', neg_neg, one_pow]
160+
exact negOnePow_mul_le (hPbnd _ chebyshevNode_mem_Icc)
161+
refine Finset.sum_lt_sum (fun i hi => h_le hi) ⟨i, hi, lt_of_le_of_ne (h_le hi) ?_⟩
162+
have := ne_of_lt (hcpos i (Finset.mem_Iic.mp hi))
163+
grind => ring
164+
165+
theorem leadingCoeff_eq_sum_chebyshevNode (n : ℕ) (P : ℝ[X]) (hP : P.degree = n) :
166+
P.leadingCoeff = ∑ i ≤ n, (P.eval (chebyshevNode n i)) *
167+
(∏ j ∈ (Finset.range (n + 1)).erase i, (chebyshevNode n i - chebyshevNode n j))⁻¹ := by
168+
rw [Lagrange.leadingCoeff_eq_sum (strictAntiOn_chebyshevNode n).injOn (by simp [hP]),
169+
show Finset.range (n + 1) = Finset.Iic n by grind]
170+
rfl
171+
172+
theorem leadingCoeff_eq_sum_chebyshevNode_coeff_pos {n i : ℕ} (hi : i ≤ n) :
173+
0 < (-1) ^ i *
174+
(∏ j ∈ (Finset.range (n + 1)).erase i, (chebyshevNode n i - chebyshevNode n j))⁻¹ := by
175+
have := inv_pos_of_pos <| zero_lt_prod_chebyshevNode_sub_chebyshevNode hi
176+
rwa [mul_inv, ← inv_pow, inv_neg_one] at this
177+
178+
theorem leadingCoeff_le_of_bounded {n : ℕ} {P : ℝ[X]}
179+
(hPdeg : P.degree = n) (hPbnd : ∀ x ∈ Set.Icc (-1) 1, P.eval x ∈ Set.Icc (-1) 1) :
180+
P.leadingCoeff ≤ 2 ^ (n - 1) := by
181+
convert apply_le_apply_T_real (leadingCoeff_eq_sum_chebyshevNode n)
182+
(fun i hi => le_of_lt <| leadingCoeff_eq_sum_chebyshevNode_coeff_pos hi) hPdeg hPbnd
183+
simp
184+
185+
theorem leadingCoeff_eq_iff_of_bounded {n : ℕ} {P : ℝ[X]}
186+
(hPdeg : P.degree = n) (hPbnd : ∀ x ∈ Set.Icc (-1) 1, P.eval x ∈ Set.Icc (-1) 1) :
187+
P.leadingCoeff = 2 ^ (n - 1) ↔ P = T ℝ n := by
188+
convert apply_eq_apply_T_real_iff (leadingCoeff_eq_sum_chebyshevNode n)
189+
(fun i hi => leadingCoeff_eq_sum_chebyshevNode_coeff_pos hi) hPdeg hPbnd
190+
simp
191+
192+
end Polynomial.Chebyshev

0 commit comments

Comments
 (0)