Legend
Not Ready
Work in Progress
Sorry (theorems only)
Proven/Defined
Fully Proven (theorems only)
Axiom
Mathlib Ready
Theorems/Lemmas
Definitions
Axioms
Filter
def:rotated_roots Rotated Roots of Unity def:realProjectionsList Real Projections List def:unscaled_poly Polynomial from Real Roots def:unscaledPolynomial Unscaled Polynomial def:scaled_poly Scaled Polynomial def:constantTermFormula Constant Term Formula def:chebyshevConstantTerm Chebyshev Constant Term def:explicitConstant Explicit Constant c(N, θ) def:scaledPolynomial-coeff Scaled Polynomial Coefficient Accessor def:chebyshevRoot Chebyshev Root def:chebyshevRootsList Chebyshev Roots List lem:sum_cos_phi_vanishes Sum of Cosines at Equally-Spaced Angles lem:list-foldr-eq-multiset-prod List Foldr Equals Multiset Product lem:sum_cos_m_phi_vanishes Cosine Sum at Integer Multiples Vanishes lem:cos-cube-formula Cubic Cosine Power Reduction lem:realProjection-eq-cos Real Projection Equals Cosine lem:realProjection-mem-Icc Real Projections Lie in [-1,1] lem:card-realProjectionsList Cardinality of Real Projections List lem:realProjection-mem-list Real Projection Membership lem:realProjectionsList-sum Real Projections List Sum lem:realProjectionsList-powersum Real Projections Power Sum lem:polynomialFromRealRoots-eval-mem Polynomial Vanishes at Its Roots lem:polynomialFromRealRoots-degree Degree Equals Number of Roots lem:unscaledPolynomial-degree Unscaled Polynomial Degree lem:scaledPolynomial-degree Scaled Polynomial Degree lem:unscaledPolynomial-monic Unscaled Polynomial Is Monic lem:scaledPolynomial-leadingCoeff Scaled Polynomial Leading Coefficient lem:polynomialFromRealRoots-eval-zero Polynomial Vanishes at Zero Iff Zero Is a Root lem:realProjectionsList-mem-cos-theta Cosine Theta in Projections List lem:cos-two-pi-k-div-odd-N-ne-zero Nonvanishing Cosine at Odd Roots lem:realProjectionsList-theta-zero-no-zero No Zero in Projections at Theta Zero lem:scaledPolynomial-constantTerm-varies Constant Term Varies with Theta lem:cos-four-formula Quartic Cosine Power Reduction lem:cos-five-mul Quintuple-Angle Formula lem:cos-five-formula Quintic Cosine Power Reduction lem:cos-six-formula Sextic Cosine Power Reduction lem:cos-ten-formula Degree-10 Cosine Power Reduction lem:sum-pow-primitive-root-mul Vanishing Sum of Rotated Powers lem:sum-primitive-root-pow-mul Geometric Sum of Primitive Root Powers lem:sum-cos-int-multiple-vanishes Integer Multiple Cosine Sum Vanishes lem:cos-as-exp Cosine via Complex Exponentials lem:exp-add-exp-pow Binomial Expansion of Exponential Sum lem:sum-cos-pow-eq-sum-binomial Power Sum as Binomial Cosine Sum lem:sum-cos-pow-theta-independent Power Sum Theta-Independence lem:power_sum_invariance Power Sum Invariance lem:fin-univ-map-get Fin Universe Map Recovers List lem:fin-sum-eq-multiset-sum Indexed Sum Equals Multiset Sum thm:newton_identities Newton's Identities for Multisets lem:flatMap-singleton-cast FlatMap Singleton Cast Simplification lem:esymm-eq-of-psum-eq Equal Power Sums Imply Equal Symmetric Functions cor:power_sums_determine_coefficients Equal Symmetric Functions Imply Equal Coefficients lem:multiset-esymm-one-eq-sum First Symmetric Function Is Sum lem:multiset-coe-realProjectionsList-sum Multiset Sum of Real Projections lem:multiset-powersum-realProjectionsList Multiset Power Sum of Real Projections lem:esymm_invariant Elementary Symmetric Functions of Rotated Roots Are Invariant thm:coefficients_independent Coefficient Independence Theorem lem:chebyshev-T-degree Chebyshev Polynomial Degree lem:scaledPolynomial-degree-eq-chebyshev Scaled Polynomial Degree Equals Chebyshev Degree lem:unscaledPolynomial-eval-at-projection Unscaled Polynomial Vanishes at Projected Roots lem:scaledPolynomial-eval-at-projection Scaled Polynomial Vanishes at Projected Roots lem:chebyshev-eval-cos Chebyshev Evaluation at Cosine lem:chebyshevRoot-in-Icc Chebyshev Roots in [-1, 1] lem:chebyshev-T-eval-chebyshevRoot Chebyshev Roots Are Roots of T_N lem:chebyshevRoots-distinct Distinctness of Chebyshev Roots lem:chebyshev-T-eval-eq-zero-forward Forward Direction: Roots of T_N Are Chebyshev Roots lem:chebyshev-T-eval-eq-zero-iff Full Root Characterization of Chebyshev Polynomials lem:sum-exp-chebyshev-angles Factoring Chebyshev Angle Exponentials lem:chebyshev_angle_sum_odd Odd Chebyshev Angle Sum Vanishes lem:cos-as-exp-chebyshev Cosine as Complex Exponential lem:exp-add-exp-pow-chebyshev Binomial Expansion of Exponential Sum lem:sum-cos-pow-chebyshev-binomial Chebyshev Angle Power Sum via Binomial Expansion lem:chebyshev_angle_sum_even Even Chebyshev Angle Sum Vanishes lem:binomial-terms-vanish-chebyshev Non-Constant Binomial Terms Vanish for Chebyshev Angles lem:rotated-roots-powersum-value Rotated Roots Power Sum Value lem:chebyshev_roots Chebyshev Roots Power Sum Value thm:power_sum_equality Power Sum Equality lem:chebyshev-T-leadingCoeff Leading Coefficient of Chebyshev T_N lem:scaledPolynomial-matches-chebyshev-at-zero Coefficient Matching at theta = 0 lem:scaledPolynomial-constantTerm-formula Scaled Polynomial Constant Term Formula lem:chebyshev-T-constantTerm Chebyshev Constant Term lem:explicitConstant-correct Explicit Constant Formula Correctness thm:main-statement Main Theorem Statement thm:main Proof of Main Theorem