{"id":"n-96f444dda9cea45a","revision":0,"first_index":0,"fingerprint":"f6-2e8e7edac39f7fae","name":"derivative of Triangle read by rows: T(n,k) = t(n-k, k), where t(n,m) = f(m)*t(n-1,m) + f(n)*t(n,m-1) and f(n) = 5*n + 3.","polytool_family":null,"interpretation":null,"rows_observed":15,"degree_pattern":"affine","degree_slope":1,"degree_intercept":-1,"palindromic":0,"gamma_positive":0,"nonnegative":1,"rr_by_factors":false,"rows":[[],["3"],["48","18"],["501","1002","81"],["4494","26052","13482","324"],["37815","500460","750690","151260","1215"],["309324","8245470","27024840","16490940","1546620","4374"],["2498649","124513254","770915835","1027887780","311283135","14991894","15309"],["20072298","1783583136","19106041698","47282837880","31843402830","5350749408","140506086","52488"],["160860507","24712075416","432196115796","1800797494632","2250996868290","864392231592","86492263956","1286884056","177147"],["1287828840","335090984010","9188118383040","60434971471560","126055824624240","90652457207340","21438942893760","1340363936040","11590459560","590490"],["10305760317","4479814360770","186999499363365","1855535675253240","6022505662680570","7227006795216684","3247187431693170","498665331635640","20159164623465","103057603170","1948617"],["82456357062","59329997283612","3688537622516010","53398625160990780","256768103129584860","476982448484301144","359475344381418804","106797250321981560","11065612867548030","296649986418060","907019927682","6377292"],["659684337279","780854902106148","71110411989335334","1464234786543812580","10059682990031630505","27449046302691007368","32023887353139508596","16095492784050608808","3294528269723578305","237034706631117780","4294701961583814","7916212047348","20726199"],["5277583112196","10234233953877078","1347921792291270888","38702535871087386276","369525210913514408940","1424898170274435377202","2433815438838602653296","1899864227032580502936","665145379644325936092","96756339677718465690","4942379905067993256","61405403723262468","68608580458548","66961566"]],"degrees":[-1,0,1,2,3,4,5,6,7,8,9,10,11,12,13],"row_sums":["0","3","66","1584","44352","1441440","53621568","2252105856","105527245824","5461034971392","309458648378880","19062652740139008","1268532891434704896","90700101737581400064","6935069317473531666432"],"nonn":true,"definitions":[{"position":0,"source":"derived:derivative","source_kind":"derived","equality_edge_id":null,"recurrence":{"first_index":0,"initial_polynomials":[["0"],["3"]],"recurrence":{"denominator":{"coeffs":[["-7"],["5"]]},"terms":[{"coeff":{"coeffs":[["48","-144","168"],["-120","420","-610"],["0","-150","525"],["0","0","-125"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["0","30","-100","70"],["0","-75","300","-225"],["0","0","-125","125"]]},"deriv_order":1,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["-62","98"],["55","-140"],["0","50"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","-35","35"],["0","25","-25"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"}}],"properties":[{"id":191003,"position":0,"claim":"real_rooted","from_index":0,"region_key":"(-inf, 0]","provenance":"edges","claim_data":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},"label":"Real-rooted","description":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 0]","region_exact":null,"edges":["e-fcc7b73c8f9611b4"]},{"id":191004,"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-fcc7b73c8f9611b4"]},{"id":191005,"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-fcc7b73c8f9611b4"]},{"id":191006,"position":3,"claim":"interlacing","from_index":1,"region_key":null,"provenance":"edges","claim_data":{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"},"label":"Interlacing of consecutive rows","description":"Rows P_(m-1), P_m interlace (weak, unordered) for every m >= 1","region_exact":null,"edges":["e-fcc7b73c8f9611b4"]}],"region_exact":{},"incoming_edges":[{"id":"e-fcc7b73c8f9611b4","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"derivative_polynomial\",\"coefficients\":[{\"numerator\":[\"0\"],\"denominator\":[\"1\"]},{\"numerator\":[\"1\"],\"denominator\":[\"1\"]}]}"},"operation_detail":"derivative_polynomial, shift 0","conclusion_id":"n-96f444dda9cea45a","premise_count":1,"theorem":"Laguerre's theorem on differential operators: if phi is a real polynomial with only real roots, then phi(D) maps every real-rooted polynomial to a real-rooted polynomial or zero (write phi(D) = C D^j prod (1 + c_i D); D preserves real-rootedness by Rolle's theorem and p + c p' is real-rooted for every real c by Rolle's theorem applied to e^(x/c) p; Polya--Schur 1914); when the coefficients of phi have one sign, coefficients of one sign stay of one sign; applied to phi(n, .) for each n","lean_route":null,"lean_declarations":["RealRooted.splits_add_C_mul_derivative_all","RealRooted.splits_C_mul_add_derivative","Polynomial.Splits.derivative"],"certificate_hash":"004ea38704714ae12451400b2f24b9b99d7d12082f315af0739789499d80228d","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},{"claim":"interlacing","from_index":1,"kind":"weak","orientation":"unordered"}],"premises":[{"position":0,"node_id":"n-4155b181fd90d601","role":"sequence","name":"Triangle read by rows: T(n,k) = t(n-k, k), where t(n,m) = f(m)*t(n-1,m) + f(n)*t(n,m-1) and f(n) = 5*n + 3.","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:         0;\n  1:         3;\n  2:        48,          18;\n  3:       501,        1002,           81;\n  4:      4494,       26052,        13482,           324;\n  5:     37815,      500460,       750690,        151260,          1215;\n  6:    309324,     8245470,     27024840,      16490940,       1546620,         4374;\n  7:   2498649,   124513254,    770915835,    1027887780,     311283135,     14991894,       15309;\n  8:  20072298,  1783583136,  19106041698,   47282837880,   31843402830,   5350749408,   140506086,      52488;\n  9: 160860507, 24712075416, 432196115796, 1800797494632, 2250996868290, 864392231592, 86492263956, 1286884056, 177147;\n","recurrence_sentence":"The row polynomials satisfy (5*n-7)*P(n,x) = -(120*n-48+(150*n^2-420*n+144)*x+(125*n^3-525*n^2+610*n-168)*x^2)*P(n-2,x) - ((75*n-30)*x+(125*n^2-300*n+100)*x^2-(125*n^2-225*n+70)*x^3)*d/dx P(n-2,x) + (55*n-62+(50*n^2-140*n+98)*x)*P(n-1,x) + ((25*n-35)*x-(25*n-35)*x^2)*d/dx P(n-1,x) for n >= 2, with P(0,x) = 0, P(1,x) = 3.","mathematica":"P[0, x_] := 0;\nP[1, x_] := 3;\nP[n_, x_] := P[n, x] = Expand[Together[(-(120*n - 48 + (150*n^2 - 420*n + 144)*x + (125*n^3 - 525*n^2 + 610*n - 168)*x^2)*P[n - 2, x] - ((75*n - 30)*x + (125*n^2 - 300*n + 100)*x^2 - (125*n^2 - 225*n + 70)*x^3)*D[P[n - 2, x], x] + (55*n - 62 + (50*n^2 - 140*n + 98)*x)*P[n - 1, x] + ((25*n - 35)*x - (25*n - 35)*x^2)*D[P[n - 1, x], x])/(5*n - 7)]];\nTable[CoefficientList[P[n, x], x], {n, 0, 9}] // Flatten","pari":"P(N) = {my(v = vector(N + 1)); v[1] = 0; v[2] = 3; for(n = 2, N, my(i = n + 1); v[i] = (-(120*n - 48 + (150*n^2 - 420*n + 144)*x + (125*n^3 - 525*n^2 + 610*n - 168)*x^2)*v[i - 2] - ((75*n - 30)*x + (125*n^2 - 300*n + 100)*x^2 - (125*n^2 - 225*n + 70)*x^3)*deriv(v[i - 2], x) + (55*n - 62 + (50*n^2 - 140*n + 98)*x)*v[i - 1] + ((25*n - 35)*x - (25*n - 35)*x^2)*deriv(v[i - 1], x))/(5*n - 7)); 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-4155b181fd90d601","steps":["D"],"edges":["e-fcc7b73c8f9611b4"],"text":"A257623 \u2192 D"},"headline":"A257623 \u2192 D","chain":null}