{"id":"e-34a35f2adf91411c","operation":{"operation":"theorem_check","theorem":"hypergeometric_row"},"operation_detail":"hypergeometric_row","conclusion_id":"n-f2a2a3d7ea29bcbf","premise_count":0,"theorem":"Row-hypergeometric rows: an exact row relation p(n, k) [x^k] P_n + q(n, k) [x^(k-1)] P_n = 0, proved for every n by an invariant row-annihilator system of the rule, writes every row as U_0(n) x^v (or its reversal) times the image of (1 + x)^M(n) under a product of nonnegative multiplier sequences: C^k (C > 0); k -> M'!/(M' - k)!, whose exponential generating function is (1 + x)^M' (Polya--Schur, Theorem 7.1 (3) => (1) of P. Branden, Unimodality, log-concavity, real-rootedness and beyond, arXiv:1410.6601: a sequence is a multiplier sequence when G(x) = sum_k lambda_k x^k / k! or G(-x) can be written C x^m e^(a x) prod_k (1 + alpha_k x) with a >= 0, alpha_k >= 0); k -> phi(k) for a polynomial phi with only real roots, all <= 0 (Laguerre's theorem, RealRooted isPFMultiplierSequence_eval_of_roots_nonpos); k -> 1/(alpha)_k for alpha > 0 (RealRooted isPFMultiplierSequence_inv_ascPochhammer, via the generalized Laguerre polynomials); products of PF multiplier sequences are PF multiplier sequences (RealRooted IsPFMultiplierSequence.mul) and map real-rooted polynomials with nonnegative coefficients to such polynomials (IsPFMultiplierSequence.diagonalOperator_isPF)","lean_route":null,"lean_declarations":["RealRooted.isPFMultiplierSequence_eval_of_roots_nonpos","RealRooted.isPFMultiplierSequence_inv_ascPochhammer","RealRooted.IsPFMultiplierSequence.mul","RealRooted.IsPFMultiplierSequence.diagonalOperator_isPF"],"certificate_hash":"fcfc46e062da622ade39f0e1594717adae393b916bb725171f91e0c142dac334","verification_polytool":"replayed","verification_lean":"not_attempted","certificate_kind":"theorem_check","certificate_raw_size":6047,"certificate_compressed_size":1934,"conclusion_name":"Triangle T(n,k), read by rows, given by (1,1,0,0,0,0,0,0,0,...) DELTA (1,0,0,0,0,0,0,0,0,...) where DELTA is the operator defined in A084938.","claims":[{"claim":"real_rooted","from_index":1,"region":{"upper":{"closed":false,"value":"0"}}}],"premises":[],"cited_by":[{"node_id":"n-f2a2a3d7ea29bcbf","claim":"real_rooted"},{"node_id":"n-f2a2a3d7ea29bcbf","claim":"one_signed_coefficients"},{"node_id":"n-f2a2a3d7ea29bcbf","claim":"hadamard_kernel"}]}