Real-rooted atlas

Proof step

Three-term recurrence criterion

Theorem check of the sequence's own rule three term recurrence

Concludes
Riordan array ((1-x)/(1+x), x/(1+x)^2).
Premises
none: a direct theorem check
Theorem
[Sze39, §3.3; Fav35] polytool ?
Checked
polytool replayed · Lean not attempted
Technical details
Step id
e-341476417f780961 · JSON
Operation
Theorem check of the sequence's own rule
{
  "operation": "theorem_check",
  "theorem": "three_term_recurrence"
}
Claims
{
  "claim": "real_rooted",
  "from_index": 1,
  "region": {}
}
{
  "claim": "interlacing",
  "from_index": 3,
  "kind": "strict",
  "orientation": "previous_interlaces_next"
}
Certificate
theorem_check, SHA-256 16b51e87082d756cef403d96adf8c6f11d048caed7104a5d930f3821394f6530, 3,514 bytes (1,162 compressed); download
polytool replayed the certificate when the step was written.
Cited by

References

  1. [Fav35] Jean Favard. Sur les polynômes de tchebicheff. C. R. Acad. Sci. Paris, 200:2052–2053, 1935.
  2. [Sze39] G. Szegő. Orthogonal Polynomials. Colloquium publications, American Mathematical Society, 1939. doi:10.1090/coll/023