{"chains":[{"edge":{"id":"e-350a04ce6807ec04","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"euler_polynomial\",\"coefficients\":[{\"numerator\":[\"1\"],\"denominator\":[\"1\"]},{\"numerator\":[\"2\"],\"denominator\":[\"1\"]},{\"numerator\":[\"1\"],\"denominator\":[\"1\"]}]}"},"operation_detail":"euler_polynomial, shift 0","conclusion_id":"n-8ecfb16735d608fb","premise_count":1,"theorem":"Laguerre's theorem on multiplier sequences: if f is a real polynomial whose roots are all real and <= 0, then (f(k))_(k >= 0) is a multiplier sequence, so x^k -> f(k) x^k maps every real-rooted polynomial to a real-rooted polynomial or zero (Laguerre; see T. Craven and G. Csordas, Multiplier sequences for fields, Illinois J. Math. 21 (1977); Polya--Schur, Theorem 40 of P. Branden, arXiv:1410.6601: sum_k f(k) x^k / k! = f(theta) e^x = C e^x x^m prod (1 + x/a_j), a_j > 0); f(k) has one sign for k >= 0, so coefficients of one sign stay of one sign; applied to f(n, .) for each n","lean_route":null,"lean_declarations":["RealRooted.isMultiplierSequence_eval_of_roots_nonpos","RealRooted.isPFMultiplierSequence_eval_of_roots_nonpos","RealRooted.isMultiplierSequence_iff_preserves"],"certificate_hash":"6c7a9ec0f2ab562a497ff241fc7495442a97118356bd0a7b5491b3cb05f787bc","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}}],"premises":[{"position":0,"node_id":"n-98c21bd2a6c7c1d4","role":"sequence","name":"basis_map_A013611 of Triangle read by rows: T(n,k) is the number of binary words of length n having degree of asymmetry equal to k (n >= 0; 0 <= k <= n/2).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-98c21bd2a6c7c1d4","role":"sequence","name":"basis_map_A013611 of Triangle read by rows: T(n,k) is the number of binary words of length n having degree of asymmetry equal to k (n >= 0; 0 <= k <= n/2).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 0]"},"chains":[{"edge":{"id":"e-6f6524a2909f4dfb","operation":{"map":"A013611","operation":"basis_map"},"operation_detail":"A013611","conclusion_id":"n-98c21bd2a6c7c1d4","premise_count":1,"theorem":"geometric family P_k = g(t) (a + d t)^k: T(p) = g(t) p(a + d t), so the roots of T(p) are those of g and the points (r - a)/d for the roots r of p (elementary)","lean_route":null,"lean_declarations":[],"certificate_hash":"6db3588ae686c2a2f048e03613bc5537aba12c714352650b76e3a685acac5285","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}}],"premises":[{"position":0,"node_id":"n-b6aca576a689e9f0","role":"sequence","name":"Triangle read by rows: T(n,k) is the number of binary words of length n having degree of asymmetry equal to k (n >= 0; 0 <= k <= n/2).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-b6aca576a689e9f0","role":"sequence","name":"Triangle read by rows: T(n,k) is the number of binary words of length n having degree of asymmetry equal to k (n >= 0; 0 <= k <= n/2).","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 0]"},"chains":[{"edge":{"id":"e-37ac46811d9937f6","operation":{"operation":"theorem_check","theorem":"iterated_preserver"},"operation_detail":"iterated_preserver","conclusion_id":"n-b6aca576a689e9f0","premise_count":0,"theorem":"Iterated real-rootedness preservers (induction on n): if P_m is nonzero and real-rooted with every root in a closed region R and, for every n > m, P_n = a_n(x) S_n(P_(n-1)) where S_n maps every polynomial that is zero or real-rooted with every root in R to zero or a real-rooted polynomial with every root in R and a_n is real-rooted with every root in R, then every P_n is real-rooted with every root in R (the roots of a product are the roots of its factors); an exact degree step keeps every row nonzero; here S_n is the identity; with lag L = 2, the induction runs in each residue class of n modulo L from its start row","lean_route":null,"lean_declarations":[],"certificate_hash":"37abffe6d51a5af3c35ba77ae8ec4cf2896fa7c72979192b4c7830e96829bcf4","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}}],"premises":[]},"premises":[]},{"edge":{"id":"e-ec4171dcd40223e2","operation":{"operation":"parent_provers","route":"periodic_product"},"operation_detail":"periodic_product","conclusion_id":"n-b6aca576a689e9f0","premise_count":0,"theorem":"polytool parent provers, route periodic_product: every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","lean_route":null,"lean_declarations":[],"certificate_hash":"cecf50e7d2eb681bca4e709c9f22b8e25ed468794c823de9e0f6102019224f88","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}}],"premises":[]},"premises":[]}]}]}]}]}],"truncated":false,"expanded":4}