Real-rooted atlas

Proof step

Gamma criterion

Gamma polynomial of a palindromic parent scale 1/2, shift 1

Concludes
Triangle read by rows: coefficients d(n,k) of André polynomials D(x,n) = Sum_{k>0} d(n,k)*x^k.
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-977fc5754e9861fd · JSON
Operation
Gamma polynomial of a palindromic parent
{
  "index_shift": 1,
  "operation": "gamma_polynomial",
  "scale": "1/2"
}
Claims
{
  "claim": "real_rooted",
  "from_index": 0,
  "region": {
    "upper": {
      "closed": true,
      "value": "0"
    }
  }
}
Certificate
gamma_polynomial, SHA-256 e095ded7efbc6f478bd3e896f287638c5525a38dcdf3abf63b33fd1a4b98f70d, 6,756 bytes (1,931 compressed); download
polytool replayed the certificate when the step was written.
Cited by