Structured Preparation
Exercise SP-103
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
Question
Consider the generating power series obtained as the product of the exponential series exp(X) and the series 1/(1-X)^{k+1}. Let its degree-r coefficient be a_{k,r}. In the coordinate t, define A_k(t) as the truncation of this series to degrees 0..k, i.e. A_k(t) = sum_{r=0}^{k} a_{k,r} t^r. The source polynomial, in the shifted coordinate t = p+1, is a positive combination S(p) = exp(-1) * (1-t)^{k+1} * A_k(t) + t^{k+1} * A_k(1-t). Prove that A_k(t) > 0 for every t >= 0, and deduce that S(p) > 0 for every p in the closed interval [-1, 0].
Hint: mathematical route
The source Hermite bridge polynomial is strictly positive on [-1,0] because its generating-series coefficients are nonnegative with constant term one.
- The series coefficient a_{k,r} is a Cauchy product of 1/m! and binomials, hence nonnegative with a_{k,0}=1.
- A finite nonnegative sum whose constant term is 1 is at least 1, so A_k(t)>0 for t>=0.
- With t=p+1 in [0,1], both A_k(t) and A_k(1-t) are positive and the prefactors nonnegative.
- A case split on t=0 vs t>0 keeps one strictly positive term, giving S(p)>0 on [-1,0].
Reference solution
Step 1 (coefficients are nonnegative): the coefficient a_{k,r} equals the Cauchy product sum_{m=0}^{r} (1/m!) * C(k+r-m, k), where C denotes a binomial coefficient coming from 1/(1-X)^{k+1} = sum C(k+i, k) X^i and 1/m! from exp. Each summand is a quotient of nonnegative reals, so a_{k,r} >= 0, and a_{k,0} = C(k,k)/0! = 1 > 0. Step 2 (positivity of A_k on t >= 0): A_k(t) = sum_{r=0}^{k} a_{k,r} t^r is a finite sum of nonnegative terms a_{k,r} t^r (products of nonnegative a_{k,r} and nonnegative t^r). The r=0 term is a_{k,0} = 1, which is strictly positive, so the whole sum is at least 1 > 0. Step 3 (positivity of S on [-1,0]): put t = p+1. For p in [-1,0] we have t in [0,1], so both t >= 0 and 1-t >= 0. Then A_k(t) > 0 and A_k(1-t) > 0 by Step 2. The prefactors exp(-1) > 0, (1-t)^{k+1} >= 0, t^{k+1} >= 0 are nonnegative. Step 4 (strictness): if t = 0 the second term vanishes but the first is exp(-1) * 1 * A_k(0) > 0; otherwise t > 0 makes t^{k+1} * A_k(1-t) > 0, so one term is always strictly positive while the other is nonnegative. Hence S(p) > 0 throughout [-1,0].
Assessment rubric
- Computes a_{k,r} as the Cauchy product sum of 1/m! and binomial C(k+r-m,k), establishing nonnegativity and a_{k,0}=1. (1 weight)
- Concludes A_k(t) >= 1 > 0 for all t >= 0 because the degree-0 term is 1 and all other terms are nonnegative. (1 weight)
- Substitutes t=p+1, noting p in [-1,0] gives t and 1-t both in [0,1] so both A_k factors are positive. (1 weight)
- Handles strictness by a case split on t=0 vs t>0 so that at least one of the two nonnegative terms is strictly positive. (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 168-205: def coefficientSeries (k) := PowerSeries.exp R * (invOneSubPow R (k+1)).val; theorem coefficientSeries_coeff : coeff r = sum_{m in range (r+1)} C(k+r-m,k)/m!; coefficientSeries_coeff_nonneg; coefficientSeries_coeff_zero = 1. lines 254-286: coefficientPolynomial_pos (k) (t) (ht: 0<=t) : 0 < eval t; sourceInterpolant_pos (k) (p) (hp : p in Icc (-1) 0) : 0 < (sourceInterpolant k).eval p
Source SHA-256:f8a3e1d5f29aed1228b6ede3577a9af1e76301559172ee67a266fcb0d56fee1e· MIT (repository LICENSE)
Contract: 599f570daff77e40df5ac08bb19712779dee7b377fed63f7caaa3adaa2edb28b
Item digest: cf9f012b3ae8f37e5d04817754ee8ca5785470f5f4faef3d82c859613ef20f54
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.