Real Projections Power Sum

StatusFully Proven

TypeTheorem

ModuleChebyshevCircles.Proofs.RootsOfUnity

Statement

Theorem Real Projections Power Sum

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

theorem realProjectionsList_powersum (N : ℕ) (θ : ℝ) (j : ℕ) :
    ((realProjectionsList N θ).map (· ^ j)).sum =
    ∑ k ∈ Finset.range N, (Real.cos (θ + 2 * π * k / N)) ^ j := by

Proof ▼


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

Dependencies (uses)

Real Projections List

Dependents (used by)

Multiset Power Sum of Real Projections

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