Structured Preparation
Exercise SP-106
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
Question
Let the generating series be C(X) = exp(X) * (1 - X)^{-(k+1)} as formal power series over the reals. Prove that its coefficient of X^r is exactly sum_{m=0}^{r} C(k + r - m, k) / m!, where C(.,.) is the binomial coefficient, and prove that this coefficient is nonnegative for every r, with the r=0 coefficient equal to 1. You may use that exp(X) has coefficient 1/m! in degree m and that (1-X)^{-(k+1)} has coefficient C(k+i, k) in degree i.
Hint: mathematical route
The exp times negative-binomial generating series has coefficient sum_m C(k+r-m,k)/m!, which is nonnegative and equals 1 at degree 0.
- The coefficient of X^r in exp(X)*(1-X)^{-(k+1)} is the convolution of 1/m! and C(k+i,k).
- Reindexing i=r-m yields the closed form sum_{m=0}^{r} C(k+r-m,k)/m!.
- Each summand is nonnegative, so the coefficient is nonnegative; at r=0 it equals 1.
Reference solution
Step 1 (Cauchy product): the coefficient of X^r in a product of two power series F*G is the convolution sum_{m=0}^{r} [X^m]F * [X^{r-m}]G. Here [X^m] exp = 1/m! and [X^{i}] (1-X)^{-(k+1)} = C(k+i, k). Step 2 (substitute i = r-m): the convolution becomes sum_{m=0}^{r} (1/m!) * C(k + (r-m), k) = sum_{m=0}^{r} C(k+r-m, k)/m!, which is the asserted closed form. The index substitution is valid because as m ranges over 0..r the complementary index r-m ranges over r..0, covering the same antidiagonal. Step 3 (nonnegativity): every summand is a ratio of a nonnegative binomial coefficient and a positive factorial, hence nonnegative; a finite sum of nonnegative reals is nonnegative. Step 4 (value at r=0): the sum collapses to the single term m=0, giving C(k, k)/0! = 1/1 = 1. This closed form is what makes the truncation A_k the exact finite object underlying the positive source polynomial, and its nonnegativity is exactly the ingredient needed downstream for positivity.
Assessment rubric
- Applies the Cauchy-product (convolution) formula for the coefficient of X^r in a product of two power series. (1 weight)
- Substitutes the known coefficients 1/m! (exponential) and C(k+i,k) (negative binomial) and reindexes to the closed form sum_{m} C(k+r-m,k)/m!. (1 weight)
- Shows each term is a nonnegative-binomial-over-positive-factorial ratio, so the coefficient is nonnegative. (1 weight)
- Evaluates the r=0 case as the single term C(k,k)/0!=1. (1 weight)
Graph-grounded prerequisites
These are support/source anchors, not an automatically extracted theorem-dependency proof.
Lean view and evidence boundary
No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.
Sources and provenance
- QuantumBlockEncoding/HermitePolynomial.lean
lines 184-204: theorem coefficientSeries_coeff (k r) : coeff r (coefficientSeries k) = sum_{m in range (r+1)} C(k+r-m,k)/m!; uses invOneSubPow_val_succ_eq_mk_add_choose and coeff_exp; coefficientSeries_coeff_nonneg; coefficientSeries_coeff_zero : coeff 0 = 1
Source SHA-256:f8a3e1d5f29aed1228b6ede3577a9af1e76301559172ee67a266fcb0d56fee1e· MIT (repository LICENSE)
Contract: 37f1d9ea04229c3484141ceb4f0a4d391bfcf2217d4d77f9d61e9638f1a60625
Item digest: bfb8236c482b42681d8f649cd2b0f1c243cc6405d52b55cb9abb4ab337f16792
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.