The Proof Mining Seminar is a joint LOS/ILDS seminar, featuring talks on recent results in proof mining.
Proof mining is a paradigm of research, concerned with the extraction of hidden finitary and combinatorial content from proofs that make use of highly infinitary principles. The new information is obtained after a logical analysis, using proof-theoretic tools, and can be both of a quantitative nature, such as algorithms and effective bounds, as well as of a qualitative nature, such as uniformities in the bounds or weakenings of the premises.
All seminars, except where otherwise indicated, will be on Wednesdays between 16:00 and 18:00, Bucharest time. The seminars are held remotely.
To receive announcements about the seminar, please send an email to proof-mining-seminar@ilds.ro.
Organizers: Ulrich Kohlenbach, Laurențiu Leuștean, Andrei Sipoș
Wednesday, July 26, 2023
Pedro Pinto (TU Darmstadt)
The strange case of Dykstra’s algorithm
Abstract:
In this talk we discuss the proof mining treatment of the strong convergence of Dykstra’s algorithm.
Halpern’s iterative method is probably the most common approach to strongly approximate fixed points of nonexpansive maps. The canonical proof (pliable to many other results) establishing strong convergence of the iteration relies on a crucial use of sequential weak compactness. It is well-understood how a proof-theoretical approach allows for the elimination of the compactness arguments via bounded collection principles, thus allowing for simple quantitative data in the analysis of such proofs.
Here, we focus on a different iterative method. Generalizing the alternating projection method, Dykstra’s algorithm strongly approximates the optimal solution of the convex feasibility problem. Similarly to Halpern, the strong convergence of Dykstra’s method makes crucial uses of compactness principles substantiated by arithmetical comprehension. Yet, as the iterative schema has no connection with Halpern’s definition and the proof follows a completely different structure, it was not known whether the removal of the compactness arguments would be possible and thus, a priori, we were only guaranteed to obtain quantitative data defined by bar-recursive functionals. Strikingly, still here, it was possible to bypass the use of arithmetical comprehension and bar-recursive functionals. We will discuss the recent quantitative analysis of Dykstra’s convergence proof and explain how it was possible to avoid the compactness principles crucial in the original proof.
References:
[1] P. Pinto, On the finitary content of Dykstra’s cyclic projections algorithm. arXiv:2306.09791 [math.OC], 2023.