Proof step
Liu–Wang theorem for three-term recurrences
Theorem check of the sequence's own rule liu wang three term
- Concludes
- A skewed version of triangular array A122075.
- Premises
- none: a direct theorem check
- Theorem
- [LW07, Thm 2.1, Thm 2.3, Cor 2.4, Prop 3.3] polytool ?
- Lean
- RealRooted
route
windowRealRooted.threeTerm_interlaces_of_roots_mem_Icc - Checked
- polytool replayed · Lean not attempted
Technical details
- Step id
e-e6a995064f37abd4· JSON- Operation
- Theorem check of the sequence's own rule
{ "operation": "theorem_check", "theorem": "liu_wang_three_term" } - Claims
{ "claim": "real_rooted", "from_index": 0, "region": { "lower": { "closed": true, "value": "-1" }, "upper": { "closed": true, "value": "0" } } }{ "claim": "interlacing", "from_index": 1, "kind": "weak", "orientation": "previous_interlaces_next" }- Certificate
theorem_check, SHA-25606aab5178290c5c2d2b50ee51b77b7d009e8ca91b0fffac7e223765851195b30, 4,943 bytes (1,361 compressed); downloadpolytool replayed the certificate when the step was written.- Cited by
n-540fd96c9759fa70(real_rooted)n-540fd96c9759fa70(one_signed_coefficients)n-540fd96c9759fa70(hadamard_kernel)n-540fd96c9759fa70(interlacing)
References
- [LW07] Lily L. Liu and Yi Wang. A unified approach to polynomial sequences with only real zeros. Advances in Applied Mathematics, 38(4):542–560, May 2007. doi:10.1016/j.aam.2006.02.003