Constant Term Varies with Theta
StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.PolynomialConstruction
Statement
For $N > 0$, there exist $\theta_1, \theta_2 \in \mathbb{R}$ such that the constant term of $S_N(x;\theta_1)$ differs from that of $S_N(x;\theta_2)$.
theorem scaledPolynomial_constantTerm_varies (N : ℕ) (hN_pos : 0 < N) :
∃ θ₁ θ₂ : ℝ, scaledPolynomial_coeff N θ₁ 0 ≠ scaledPolynomial_coeff N θ₂ 0 := by
Proof
Case analysis on small $N$ (explicit witnesses) and for $N \ge 7$ use $\theta = 0$ (where $\cos\theta = 1 \ne 0$ keeps the constant term nonzero) versus $\theta = \pi/2$ (where $\cos(\pi/2) = 0$ is a root, forcing the constant term to zero).
obtain ⟨N', rfl⟩ := Nat.exists_eq_succ_of_ne_zero (Nat.pos_iff_ne_zero.mp hN_pos)
cases N' with
| zero =>
use 0, Real.pi / 2
unfold scaledPolynomial_coeff scaledPolynomial unscaledPolynomial polynomialFromRealRoots
rw [Polynomial.coeff_C_mul, Polynomial.coeff_C_mul]
simp only [realProjectionsList, zero_add]
norm_num
| succ N'' =>
cases N'' with
| zero =>
use Real.pi / 2, 0
unfold scaledPolynomial_coeff scaledPolynomial unscaledPolynomial polynomialFromRealRoots
rw [Polynomial.coeff_C_mul, Polynomial.coeff_C_mul]
simp only [realProjectionsList]
have h_range : List.range 2 = [0, 1] := by rfl
simp only [h_range]
norm_num [Real.cos_pi_div_two, Real.cos_zero, Real.cos_pi]
| succ N''' =>
cases N''' with
| zero =>
use 0, Real.pi / 2
unfold scaledPolynomial_coeff scaledPolynomial unscaledPolynomial polynomialFromRealRoots
rw [Polynomial.coeff_C_mul, Polynomial.coeff_C_mul]
simp only [realProjectionsList]
have h_range : List.range 3 = [0, 1, 2] := by rfl
simp only [h_range]
norm_num [Real.cos_pi_div_two, Real.cos_zero, Real.cos_pi]
constructor
· intro h
rw [Real.cos_eq_zero_iff] at h
obtain ⟨k, hk⟩ := h
have eq1 : (4 : ℝ) = 3 * (2 * (k : ℝ) + 1) := by
have h3 := congr_arg (· * 6) hk
field_simp at h3; norm_num at h3; exact h3
have eq2 : (1 : ℝ) = 6 * (k : ℝ) := by linarith
have eq3 : (k : ℝ) = 1 / 6 := by field_simp at eq2; linarith
have hk_pos : (0 : ℝ) < (k : ℝ) := by linarith [show (0 : ℝ) < 1 / 6 by norm_num]
have hk_lt_one : (k : ℝ) < 1 := by linarith [show (1 / 6 : ℝ) < 1 by norm_num]
have : (0 : ℤ) < k := by exact_mod_cast hk_pos
have : k < (1 : ℤ) := by exact_mod_cast hk_lt_one
omega
· intro h
rw [Real.cos_eq_zero_iff] at h
obtain ⟨k, hk⟩ := h
have eq1 : (8 : ℝ) = 3 * (2 * (k : ℝ) + 1) := by
have h3 := congr_arg (· * 6) hk
field_simp at h3; norm_num at h3; exact h3
have eq2 : (5 : ℝ) = 6 * (k : ℝ) := by linarith
have eq3 : (k : ℝ) = 5 / 6 := by field_simp at eq2; linarith
have hk_pos : (0 : ℝ) < (k : ℝ) := by linarith [show (0 : ℝ) < 5 / 6 by norm_num]
have hk_lt_one : (k : ℝ) < 1 := by linarith [show (5 / 6 : ℝ) < 1 by norm_num]
have : (0 : ℤ) < k := by exact_mod_cast hk_pos
have : k < (1 : ℤ) := by exact_mod_cast hk_lt_one
omega
| succ N'''' =>
cases N'''' with
| zero =>
use 0, Real.pi / 8
unfold scaledPolynomial_coeff scaledPolynomial unscaledPolynomial polynomialFromRealRoots
rw [Polynomial.coeff_C_mul, Polynomial.coeff_C_mul]
simp only [realProjectionsList]
have h_range : List.range 4 = [0, 1, 2, 3] := by rfl
simp only [h_range]
norm_num [Real.cos_zero, Real.cos_pi, Real.cos_pi_div_two, Real.cos_pi_div_eight]
have h_left : Real.cos (2 * Real.pi / 4) *
(Real.cos (2 * Real.pi * 2 / 4) * Real.cos (2 * Real.pi * 3 / 4)) = 0 := by
have : 2 * Real.pi / 4 = Real.pi / 2 := by ring
rw [this, Real.cos_pi_div_two]; ring
rw [h_left]
intro h_eq
have h1 : Real.pi / 8 + 2 * Real.pi / 4 = 5 * Real.pi / 8 := by ring
have h2 : Real.pi / 8 + 2 * Real.pi * 2 / 4 = 9 * Real.pi / 8 := by ring
have h3 : Real.pi / 8 + 2 * Real.pi * 3 / 4 = 13 * Real.pi / 8 := by ring
rw [h1, h2, h3] at h_eq
have h_sqrt_ne_zero : √(2 + √2) / 2 ≠ 0 := by
apply div_ne_zero
· apply Real.sqrt_ne_zero'.mpr
have : (0 : ℝ) < 2 := by norm_num
have : (0 : ℝ) < √2 := by rw [Real.sqrt_pos]; norm_num
linarith
· norm_num
have h_cos_prod_zero : Real.cos (5 * Real.pi / 8) *
(Real.cos (9 * Real.pi / 8) * Real.cos (13 * Real.pi / 8)) = 0 := by
exact eq_zero_of_ne_zero_of_mul_left_eq_zero h_sqrt_ne_zero (Eq.symm h_eq)
cases mul_eq_zero.mp h_cos_prod_zero with
| inl h_cos1 =>
rw [Real.cos_eq_zero_iff] at h_cos1
obtain ⟨k, hk⟩ := h_cos1
have eq1 : (10 : ℝ) = 8 * (2 * (k : ℝ) + 1) := by
have h := congr_arg (· * 16) hk
field_simp at h; norm_num at h; exact h
have eq2 : (2 : ℝ) = 16 * (k : ℝ) := by linarith
have eq3 : (k : ℝ) = 1 / 8 := by field_simp at eq2; linarith
have hk_pos : (0 : ℝ) < (k : ℝ) := by linarith [show (0 : ℝ) < 1 / 8 by norm_num]
have hk_lt_one : (k : ℝ) < 1 := by linarith [show (1 / 8 : ℝ) < 1 by norm_num]
have : (0 : ℤ) < k := by exact_mod_cast hk_pos
have : k < (1 : ℤ) := by exact_mod_cast hk_lt_one
omega
| inr h_cos23 =>
cases mul_eq_zero.mp h_cos23 with
| inl h_cos2 =>
rw [Real.cos_eq_zero_iff] at h_cos2
obtain ⟨k, hk⟩ := h_cos2
have eq1 : (18 : ℝ) = 8 * (2 * (k : ℝ) + 1) := by
have h := congr_arg (· * 16) hk
field_simp at h; norm_num at h; exact h
have eq2 : (10 : ℝ) = 16 * (k : ℝ) := by linarith
have eq3 : (k : ℝ) = 5 / 8 := by field_simp at eq2; linarith
have hk_pos : (0 : ℝ) < (k : ℝ) := by linarith [show (0 : ℝ) < 5 / 8 by norm_num]
have hk_lt_one : (k : ℝ) < 1 := by linarith [show (5 / 8 : ℝ) < 1 by norm_num]
have : (0 : ℤ) < k := by exact_mod_cast hk_pos
have : k < (1 : ℤ) := by exact_mod_cast hk_lt_one
omega
| inr h_cos3 =>
rw [Real.cos_eq_zero_iff] at h_cos3
obtain ⟨k, hk⟩ := h_cos3
have eq1 : (26 : ℝ) = 8 * (2 * (k : ℝ) + 1) := by
have h := congr_arg (· * 16) hk
field_simp at h; norm_num at h; exact h
have eq2 : (18 : ℝ) = 16 * (k : ℝ) := by linarith
have eq3 : (k : ℝ) = 9 / 8 := by field_simp at eq2; linarith
have hk_gt_one : (1 : ℝ) < (k : ℝ) := by linarith [show (1 : ℝ) < 9 / 8 by norm_num]
have hk_lt_two : (k : ℝ) < 2 := by linarith [show (9 / 8 : ℝ) < 2 by norm_num]
have : (1 : ℤ) < k := by exact_mod_cast hk_gt_one
have : k < (2 : ℤ) := by exact_mod_cast hk_lt_two
omega
| succ N''''' =>
cases N''''' with
| zero =>
use 0, Real.pi / 2
unfold scaledPolynomial_coeff scaledPolynomial unscaledPolynomial
unfold polynomialFromRealRoots
rw [Polynomial.coeff_C_mul, Polynomial.coeff_C_mul]
simp only [realProjectionsList]
have h_range : List.range 5 = [0, 1, 2, 3, 4] := by rfl
simp only [h_range]
norm_num [Real.cos_pi_div_two, Real.cos_zero, Real.cos_pi]
constructor
· intro h
rw [Real.cos_eq_zero_iff] at h
obtain ⟨k, hk⟩ := h
have h_real : (4 : ℝ) = 5 * (2 * (k : ℝ) + 1) := by
have h3 := congr_arg (· * 10) hk
field_simp at h3; norm_num at h3; exact h3
have eq1 : (4 : ℤ) = 5 * (2 * k + 1) := by
have : ((4 : ℤ) : ℝ) = ((5 * (2 * k + 1) : ℤ) : ℝ) := by
push_cast; exact h_real
exact Int.cast_injective this
omega
· constructor
· intro h
rw [Real.cos_eq_zero_iff] at h
obtain ⟨k, hk⟩ := h
have h_real : (8 : ℝ) = 5 * (2 * (k : ℝ) + 1) := by
have h3 := congr_arg (· * 10) hk
field_simp at h3; norm_num at h3; exact h3
have eq1 : (8 : ℤ) = 5 * (2 * k + 1) := by
have : ((8 : ℤ) : ℝ) = ((5 * (2 * k + 1) : ℤ) : ℝ) := by
push_cast; exact h_real
exact Int.cast_injective this
omega
· constructor
· intro h
rw [Real.cos_eq_zero_iff] at h
obtain ⟨k, hk⟩ := h
have h_real : (12 : ℝ) = 5 * (2 * (k : ℝ) + 1) := by
have h3 := congr_arg (· * 10) hk
field_simp at h3; norm_num at h3; exact h3
have eq1 : (12 : ℤ) = 5 * (2 * k + 1) := by
have : ((12 : ℤ) : ℝ) = ((5 * (2 * k + 1) : ℤ) : ℝ) := by
push_cast; exact h_real
exact Int.cast_injective this
omega
· intro h
rw [Real.cos_eq_zero_iff] at h
obtain ⟨k, hk⟩ := h
have h_real : (16 : ℝ) = 5 * (2 * (k : ℝ) + 1) := by
have h3 := congr_arg (· * 10) hk
field_simp at h3; norm_num at h3; exact h3
have eq1 : (16 : ℤ) = 5 * (2 * k + 1) := by
have : ((16 : ℤ) : ℝ) = ((5 * (2 * k + 1) : ℤ) : ℝ) := by
push_cast; exact h_real
exact Int.cast_injective this
omega
| succ n6 =>
cases n6 with
| zero =>
-- N = 6: use θ=0 and θ=π/2
use 0, Real.pi / 2
unfold scaledPolynomial_coeff scaledPolynomial unscaledPolynomial
unfold polynomialFromRealRoots
rw [Polynomial.coeff_C_mul, Polynomial.coeff_C_mul]
simp only [realProjectionsList]
have h_range : List.range 6 = [0, 1, 2, 3, 4, 5] := by rfl
simp only [h_range]
norm_num [Real.cos_zero, Real.cos_pi, Real.cos_pi_div_two]
-- Need to show ¬cos(2πk/6) = 0 for k = 1,2,3,4,5
-- cos(2πk/6) = cos(πk/3)
-- k=1: cos(π/3) = 1/2 ≠ 0
-- k=2: cos(2π/3) = -1/2 ≠ 0
-- k=3: cos(π) = -1 ≠ 0
-- k=4: cos(4π/3) = -1/2 ≠ 0
-- k=5: cos(5π/3) = 1/2 ≠ 0
constructor
· intro h
-- cos(2π/6) = cos(π/3) = 1/2 ≠ 0
have h1 : Real.cos (2 * Real.pi / 6) = Real.cos (Real.pi / 3) := by
congr 1; field_simp; ring
have h2 : Real.cos (Real.pi / 3) = 1 / 2 := by norm_num
rw [h1, h2] at h
norm_num at h
· constructor
· intro h
have h1 : Real.cos (2 * Real.pi * 2 / 6) = Real.cos (2 * Real.pi / 3) := by
congr 1; field_simp; ring
rw [h1] at h
-- cos(2π/3) = cos(π - π/3) = -cos(π/3) = -1/2
have h2 : Real.cos (2 * Real.pi / 3) = -Real.cos (Real.pi / 3) := by
have : 2 * Real.pi / 3 = Real.pi - Real.pi / 3 := by field_simp; ring
rw [this, Real.cos_pi_sub]
have h3 : Real.cos (Real.pi / 3) = 1 / 2 := by norm_num
rw [h2, h3] at h
norm_num at h
· constructor
· intro h
have h1 : Real.cos (2 * Real.pi * 3 / 6) = Real.cos Real.pi := by
congr 1; field_simp; ring
rw [h1, Real.cos_pi] at h
norm_num at h
· constructor
· intro h
have h1 : Real.cos (2 * Real.pi * 4 / 6) = Real.cos (4 * Real.pi / 3) := by
congr 1; field_simp; ring
rw [h1] at h
-- cos(4π/3) = cos(π/3 + π) = -cos(π/3) = -1/2
have h2 : Real.cos (4 * Real.pi / 3) = -Real.cos (Real.pi / 3) := by
have : 4 * Real.pi / 3 = Real.pi / 3 + Real.pi := by field_simp; ring
rw [this, Real.cos_add_pi]
have h3 : Real.cos (Real.pi / 3) = 1 / 2 := by norm_num
rw [h2, h3] at h
norm_num at h
· intro h
have h1 : Real.cos (2 * Real.pi * 5 / 6) = Real.cos (5 * Real.pi / 3) := by
congr 1; field_simp; ring
rw [h1] at h
-- cos(5π/3) = cos(2π - π/3) = cos(π/3) = 1/2
have h2 : Real.cos (5 * Real.pi / 3) = Real.cos (Real.pi / 3) := by
have : 5 * Real.pi / 3 = 2 * Real.pi - Real.pi / 3 := by field_simp; ring
rw [this, Real.cos_two_pi_sub]
have h3 : Real.cos (Real.pi / 3) = 1 / 2 := by norm_num
rw [h2, h3] at h
norm_num at h
| succ n7 =>
-- N = (n7 + 1 + 1 + 1 + 1 + 1 + 1).succ = n7 + 7 ≥ 7
have N_eq : (n7 + 1 + 1 + 1 + 1 + 1 + 1).succ = n7 + 7 := by omega
by_cases h_odd : Odd (n7 + 7)
· -- Odd N ≥ 7: use helper lemma
rw [N_eq]
exact scaledPolynomial_constantTerm_varies_odd_ge_7 (n7 + 7) h_odd (by omega)
· -- Even N ≥ 7: use helper lemma
rw [N_eq]
have h_even : Even (n7 + 7) := Nat.even_or_odd (n7 + 7) |>.resolve_right h_odd
exact scaledPolynomial_constantTerm_varies_even_ge_7 (n7 + 7) h_even (by omega)
Dependencies (uses)
Dependents (used by)
NoneNeighborhood
Legend
Not Ready
Work in Progress
Sorry (theorems only)
Proven/Defined
Fully Proven (theorems only)
Axiom
Mathlib Ready
Theorems/Lemmas
Definitions
Axioms