{"id":"n-788e4697181967e9","revision":0,"first_index":0,"fingerprint":"f6-9adf2978aaed3e00","name":"derivative of Stirling2 triangle with scaled diagonals (powers of 10).","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":[["30","2"],["700","120","3"],["15000","5000","300","4"],["310000","180000","19500","600","5"],["6300000","6020000","1050000","56000","1050","6"],["127000000","193200000","51030000","4200000","133000","1680","7"],["2550000000","6050000000","2331000000","278040000","13230000","277200","2520","8"],["51100000000","186600000000","102315000000","17010000000","1141350000","35280000","525000","3600","9"],["1023000000000","5700200000000","4372500000000","986920000000","89743500000","3839220000","83160000","924000","4950","10"],["20470000000000","173052000000000","183450300000000","55176000000000","6618260000000","376437600000","11131890000","178200000","1534500","6600","11"],["409500000000000","5232500000000000","7597590000000000","3003400400000000","466065600000000","34292544000000","1329728400000","28760160000","353925000","2431000","8580","12"],["8191000000000000","157794000000000000","311752350000000000","160300140000000000","31718186500000000","2959756800000000","146386240000000","4108104000000","67747680000","660660000","3703700","10920","13"],["163830000000000000","4750202000000000000","12706785000000000000","8430676800000000000","2103466365000000000","245244799800000000","15163948800000000","537027920000000","11396385000000","147947800000","1171170000","5460000","13650","14"],["3276700000000000000","142833720000000000000","515396703000000000000","438476220000000000000","136746327900000000000","19691295624000000000","1499234837100000000","65662740000000000","1743794910000000","28936908000000","303282980000","1987440000","7826000","16800","15"],["65535000000000000000","4291565000000000000000","20830118700000000000000","22611006604000000000000","8752874949000000000000","1542486287160000000000","142911965196000000000","7623057842400000000","248250073500000000","5120609780000000","68224556400000","589221360000","3248700000","10948000","20400","16"]],"degrees":[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15],"row_sums":["32","823","20304","510105","13427056","375564687","11222549728","358202158609","12176286808960","439154309231111","16744707388924592","672865996056054633","28415917487029443664","1257987637138196262815","58244375002698717428416"],"nonn":true,"definitions":[{"position":0,"source":"derived:derivative","source_kind":"derived","equality_edge_id":null,"recurrence":{"first_index":0,"initial_polynomials":[["30","2"],["700","120","3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-200","-20","-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["0","-100","-10"]]},"deriv_order":1,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["30","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","10"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"}}],"properties":[{"id":193236,"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-aec3072bbd4c8889"]},{"id":193237,"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-aec3072bbd4c8889"]},{"id":193238,"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-aec3072bbd4c8889"]},{"id":193239,"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-aec3072bbd4c8889"]}],"region_exact":{},"incoming_edges":[{"id":"e-aec3072bbd4c8889","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-788e4697181967e9","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":"708884a1bbdf120f7fbc384b27eae7b4f5af026af6b2c9ffc2d6b2804453b66e","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-65034f179833a7f6","role":"sequence","name":"Stirling2 triangle with scaled diagonals (powers of 10).","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:             30,               2;\n  1:            700,             120,               3;\n  2:          15000,            5000,             300,              4;\n  3:         310000,          180000,           19500,            600,             5;\n  4:        6300000,         6020000,         1050000,          56000,          1050,            6;\n  5:      127000000,       193200000,        51030000,        4200000,        133000,         1680,           7;\n  6:     2550000000,      6050000000,      2331000000,      278040000,      13230000,       277200,        2520,         8;\n  7:    51100000000,    186600000000,    102315000000,    17010000000,    1141350000,     35280000,      525000,      3600,       9;\n  8:  1023000000000,   5700200000000,   4372500000000,   986920000000,   89743500000,   3839220000,    83160000,    924000,    4950,   10;\n  9: 20470000000000, 173052000000000, 183450300000000, 55176000000000, 6618260000000, 376437600000, 11131890000, 178200000, 1534500, 6600, 11;\n","recurrence_sentence":"The row polynomials satisfy P(n,x) = -(200+20*x+x^2)*P(n-2,x) - (100*x+10*x^2)*d/dx P(n-2,x) + (30+2*x)*P(n-1,x) + 10*x*d/dx P(n-1,x) for n >= 2, with P(0,x) = 30 + 2*x, P(1,x) = 700 + 120*x + 3*x^2.","mathematica":"P[0, x_] := 30 + 2*x;\nP[1, x_] := 700 + 120*x + 3*x^2;\nP[n_, x_] := P[n, x] = Expand[-(200 + 20*x + x^2)*P[n - 2, x] - (100*x + 10*x^2)*D[P[n - 2, x], x] + (30 + 2*x)*P[n - 1, x] + 10*x*D[P[n - 1, x], x]];\nTable[CoefficientList[P[n, x], x], {n, 0, 9}] // Flatten","pari":"P(N) = {my(v = vector(N + 1)); v[1] = 30 + 2*x; v[2] = 700 + 120*x + 3*x^2; for(n = 2, N, my(i = n + 1); v[i] = -(200 + 20*x + x^2)*v[i - 2] - (100*x + 10*x^2)*deriv(v[i - 2], x) + (30 + 2*x)*v[i - 1] + 10*x*deriv(v[i - 1], 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-65034f179833a7f6","steps":["D"],"edges":["e-aec3072bbd4c8889"],"text":"A075505 \u2192 D"},"headline":"A075505 \u2192 D","chain":null}
