This document is a blueprint for the formalization in Lean 4 of the paper Catching-Up Algorithm with Approximate Projections for Moreau’s Sweeping Processes by Juan Guillermo Garrido and Emilio Vilches (2024).

The paper develops an enhanced version of the catching-up algorithm for sweeping processes through an appropriate concept of approximate projection. Under suitable assumptions, convergence is shown for three main cases: uniformly prox-regular moving sets (without compactness assumptions), boundedly compact subsmooth moving sets, and general boundedly compact fixed closed sets.

The main reference is:

• Garrido, J.G., Vilches, E. Catching-Up Algorithm with Approximate Projections for Moreau’s Sweeping Processes. J Optim Theory Appl (2024). https://doi.org/10.1007/s10957-024-02398-1

This blueprint is maintained by Gabriel Ortega.