claimroutine

Tapered multiplicities permit Hermite recovery of F(0)

Claim·§D.4.4 Tapered Hermite recovery·inside lemTapered Hermite recovery of F(0)

Statement (paper)

The total multiplicity satisfies ∑t≠0qt⩾Lhu⩾3ML>M(2L−1)\sum_{t\ne0}q_t\ge Lhu\ge 3ML>M(2L-1), and qt⩽4Mq_t\le 4M for every tt. Consequently, with Et(T)=∏q∈S∖{0,t}(T−qt−q)qqE_t(T)=\prod_{q\in S\setminus\{0,t\}}\left(\frac{T-q}{t-q}\right)^{q_q}, Hermite interpolation gives F(0)=∑t:qt>0Et(0)([F(t+αz)Et(t+αz)]<qt)(−t/α)F(0)=\sum_{t:q_t>0}E_t(0)\left(\left[\frac{F(t+\alpha z)}{E_t(t+\alpha z)}\right]_{<q_t}\right)(-t/\alpha).

In plain English

The multiplicities qtq_t sum over t≠0t\ne0 to at least Lhu⩾3ML>M(2L−1)Lhu\ge 3ML>M(2L-1), each qt⩽4Mq_t\le 4M, and Hermite interpolation with these multiplicities expresses F(0)F(0) as ∑t:qt>0Et(0) ([F(t+αz)/Et(t+αz)]<qt)(−t/α)\sum_{t:q_t>0}E_t(0)\,\bigl([F(t+\alpha z)/E_t(t+\alpha z)]_{<q_t}\bigr)(-t/\alpha).

Why it's here

Since the total multiplicity exceeds the degree bound M(2L−1)M(2L-1) of FF, FF is determined by its first qtq_t Taylor coefficients at each tt, which gives the explicit Hermite formula at the origin. The bound qt⩽4Mq_t\le 4M keeps the needed coefficients few, and the formula's two ingredients, dividing by EtE_t and multiplying by Et(0)E_t(0), are what the following claims check for precision loss.
Classified routine:
This is standard Hermite interpolation: a polynomial of degree below the total multiplicity is determined by its Taylor data at the nodes. The only additions are bookkeeping of the tapered multiplicity bounds and the explicit Lagrange–Hermite formula at the origin.

Uses

Nothing else in the paper

Used by

claimDivision by E_t loses no precisionclaimTwo-adic loss of E_t(0) is at most 6Dh

Sources

PaperOpen
Section
§D.4.4 Tapered Hermite recovery
Page
—
Label
—
Line
quantitative-contraction.tex:271
Leannot aligned

Phase 2 aligns this node to a Lean declaration.