Structured Preparation
Exercise SP-110
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 a degree-d polynomial be given by Bernstein coefficients c(0),...,c(d), all lying in a common interval [lo, hi]. Suppose we restrict the polynomial to a subinterval [u, v] with 0 <= u < v <= 1 by two successive de Casteljau subdivisions, producing new Bernstein coefficients c'(0),...,c'(d) for the restricted piece. Prove that every restricted coefficient c'(i) still lies in [lo, hi]. Identify the two structural facts about the Bernstein basis that make this true.
Hint: mathematical route
De Casteljau subinterval restriction keeps every Bernstein coefficient inside the original range, because each new coefficient is a convex combination (partition of unity plus nonnegativity).
- Partition of unity plus basis nonnegativity make every Bernstein sum on [0,1] a convex combination of its coefficients.
- Each de Casteljau output is such a convex combination, so a subdivision at a parameter in [0,1] preserves the bounds.
- The second subdivision parameter (v-u)/(1-u) lies in [0,1], so composing both keeps all restricted coefficients in [lo,hi].
Reference solution
Two facts drive the proof. Fact A (partition of unity): the Bernstein basis functions of a fixed degree sum to 1 at every t, i.e. sum_{r=0}^{d} B_{d,r}(t) = 1. Fact B (nonnegativity on [0,1]): each B_{d,r}(t) >= 0 for t in [0,1]. Together they say that any Bernstein sum sum_r c(r) B_{d,r}(t) with t in [0,1] is a convex combination of the c(r), hence lies between min and max of the coefficients; in particular if all c(r) in [lo,hi] the value lies in [lo,hi]. Step 1 (one subdivision preserves bounds): each new coefficient produced by a single de Casteljau subdivision at a parameter in [0,1] is itself a Bernstein sum of a sub-row of the original coefficients evaluated at that parameter. By Facts A and B it is a convex combination of coefficients from [lo,hi], hence in [lo,hi]. This applies to the right-edge (upper) subdivision at u in [0,1]: all its outputs stay in [lo,hi]. Step 2 (second subdivision): the left-edge (lower) subdivision is applied at the parameter (v-u)/(1-u). Because 0 <= u < v <= 1 we have 0 <= (v-u)/(1-u) <= 1 (the numerator is nonnegative and at most the positive denominator 1-u). So the second subdivision is again evaluated at a parameter in [0,1], and by the same convex-combination argument its outputs — the restricted coefficients c'(i) — remain in [lo,hi]. Step 3 (conclusion): composing the two bound-preserving subdivisions keeps every c'(i) in [lo,hi]. This is the exact numerical-stability property of de Casteljau subdivision: restricting to a subinterval never amplifies coefficients beyond the original range, in contrast to monomial-basis restriction which can.
Assessment rubric
- States the partition-of-unity and nonnegativity facts and concludes any Bernstein sum on [0,1] is a convex combination of its coefficients. (1 weight)
- Shows one de Casteljau subdivision at a parameter in [0,1] outputs convex combinations, hence stays in [lo,hi] (applied to the u subdivision). (1 weight)
- Verifies the second subdivision parameter (v-u)/(1-u) lies in [0,1] using 0<=u<v<=1. (1 weight)
- Composes the two bound-preserving steps to conclude all restricted coefficients remain in [lo,hi], noting this is the stability advantage of the Bernstein basis. (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/HermiteBernstein.lean
lines 313-374: restrictCoefficients d u v c = leftRestriction ((v-u)/(1-u)) (rightRestriction d u c); basis_sum : sum_r basis d r t = 1; bernstein_sum_bounds (ht: t in Icc 0 1) (hc: c r in Icc lo hi) : sum in Icc lo hi; restrictCoefficients_bounds (hu:0<=u)(huv:u<v)(hv:v<=1) : restricted coeff in Icc lo hi
Source SHA-256:661618d9c10826491ee293c7c411ac2d55056426739f4bbfd3e7c410c05e4bff· MIT (repository LICENSE)
Contract: c5283bcf00ecd69dfd00de82a822875dc87c7da90c35b71678fe5dc8f992259a
Item digest: 19291aabce76c1930159c1330905a8a44784b80535f3d33e1810e220eb3aa5ec
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.