[Merged by Bors] - feat: Ordinal Approximants of the least/greatest fixed point in a complete lattice

[PhoenixIra]

Define ordinal approximants for the least/greatest fixed points of a monotone function in a complete lattice. It is sometimes also called the constructive Knaster-Tarski Theorem, first introduced by Cousot & Cousot in 1979. This implementation is however not constructive.

This has a variety of applications in non standard logics and proofs such as quantitative logics or cyclic proofs.

---

I am a bit unsure about the placement of certain theorems, namely:

• The placement of the limitation definition and its theorems. This feels very special to this theorem. Thus I left it in this file. It could however also live somewhere in Ordinals/Cardinals
• The theorems monotone_stabilizing and antitone_stabilizing. I first thought about placing them in Mathlib.Order.Monotone.Basic. However, Monotone is using preorders and not partialorders, where this theorem does not hold. Maybe this theorem is also already proven somewhere else and I missed it?
• The OrdinalApprox namespace could also live in Mathlib.Order.FixedPoints. However, I decided aginst it as this would mean that importing Mathlib.Order.FixedPoints would also import a lot of (likely unecessary) files from Mathlib.SetTheory.Ordinal and Mathlib.SetTheory.Cardinal when not using ordinal approximants.

I appreciate comments regarding these questions and reviews in general. I also appreciate a comment if this has already been done and I just totally missed it.

[Ruben-VandeVelde]

Sorry for the delayed response here, @PhoenixIra. I don't know enough about the mathematics to judge whether this is the right thing to prove, but I can make suggestions about mathlib style, which you'll find below. Could you let us know whether you're still up for finishing this PR?

[PhoenixIra]

Thank you for the detailed comments! I am rather busy the next two weeks. But as soon as I get to it, I will incorporate or react to all comments. I am also still very motivated to finish up the PR.

[PhoenixIra]

I believe, I have addressed all issues. Please let me know if I missed anything.

[PhoenixIra]

Thank you for the review and don't worry about the delay.

I have changed the documentation to only communicate the approximation scheme and explain why it's not constructive (despite the name of the papers). If I missed anything, please let me know.

I also decided to remove Ordinal from the filename, as the filename was already very long. Please also let me know if you think this is confusing now (as e.g. the Kleene fixed-point theorem is not located there)

I will also resolve / comment on your detailed comments.

[fpvandoorn]

Thanks for the changes.

I have a few more suggestions. If you incorporate those (and the same for gfp, then I'm happy to merge this.

[fpvandoorn]

Can you move/rename the file to Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean? I think Ordinal is a better folder for this file (though I do not feel strongly about this), but the name FixedPointApproximants is a bit better than the current name.

[PhoenixIra]

Every suggestion should be incorporated.

[fpvandoorn]

Thank you for incorporating all review suggestions!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style