Dependency Graph
83
Total
83
Fully Proven
0
Proven
0
Has Sorry
0
WIP
0
Not Ready
0
Axiom
0
Mathlib Ready
Ch 1: Introduction4 declarations
| Name | Status | Type | Module |
|---|---|---|---|
| Rotated Roots of Unity | Fully Proven | Definition | ChebyshevCircles.Definitions.Core |
| Polynomial from Real Roots | Fully Proven | Definition | ChebyshevCircles.Definitions.Core |
| Scaled Polynomial | Fully Proven | Definition | ChebyshevCircles.Definitions.Core |
| Proof of Main Theorem | Fully Proven | Theorem | ChebyshevCircles.ProofOfMainTheorem |
Ch 3: Discrete Orthogonality Relations2 declarations
| Name | Status | Type | Module |
|---|---|---|---|
| Odd Chebyshev Angle Sum Vanishes | Fully Proven | Theorem | ChebyshevCircles.Proofs.ChebyshevOrthogonality |
| Even Chebyshev Angle Sum Vanishes | Fully Proven | Theorem | ChebyshevCircles.Proofs.ChebyshevOrthogonality |
Ch 4: Power Sum Invariance1 declaration
| Name | Status | Type | Module |
|---|---|---|---|
| Power Sum Invariance | Fully Proven | Theorem | ChebyshevCircles.Proofs.PowerSums |
Ch 5: From Power Sums to Polynomial Coefficients1 declaration
| Name | Status | Type | Module |
|---|---|---|---|
| Coefficient Independence Theorem | Fully Proven | Theorem | ChebyshevCircles.Proofs.PolynomialProperties |
Ch 6: Proof of Main Theorem2 declarations
| Name | Status | Type | Module |
|---|---|---|---|
| Chebyshev Roots Power Sum Value | Fully Proven | Theorem | ChebyshevCircles.Proofs.PowerSumEquality |
| Power Sum Equality | Fully Proven | Theorem | ChebyshevCircles.Proofs.PowerSumEquality |
Other73 declarations
| Name | Status | Type | Module |
|---|---|---|---|
| Real Projections List | Fully Proven | Definition | ChebyshevCircles.Definitions.Core |
| Unscaled Polynomial | Fully Proven | Definition | ChebyshevCircles.Definitions.Core |
| Constant Term Formula | Fully Proven | Definition | ChebyshevCircles.Definitions.Core |
| Chebyshev Constant Term | Fully Proven | Definition | ChebyshevCircles.Definitions.Core |
| Explicit Constant c(N, θ) | Fully Proven | Definition | ChebyshevCircles.Definitions.Core |
| Scaled Polynomial Coefficient Accessor | Fully Proven | Abbrev | ChebyshevCircles.Definitions.Core |
| Chebyshev Root | Fully Proven | Definition | ChebyshevCircles.Definitions.ChebyshevRoots |
| Chebyshev Roots List | Fully Proven | Definition | ChebyshevCircles.Definitions.ChebyshevRoots |
| Sum of Cosines at Equally-Spaced Angles | Fully Proven | Theorem | ChebyshevCircles.Proofs.TrigonometricIdentities |
| List Foldr Equals Multiset Product | Fully Proven | Theorem | ChebyshevCircles.Proofs.TrigonometricIdentities |
| Cosine Sum at Integer Multiples Vanishes | Fully Proven | Theorem | ChebyshevCircles.Proofs.TrigonometricIdentities |
| Cubic Cosine Power Reduction | Fully Proven | Theorem | ChebyshevCircles.Proofs.TrigonometricIdentities |
| Real Projection Equals Cosine | Fully Proven | Theorem | ChebyshevCircles.Proofs.RootsOfUnity |
| Real Projections Lie in [-1,1] | Fully Proven | Theorem | ChebyshevCircles.Proofs.RootsOfUnity |
| Cardinality of Real Projections List | Fully Proven | Theorem | ChebyshevCircles.Proofs.RootsOfUnity |
| Real Projection Membership | Fully Proven | Theorem | ChebyshevCircles.Proofs.RootsOfUnity |
| Real Projections List Sum | Fully Proven | Theorem | ChebyshevCircles.Proofs.RootsOfUnity |
| Real Projections Power Sum | Fully Proven | Theorem | ChebyshevCircles.Proofs.RootsOfUnity |
| Polynomial Vanishes at Its Roots | Fully Proven | Theorem | ChebyshevCircles.Proofs.PolynomialConstruction |
| Degree Equals Number of Roots | Fully Proven | Theorem | ChebyshevCircles.Proofs.PolynomialConstruction |
| Unscaled Polynomial Degree | Fully Proven | Theorem | ChebyshevCircles.Proofs.PolynomialConstruction |
| Scaled Polynomial Degree | Fully Proven | Theorem | ChebyshevCircles.Proofs.PolynomialConstruction |
| Unscaled Polynomial Is Monic | Fully Proven | Theorem | ChebyshevCircles.Proofs.PolynomialConstruction |
| Scaled Polynomial Leading Coefficient | Fully Proven | Theorem | ChebyshevCircles.Proofs.PolynomialConstruction |
| Polynomial Vanishes at Zero Iff Zero Is a Root | Fully Proven | Theorem | ChebyshevCircles.Proofs.PolynomialConstruction |
| Cosine Theta in Projections List | Fully Proven | Theorem | ChebyshevCircles.Proofs.PolynomialConstruction |
| Nonvanishing Cosine at Odd Roots | Fully Proven | Theorem | ChebyshevCircles.Proofs.PolynomialConstruction |
| No Zero in Projections at Theta Zero | Fully Proven | Theorem | ChebyshevCircles.Proofs.PolynomialConstruction |
| Constant Term Varies with Theta | Fully Proven | Theorem | ChebyshevCircles.Proofs.PolynomialConstruction |
| Quartic Cosine Power Reduction | Fully Proven | Theorem | ChebyshevCircles.Proofs.PowerSums |
| Quintuple-Angle Formula | Fully Proven | Theorem | ChebyshevCircles.Proofs.PowerSums |
| Quintic Cosine Power Reduction | Fully Proven | Theorem | ChebyshevCircles.Proofs.PowerSums |
| Sextic Cosine Power Reduction | Fully Proven | Theorem | ChebyshevCircles.Proofs.PowerSums |
| Degree-10 Cosine Power Reduction | Fully Proven | Theorem | ChebyshevCircles.Proofs.PowerSums |
| Vanishing Sum of Rotated Powers | Fully Proven | Theorem | ChebyshevCircles.Proofs.PowerSums |
| Geometric Sum of Primitive Root Powers | Fully Proven | Theorem | ChebyshevCircles.Proofs.PowerSums |
| Integer Multiple Cosine Sum Vanishes | Fully Proven | Theorem | ChebyshevCircles.Proofs.PowerSums |
| Cosine via Complex Exponentials | Fully Proven | Theorem | ChebyshevCircles.Proofs.PowerSums |
| Binomial Expansion of Exponential Sum | Fully Proven | Theorem | ChebyshevCircles.Proofs.PowerSums |
| Power Sum as Binomial Cosine Sum | Fully Proven | Theorem | ChebyshevCircles.Proofs.PowerSums |
| Power Sum Theta-Independence | Fully Proven | Theorem | ChebyshevCircles.Proofs.PowerSums |
| Fin Universe Map Recovers List | Fully Proven | Theorem | ChebyshevCircles.Proofs.NewtonIdentities |
| Indexed Sum Equals Multiset Sum | Fully Proven | Theorem | ChebyshevCircles.Proofs.NewtonIdentities |
| Newton's Identities for Multisets | Fully Proven | Theorem | ChebyshevCircles.Proofs.NewtonIdentities |
| FlatMap Singleton Cast Simplification | Fully Proven | Theorem | ChebyshevCircles.Proofs.NewtonIdentities |
| Equal Power Sums Imply Equal Symmetric Functions | Fully Proven | Theorem | ChebyshevCircles.Proofs.NewtonIdentities |
| Equal Symmetric Functions Imply Equal Coefficients | Fully Proven | Theorem | ChebyshevCircles.Proofs.NewtonIdentities |
| First Symmetric Function Is Sum | Fully Proven | Theorem | ChebyshevCircles.Proofs.NewtonIdentities |
| Multiset Sum of Real Projections | Fully Proven | Theorem | ChebyshevCircles.Proofs.NewtonIdentities |
| Multiset Power Sum of Real Projections | Fully Proven | Theorem | ChebyshevCircles.Proofs.NewtonIdentities |
| Elementary Symmetric Functions of Rotated Roots Are Invariant | Fully Proven | Theorem | ChebyshevCircles.Proofs.NewtonIdentities |
| Chebyshev Polynomial Degree | Fully Proven | Theorem | ChebyshevCircles.Proofs.PolynomialProperties |
| Scaled Polynomial Degree Equals Chebyshev Degree | Fully Proven | Theorem | ChebyshevCircles.Proofs.PolynomialProperties |
| Unscaled Polynomial Vanishes at Projected Roots | Fully Proven | Theorem | ChebyshevCircles.Proofs.PolynomialProperties |
| Scaled Polynomial Vanishes at Projected Roots | Fully Proven | Theorem | ChebyshevCircles.Proofs.PolynomialProperties |
| Chebyshev Evaluation at Cosine | Fully Proven | Theorem | ChebyshevCircles.Proofs.PolynomialProperties |
| Chebyshev Roots in [-1, 1] | Fully Proven | Theorem | ChebyshevCircles.Proofs.ChebyshevRoots |
| Chebyshev Roots Are Roots of T_N | Fully Proven | Theorem | ChebyshevCircles.Proofs.ChebyshevRoots |
| Distinctness of Chebyshev Roots | Fully Proven | Theorem | ChebyshevCircles.Proofs.ChebyshevRoots |
| Forward Direction: Roots of T_N Are Chebyshev Roots | Fully Proven | Theorem | ChebyshevCircles.Proofs.ChebyshevRoots |
| Full Root Characterization of Chebyshev Polynomials | Fully Proven | Theorem | ChebyshevCircles.Proofs.ChebyshevRoots |
| Factoring Chebyshev Angle Exponentials | Fully Proven | Theorem | ChebyshevCircles.Proofs.ChebyshevOrthogonality |
| Cosine as Complex Exponential | Fully Proven | Theorem | ChebyshevCircles.Proofs.ChebyshevOrthogonality |
| Binomial Expansion of Exponential Sum | Fully Proven | Theorem | ChebyshevCircles.Proofs.ChebyshevOrthogonality |
| Chebyshev Angle Power Sum via Binomial Expansion | Fully Proven | Theorem | ChebyshevCircles.Proofs.ChebyshevOrthogonality |
| Non-Constant Binomial Terms Vanish for Chebyshev Angles | Fully Proven | Theorem | ChebyshevCircles.Proofs.ChebyshevOrthogonality |
| Rotated Roots Power Sum Value | Fully Proven | Theorem | ChebyshevCircles.Proofs.PowerSumEquality |
| Leading Coefficient of Chebyshev T_N | Fully Proven | Theorem | ChebyshevCircles.Proofs.MainTheoremSupport |
| Coefficient Matching at theta = 0 | Fully Proven | Theorem | ChebyshevCircles.Proofs.MainTheoremSupport |
| Scaled Polynomial Constant Term Formula | Fully Proven | Theorem | ChebyshevCircles.Proofs.MainTheoremSupport |
| Chebyshev Constant Term | Fully Proven | Theorem | ChebyshevCircles.Proofs.MainTheoremSupport |
| Explicit Constant Formula Correctness | Fully Proven | Theorem | ChebyshevCircles.Proofs.MainTheoremSupport |
| Main Theorem Statement | Fully Proven | Definition | ChebyshevCircles.MainTheorem |