{"id":"n-7674f5b97866799a","revision":0,"first_index":0,"fingerprint":"f6-7ac044cd69385489","name":"mobius_x_over_x_plus_one of basis_map_A013610 of Exponential Riordan array (1, x(1+x/2)).","polytool_family":null,"interpretation":null,"rows_observed":15,"degree_pattern":"affine","degree_slope":1,"degree_intercept":0,"palindromic":0,"gamma_positive":0,"nonnegative":1,"rr_by_factors":false,"rows":[["1"],["1","4"],["2","13","20"],["4","39","120","112"],["10","124","555","1048","688"],["26","400","2375","6740","9040","4544"],["76","1374","10050","37835","76740","78864","31936"],["232","4858","42420","199325","541520","846048","700672","236800"],["764","18064","182420","1024072","3481625","7309456","9217376","6365440","1841408"],["2620","69264","795780","5200608","21240513","56043540","95231136","100229760","59196672","14943232"],["9496","276700","3555000","26459580","126027930","400330413","856625700","1216365600","1094958720","563749120","126063616"],["35696","1138324","16187600","135245220","736132980","2734927503","7062056232","12648464400","15373121280","12062040320","5496088576","1101983744"],["140152","4847088","75482220","698750800","4275117990","18178851636","54988050579","119005662600","182603163600","193498581760","134315334912","54824798208","9954734080"],["568504","21209344","359134620","3649517872","24795434950","118758202992","411878165127","1045739331780","1940989832496","2598169288000","2435894965504","1514053192704","559185203200","92714156032"],["2390480","95605384","1747589480","19328209628","144313917748","768482725010","3005687126442","8759849178795","19092534985524","30935110270064","36647443792960","30762778452224","17292818816000","5827402190848","888502796288"]],"degrees":[0,1,2,3,4,5,6,7,8,9,10,11,12,13,14],"row_sums":["1","5","35","275","2425","23125","236875","2571875","29440625","352953125","4414421875","57367421875","772423515625","10746208203125","154146098046875"],"nonn":true,"definitions":[{"position":0,"source":"derived:mobius_x_over_x_plus_one","source_kind":"derived","equality_edge_id":null,"recurrence":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"denominator":{"coeffs":[["3","3"]]},"terms":[{"coeff":{"coeffs":[["8","33","33","8"],["-5","-18","-21","-8"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["2","14","30","26","8"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"}}],"properties":[{"id":181302,"position":0,"claim":"real_rooted","from_index":0,"region_key":"[-1, 0]","provenance":"edges","claim_data":{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":true,"value":"-1"},"upper":{"closed":true,"value":"0"}}},"label":"Real-rooted","description":"Every row P_n, n >= 0, is zero or real-rooted with all roots in [-1, 0]","region_exact":null,"edges":["e-b59dfb75c0172ee2"]},{"id":181303,"position":1,"claim":"one_signed_coefficients","from_index":0,"region_key":null,"provenance":"derived_from_edges","claim_data":{"alternating":false,"claim":"one_signed_coefficients","from_index":0},"label":"Coefficients of one sign","description":"Every nonzero row, n >= 0: the coefficients of P_n have one sign","region_exact":null,"edges":["e-b59dfb75c0172ee2"]},{"id":181304,"position":2,"claim":"hadamard_kernel","from_index":0,"region_key":null,"provenance":"derived_from_edges","claim_data":{"claim":"hadamard_kernel","from_index":0},"label":"Hadamard kernel (Malo)","description":"Rows P_n, n >= 0, are Hadamard kernels (preserve real-rootedness)","region_exact":null,"edges":["e-b59dfb75c0172ee2"]}],"region_exact":{},"incoming_edges":[{"id":"e-b59dfb75c0172ee2","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"mobius\",\"a\":\"1\",\"b\":\"0\",\"c\":\"1\",\"e\":\"1\",\"schedule\":{\"first_index\":0,\"first_degree\":0,\"step\":1}}"},"operation_detail":"mobius, shift 0","conclusion_id":"n-7674f5b97866799a","premise_count":1,"theorem":"a real affine substitution x -> a x + b (a != 0), the reversal x^d p(1/x) (d >= deg p) and a real Mobius map (c x + e)^d p((a x + b)/(c x + e)) (a e - b c != 0, d >= deg p) map real roots to real roots: a root r of p gives the root (r - b)/a, 1/r (and 0) or (e r - b)/(a - c r) (and -e/c); for an input row that is a polynomial the degree condition holds automatically","lean_route":"fTransform","lean_declarations":["RealRooted.splits_fPolynomial"],"certificate_hash":"c79cfddcefad3bcb4e72d2040e86ea00509994c87d3d92a908c2633395b37d5d","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"lower":{"closed":true,"value":"-1"},"upper":{"closed":true,"value":"0"}}}],"premises":[{"position":0,"node_id":"n-8409b69bc5d8591b","role":"sequence","name":"basis_map_A013610 of Exponential Riordan array (1, x(1+x/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]"}]}],"used_by":[],"used_by_total":0,"links":[],"oeis":[],"bfiles":[],"oeis_texts":[{"oeis_id":"","target":"node","first_row":0,"oeis_offset":0,"reversed":false,"trim_zeros":"none","regular_triangle":false,"rows_shown":10,"polytool_commit":"c48629374597092cc41ef4d6273f37991516f984","triangle_example":"Triangle begins:\n  0:    1;\n  1:    1,     4;\n  2:    2,    13,     20;\n  3:    4,    39,    120,     112;\n  4:   10,   124,    555,    1048,      688;\n  5:   26,   400,   2375,    6740,     9040,     4544;\n  6:   76,  1374,  10050,   37835,    76740,    78864,    31936;\n  7:  232,  4858,  42420,  199325,   541520,   846048,   700672,    236800;\n  8:  764, 18064, 182420, 1024072,  3481625,  7309456,  9217376,   6365440,  1841408;\n  9: 2620, 69264, 795780, 5200608, 21240513, 56043540, 95231136, 100229760, 59196672, 14943232;\n","recurrence_sentence":"The row polynomials satisfy (3+3*x)*P(n,x) = -(5*n-8+(18*n-33)*x+(21*n-33)*x^2+(8*n-8)*x^3)*P(n-1,x) + (2+14*x+30*x^2+26*x^3+8*x^4)*d/dx P(n-1,x) for n >= 1, with P(0,x) = 1.","mathematica":"P[0, x_] := 1;\nP[n_, x_] := P[n, x] = Expand[Together[(-(5*n - 8 + (18*n - 33)*x + (21*n - 33)*x^2 + (8*n - 8)*x^3)*P[n - 1, x] + (2 + 14*x + 30*x^2 + 26*x^3 + 8*x^4)*D[P[n - 1, x], x])/(3 + 3*x)]];\nTable[CoefficientList[P[n, x], x], {n, 0, 9}] // Flatten","pari":"P(N) = {my(v = vector(N + 1)); v[1] = 1; for(n = 1, N, my(i = n + 1); v[i] = (-(5*n - 8 + (18*n - 33)*x + (21*n - 33)*x^2 + (8*n - 8)*x^3)*v[i - 1] + (2 + 14*x + 30*x^2 + 26*x^3 + 8*x^4)*deriv(v[i - 1], x))/(3 + 3*x)); v};\nrow(n, p) = {my(c = Vecrev(p)); c};\nT(N) = {my(v = P(N)); concat(vector(#v, i, row(i - 1, v[i])))};\nT(9)","reading":{"first_row":0,"offset":0,"reversed":false,"trim_zeros":"none","regular_triangle":false}}],"derivation":{"root":"n-f6268da8d9636534","steps":["basis A013610","x \u21a6 x/(x+1)"],"edges":["e-a15a4571c9a83032","e-b59dfb75c0172ee2"],"text":"A122848 \u2192 basis A013610 \u2192 x \u21a6 x/(x+1)"},"headline":"A122848 \u2192 basis A013610 \u2192 x \u21a6 x/(x+1)","chain":null}