Real Projections List Sum

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.RootsOfUnity

Statement

Theorem Real Projections List Sum
[blueprint]

$\sum \mathrm{realProjectionsList}(N, \theta) = \sum_{k=0}^{N-1} \cos(\theta + 2\pi k/N).$

theorem realProjectionsList_sum (N : ℕ) (θ : ℝ) :
    (realProjectionsList N θ).sum = ∑ k ∈ Finset.range N, Real.cos (θ + 2 * π * k / N) := by
Proof ▼ 


  rw [realProjectionsList]
  convert list_range_map_sum_eq_finset_sum N (fun k => Real.cos (θ + 2 * π * ↑k / ↑N)) using 2

Dependencies (uses)

Dependents (used by)

Neighborhood

Legend
Not Ready
Work in Progress
Sorry (theorems only)
Proven/Defined
Fully Proven (theorems only)
Axiom
Mathlib Ready
Theorems/Lemmas
Definitions
Axioms