Multiset Sum of Real Projections

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.NewtonIdentities

Statement

Theorem Multiset Sum of Real Projections
[blueprint]

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

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


  rw [Multiset.sum_coe, realProjectionsList_sum]

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