No Zero in Projections at Theta Zero

StatusFully Proven

TypeTheorem

ModuleChebyshevCircles.Proofs.PolynomialConstruction

Statement

Theorem No Zero in Projections at Theta Zero

For odd $N \ge 5$, $0 \notin \mathrm{realProjectionsList}(N, 0).$

theorem realProjectionsList_theta_zero_no_zero (N : ℕ) (hN_odd : Odd N) (hN_ge : N ≥ 5) :
    0 ∉ realProjectionsList N 0 := by

Proof ▼


  unfold realProjectionsList
  simp only [List.mem_map, not_exists, not_and, List.mem_range]
  intro k hk
  simp only [zero_add]
  by_cases h_zero : k = 0
  · rw [h_zero]
    simp [Real.cos_zero]
  · have hk_pos : 0 < k := Nat.pos_of_ne_zero h_zero
    exact cos_two_pi_k_div_odd_N_ne_zero N k hN_odd hN_ge hk_pos hk

Dependencies (uses)

Real Projections List
Nonvanishing Cosine at Odd Roots

Dependents (used by)

Constant Term Varies with Theta

Neighborhood

Depth: 1 / 1

Legend

Not Ready

Work in Progress

Sorry (theorems only)

Proven/Defined

Fully Proven (theorems only)

Axiom

Mathlib Ready

Theorems/Lemmas

Definitions

Axioms