Real-rooted atlas

Proof step

Gamma criterion

Gamma polynomial of a palindromic parent scale 1, shift 1

Concludes
Triangle T(n,k) (n >= 1, 0 <= k <= floor((n-1)/2)) read by rows, where T(n,k) = (k+1)T(n-1,k) + (2n-4k)T(n-1,k-1).
Premises
  • eulerian
    sequence: Every row P_n, n >= 1, is zero or real-rooted with all roots in (-inf, 0]
Theorem
RealRooted IsGammaExpansion.isRealRooted_and_hasRootsNonpos_iff ?
Checked
polytool replayed · Lean not attempted
Technical details
Step id
e-7e5061201b6d9b87 · JSON
Operation
Gamma polynomial of a palindromic parent
{
  "index_shift": 1,
  "operation": "gamma_polynomial",
  "scale": "1"
}
Claims
{
  "claim": "real_rooted",
  "from_index": 0,
  "region": {
    "upper": {
      "closed": true,
      "value": "0"
    }
  }
}
Certificate
gamma_polynomial, SHA-256 c583f478ec022f4f3602fa8dbef736d6a18f293228cce6df8f65c91292fbe402, 6,744 bytes (1,925 compressed); download
polytool replayed the certificate when the step was written.
Cited by