Proof step
Three-term recurrence criterion
Theorem check of the sequence's own rule three term recurrence
- Concludes
- Triangle read by rows: T(n,0)=1, T(n,n)=2, T(n,m) = T(n-1,m-1) + Sum_{k=0..m} T(n-1-k,m-k).
- Premises
- none: a direct theorem check
- Theorem
- [Sze39, §3.3; Fav35] polytool ?
- Checked
- polytool replayed · Lean not attempted
Technical details
- Step id
e-6cc9c42d16d0f5eb· JSON- Operation
- Theorem check of the sequence's own rule
{ "operation": "theorem_check", "theorem": "three_term_recurrence" } - Claims
{ "claim": "real_rooted", "from_index": 0, "region": {} }- Certificate
theorem_check, SHA-256e6723667bf232746ed1eb0a7ec2ed90226efd42471eae307437b59243c8e2168, 3,605 bytes (1,201 compressed); downloadpolytool replayed the certificate when the step was written.- Cited by
n-2496e2f555756362(real_rooted)
References
- [Fav35] Jean Favard. Sur les polynômes de tchebicheff. C. R. Acad. Sci. Paris, 200:2052–2053, 1935.
- [Sze39] G. Szegő. Orthogonal Polynomials. Colloquium publications, American Mathematical Society, 1939. doi:10.1090/coll/023