Structured Preparation
Exercise SP-101
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- v is an arbitrary real sequence; only its first k+1 entries are constrained
- derivatives are ordinary real polynomial derivatives
- the center a is fixed and the polynomial is expressed in the shifted basis (x-a)
Question
Fix a real point a and a natural number k, and prescribe target values v(0), v(1), ..., v(k). Define a degree-at-most-k real polynomial P by taking the local Taylor polynomial centred at a whose coefficient of (x-a)^j is v(j)/j!. Prove that for every j with 0 <= j <= k the ordinary j-th derivative of P evaluated at a equals exactly v(j). You may use the fact that the j-th derivative of a polynomial at a point equals j! times the degree-j Taylor coefficient of the polynomial about that point.
Hint: mathematical route
A single Taylor-truncation polynomial reproduces every prescribed derivative up to order k exactly, via the j! normalization of Taylor coefficients.
- The j-th derivative at a of any polynomial equals j! times its degree-j Taylor coefficient about a.
- The polynomial written in the (x-a) basis has degree-j coefficient v(j)/j! for j<=k.
- Multiplying the coefficient by j! cancels the normalization, giving exactly v(j).
Reference solution
Write P = sum over i in {0,...,k} of (v(i)/i!) * (x-a)^i. The key bridge is that for any polynomial Q, (d^j/dx^j Q)(a) = j! * c_j, where c_j is the coefficient of (x-a)^j in the Taylor expansion of Q about a; equivalently c_j is the degree-j coefficient of the shifted polynomial Q(x+a). Step 1: the Taylor coefficients of P about a are read off directly: the coefficient of (x-a)^j is v(j)/j! for j <= k and 0 for j > k, because P is already written in the (x-a) basis. Step 2: apply the bridge at order j <= k: (d^j P/dx^j)(a) = j! * (coefficient of (x-a)^j) = j! * (v(j)/j!). Step 3: since j! is a nonzero natural number cast into the reals, j! * (v(j)/j!) = v(j) exactly. Hence every requested jet value is reproduced exactly. Each summand has degree at most k, so the finite sum has degree at most k. This is only an upper bound on the degree of the polynomial for the prescribed data; for example all-zero data gives the zero polynomial. No minimality claim or numerical approximation is needed.
Assessment rubric
- Writes P in the (x-a) monomial basis with coefficient v(j)/j! and identifies these as the Taylor coefficients about a. (1 weight)
- Invokes the derivative/Taylor-coefficient bridge: j-th derivative at a equals j! times the degree-j Taylor coefficient. (1 weight)
- Cancels j! against the 1/j! normalization to conclude the j-th derivative at a equals v(j) for all j <= k. (1 weight)
- Notes the degree bound k and that the identities are exact (no numerical approximation). (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 27-49: def jetPolynomial (a : R) (k : N) (v : N -> R) := taylor (-a) (sum_{j in range (k+1)} monomial j (v j / j!)); theorem eval_iterate_derivative (p) (a) (j) : (derivative^[j] p).eval a = j! * (taylor a p).coeff j; theorem jetPolynomial_jet (a k j v) (hj : j <= k) : (derivative^[j] (jetPolynomial a k v)).eval a = v j
Source SHA-256:f8a3e1d5f29aed1228b6ede3577a9af1e76301559172ee67a266fcb0d56fee1e· MIT (repository LICENSE)
Contract: e889d7034e421885bad33bb7c60aac995da96953d1e137755e5846fb670f3664
Item digest: b8d06ee21a9000b00a45e7a559e8ec84e1a3821bc80cf948e134426bf5687741
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.