Formalization of various notions of convergence

Hello,

I wrote a note on notions of convergence of sequences of functions in mathematics.

My goal was to see by myself if many definitions were possible.

I did found quite a few definitions at the end.

Maybe the approximate notions of convergence would be more interesting to computer scientists than mathematicians.

I was expecting to write 3 pages or so, and my note is 9 pages long now.

I thought this note would be better completed as a package of definitions and proofs in Rocq or LEAN. And that it could maybe be a good exercise for students to code it in LEAN.

Here are the links if you want to check if it can be interesting.

French version:
https://lyaudet.eu/laurent/Publi/Journaux/LL2026Convergence/LL2026Convergence_fr_v1.pdf

English version:
https://lyaudet.eu/laurent/Publi/Journaux/LL2026Convergence/LL2026Convergence_en_v1.pdf

Best regards,

Laurent Lyaudet

Start by reading the linked English and French notes on convergence of sequences of functions. Determine which definitions and proofs should be formalized in Rocq or Lean, then establish a scoped package and student-friendly exercise; done means the selected notions are formalized with their proofs.