{"id":"palomar/PALOMAR-2026-08-20-000009","url":"https://github.com/sloisel/MPE-Formal/tree/149d06281b1e5f2b2af85e03f8492e1b793ab4f9","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-20-000009-v1.json","repo":"https://github.com/sloisel/MPE-Formal","tags":["math.NA","msc:65B05","msc:65F10","msc:65H10","msc:41A17","msc:60D05","numerical-analysis","extrapolation","lean-formalization","fixed-point-iteration"],"score":0,"title":"sloisel/MPE-Formal","trust":"high","domain":"math.NA","source":"palomar","authors":["Sébastien Loisel"],"reviews":0,"subject":"math.NA","summary":"Machine-checked proofs of three probabilistic convergence theorems for restarted Minimal Polynomial Extrapolation (MPE) applied to nonlinear fixed-point iterations. Dithered restarts keep the error below the doubly exponential schedule delta^(theta^m), for any theta in (1,2), from every starting point -- the breakdown set included -- with an explicit failure-probability exponent over the dither; in the root sense the convergence order is at least theta. Under simple spectrum, the error follows a quadratically shrinking dither schedule (root order at least 2) with failure probability linear…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-20","reactions":{},"formalized":true,"formalizes":[{"title":"On the local convergence of minimal polynomial and reduced rank extrapolation for nonlinear fixed-point iterations","identifier":"Submitted manuscript, July 2026; no public identifier yet","relationship":"formalizes"}]}