Multiset Power Sum of Real Projections

StatusFully Proven

TypeTheorem

ModuleChebyshevCircles.Proofs.NewtonIdentities

Statement

Theorem Multiset Power Sum of Real Projections

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

theorem multiset_powersum_realProjectionsList (N : ℕ) (θ : ℝ) (j : ℕ) :
    ((↑(realProjectionsList N θ) : Multiset ℝ).map (fun x => x ^ j)).sum =
    ∑ k ∈ Finset.range N, (Real.cos (θ + 2 * π * k / N)) ^ j := by

Proof ▼


  rw [Multiset.map_coe, Multiset.sum_coe, realProjectionsList_powersum]

Dependencies (uses)

Real Projections Power Sum

Dependents (used by)

Elementary Symmetric Functions of Rotated Roots Are Invariant
Coefficient Matching at theta = 0

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