claimroutineinferred_dep
Fiber polynomial retains derivative vanishing
Restricts to the fiber : gives with high order and vanishing derivatives
fiber polynomial for isolating a single center
Statement (paper)
In the affine fiber , with degree weights , order weights and , for all sufficiently large there is a nonzero polynomial of weighted degree at most and order at least at every center, and it satisfies for all multi-indices with .
In plain English
On the fiber , for all large there is a nonzero polynomial of weighted degree at most with order at least at every center, such that vanishes on for all with .
Why it's here
Since on (previous claim), the auxiliary polynomial can be restricted to the fiber, giving a polynomial in alone. The restriction keeps the high vanishing order at the centers and the vanishing of low-cost derivatives along from the earlier claim. The next claims use to analyze the persistent component inside the fiber and isolate a single center.
Classified routine:
This is a restriction-to-a-fiber step: the earlier claims establish that Y=1 on C and that the auxiliary polynomial has the required vanishing. The nonzero restriction needs a separate justification if it is not supplied by the earlier construction.
Uses
Used by
Sources
PaperOpen
- Section
- §2.2 The curve inequality
- Page
- —
- Label
—- Line
sections/interpolation.tex:368
Leannot aligned
Phase 2 aligns this node to a Lean declaration.
Friction
- infoinferred_depoutline: "Fiber polynomial retains derivative vanishing" rests on claim-geom-curve-inequality-2
- infoinferred_depoutline: "Fiber polynomial retains derivative vanishing" rests on claim-geom-curve-inequality-4
- infoinferred_depoutline: "Fiber polynomial retains derivative vanishing" rests on claim-geom-interpolation-1