[Merged by Bors] - feat: Add ConditionallyCompleteLinearOrder versions of Monotone.map_limsSup_of_continuousAt etc. #6107

kkytola · 2023-07-24T15:14:40Z

Generalize some existing lemmas from CompleteLinearOrders to ConditionallyCompleteLinearOrders, adding the appropriate boundedness assumptions:

Monotone.map_limsSup_of_continuousAt + its 3 order-dual variants
Monotone.map_limsup_of_continuousAt + its 3 order-dual variants
Monotone.map_sSup_of_continuousAt' + its 3 order-dual variants
Monotone.map_iSup_of_continuousAt' + its 3 order-dual variants

For the first two to work automatically still on CompleteLinearOrders, the existing macro tactic isBoundedDefault about boundedness of filters is used. For the last two to work automatically still on CompleteLinearOrders, a similar new macro tactic bddDefault about boundedness of sets is included in the PR.

…msSup_of_continuousAt etc.

ADedecker · 2023-07-24T15:21:23Z

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

+-- Q: Was there a way to "automatically specialize" these kinds of lemmas from
+-- conditionally complete linear orders to complete linear orders so that the then
+-- trivial boundedness assumptions (such as `F.IsBounded (· ≤ ·)`, `F.IsBounded (· ≥ ·)`)
+-- don't need to be provided by the user?
+--
+-- That would allow to use the new `Antitone.map_limsSup_of_continuousAt'` (with prime) and friends
+-- as strictly more general direct replacements of `Antitone.map_limsSup_of_continuousAt` (no
+-- prime) and friends.


I think you can use something like (h : f.IsBoundedUnder (· ≤ ·) u := by isBoundedDefault). See tendsto_of_liminf_eq_limsup for example.

If it works indeed you should replace the existing versions.

Thank you! This seems to work. I'm renaming the new ones to see if they now work throughout Mathlib as direct replacements of the old ones. (I currently only did this for 4 lemmas, but I will do the same for the other 4 if Mathlib compiles, and in fact also for yet another 4 which were just alternative phrasings.)

If I get to removing the old ones altogether, is it ok to keep the #aligns although the type signature will have changed? Since the results would presumably still work with the same explicit arguments, my naive opinion is that aligning would still be ok.

Yes that's fine, because 1) indeed this is close enough in practice and 2) we got past port-complete so we don't need to be as careful as before IIUC.

The tactic isBoundedDefault was for filters only (as far as I understood). I wrote a similar 2-line macro setIsBddDefault to be used with default boundedness of sets.

Oh, or would it be desirable that the same tactic handles automatic boundedness of both filters and sets in complete linear orders? The tactic isBoundedDefault seemed to be in Filter namespace, so I thought boundedness of sets would not be in scope, but now I'm not so sure anymore...

Yes I think the best solution is to have the same tactic taking care of both. That said, I've thought about it a few times before, and arrived to the conclusion that there is a "good" reason that we don't have the set version: even if we had, we wouldn't be able to merge the APIs of CompleteLattice and ConditionallyCompleteLattice, because we still can't get rid of the Nonempty assumptions that are required in the conditionally complete case but not in the complete case. This situation doesn't happen for (nontrivial?) filters, so here it makes more sense to have each lemma once.

That doesn't mean that we shouldn't add it, in fact it can't hurt and I have some ideas about a (gigantic) refactor that would make it useful, I just wanted to mention why it's not so strange that it is missing.

On the technical side, I'm not sure how to make it so that the same tactic work without messing up with the import tree. We could probably take inspiration about positivity that is split into small extensions, but if that gets too hard then having two tactics is not that bad (you basically never have to call these tactics explicitly anyway)

I think having two tactics is fine for now. If this kind of thing keeps coming up we can develop a uniform way to deal with it.

…iew suggestion.

…tly used instead.

…o the original Monotone section.

…s to be the Lean4 syntax for it.

…at appears to be the Lean4 syntax for it.

…rs) so that automation makes the new lemmas function as direct generalizations of the old ones.

…mpiles.

Mathlib/Order/LiminfLimsup.lean

…ete_linear_orders

Mathlib/Topology/Order/Basic.lean

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

ADedecker · 2023-08-04T12:25:13Z

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

+      by_contra con
+      simp only [not_exists, not_lt] at con
+      simpa only [lt_self_iff_false] using lt_of_le_of_lt
+        (@liminf_le_of_frequently_le R S _ F f (f (limsSup F))
+          (frequently_of_forall (fun r ↦ f_decr (con r))) (bdd_above.isBoundedUnder f_decr)) H


What do you think of keeping the structure of the existing proof treating the case where F.limsSup is a bottom element (using IsBot) separately from the beginning?

Sorry, I honestly can't form an opinion about that!

I guess I mainly opted for not talking about a bottom element, since under the conditionally complete hypotheses it is not given that a bottom element exists. But the proof ends up being a bit of a case bash anyway, and one way to handle some cases would be to consider the case that there indeed exists a bottom element and F.limsSup happens to be that.

Is it the number of (nested) reasoning steps that argue by contradiction that seems questionable style here?

I really don't know what would be elegant (or the least inelegant) here. Do you have a clear opinion?

Thinking about it again I think your structure is actually good (and there was no style issue at all with that, I was mostly nit-picking). The only thing I'd change about the structure is I think it would be clearer if you did

have : \not IsBot F.limsSup := by sorry

after by_contra' H and then use that in the obtain. Is that clear enough?

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

…der duals throughout the file (ended up being more than I expected).

…o rename it.

…-namespaced macro name.

…ent before).

ADedecker

Final nitpicks!

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

ADedecker · 2023-08-08T13:18:09Z

Thanks!

maintainer merge

github-actions · 2023-08-08T13:18:24Z

🚀 Pull request has been placed on the maintainer queue by ADedecker.

j-loreaux · 2023-08-08T13:50:07Z

This looks like some nice generalization. Thanks!

bors r+

…msSup_of_continuousAt etc. (#6107) Generalize some existing lemmas from `CompleteLinearOrder`s to `ConditionallyCompleteLinearOrder`s, adding the appropriate boundedness assumptions: - `Monotone.map_limsSup_of_continuousAt` + its 3 order-dual variants - `Monotone.map_limsup_of_continuousAt` + its 3 order-dual variants - `Monotone.map_sSup_of_continuousAt'` + its 3 order-dual variants - `Monotone.map_iSup_of_continuousAt'` + its 3 order-dual variants For the first two to work automatically still on `CompleteLinearOrder`s, the existing macro tactic `isBoundedDefault` about boundedness of filters is used. For the last two to work automatically still on `CompleteLinearOrder`s, a similar new macro tactic `bddDefault` about boundedness of sets is included in the PR. Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>

bors · 2023-08-08T15:11:31Z

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

…msSup_of_continuousAt etc. (#6107) Generalize some existing lemmas from `CompleteLinearOrder`s to `ConditionallyCompleteLinearOrder`s, adding the appropriate boundedness assumptions: - `Monotone.map_limsSup_of_continuousAt` + its 3 order-dual variants - `Monotone.map_limsup_of_continuousAt` + its 3 order-dual variants - `Monotone.map_sSup_of_continuousAt'` + its 3 order-dual variants - `Monotone.map_iSup_of_continuousAt'` + its 3 order-dual variants For the first two to work automatically still on `CompleteLinearOrder`s, the existing macro tactic `isBoundedDefault` about boundedness of filters is used. For the last two to work automatically still on `CompleteLinearOrder`s, a similar new macro tactic `bddDefault` about boundedness of sets is included in the PR. Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>

kkytola added 2 commits July 24, 2023 18:08

feat: Add ConditionallyCompleteLinearOder versions of Monotone.map_li…

d54a551

…msSup_of_continuousAt etc.

feat: Add ConditionallyCompleteLinearOder versions of Monotone.map_li…

ac30179

…msSup_of_continuousAt etc.

kkytola added WIP Work in progress t-topology Topological spaces, uniform spaces, metric spaces, filters t-order Order theory labels Jul 24, 2023

Fix a long line.

f751aa0

ADedecker reviewed Jul 24, 2023

View reviewed changes

kkytola added 12 commits July 24, 2023 18:23

Add docstrings and correct redundant phrasings.

aaebb58

Automatic inference of boundedness properties following Anatole's rev…

681b3e2

…iew suggestion.

Renaming some old results to see if the new general ones can be direc…

c659977

…tly used instead.

Generalized four alternative phrasings as well and moved everything t…

b7ea924

…o the original Monotone section.

Edited the docstring of isBoundedDefault to correspond to what appear…

95787b1

…s to be the Lean4 syntax for it.

Re-edited (fix) the docstring of isBoundedDefault to correspond to wh…

f9c8346

…at appears to be the Lean4 syntax for it.

Remove a question in the comments.

ee29f05

Added a tactic setIsBddDefault similar to isBoundedDefault (for filte…

e4b5ac5

…rs) so that automation makes the new lemmas function as direct generalizations of the old ones.

Generalize another 4 lemmas and align the generalized versions instead.

3350c80

Just remove the old less general versions --- let's see if Mathlib co…

2fccb86

…mpiles.

Remove a prime (fix).

11f2ea3

Moved some filter lemmas.

ccc01ed

ADedecker reviewed Jul 26, 2023

View reviewed changes

Mathlib/Order/LiminfLimsup.lean Outdated Show resolved Hide resolved

kkytola added 2 commits August 2, 2023 11:34

Merge branch 'master' into kkytola/map_limsup_for_conditionally_compl…

eab774b

…ete_linear_orders

Removed lemmas made obsolete by better ones in PR #6287.

9a3bb86

kkytola added awaiting-review and removed WIP Work in progress labels Aug 2, 2023

ADedecker reviewed Aug 3, 2023

View reviewed changes

Mathlib/Topology/Order/Basic.lean Outdated Show resolved Hide resolved

Mathlib/Topology/Order/Basic.lean Outdated Show resolved Hide resolved

ADedecker reviewed Aug 4, 2023

View reviewed changes

ADedecker added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Aug 4, 2023

kkytola and others added 2 commits August 5, 2023 11:43

Apply suggestions from code review

7c811bb

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

Use named arguments instead of @ _ _ _ _ for specifying the use of or…

361b55c

…der duals throughout the file (ended up being more than I expected).

ADedecker added the awaiting-author A reviewer has asked the author a question or requested changes label Aug 5, 2023

kkytola added 3 commits August 6, 2023 00:22

Move the default boundedness tactic to an appropriate place and try t…

38d7773

…o rename it.

Could not get the namespace for the macro working, used a similar non…

1ad722c

…-namespaced macro name.

Forgot to commit the renaming of the tactic where it is used.

4cd878b

kkytola added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Aug 6, 2023

ADedecker added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Aug 7, 2023

kkytola added 2 commits August 7, 2023 23:15

Clarify proof following a review comment (sorry for missing this comm…

57bcf76

…ent before).

Changed the name of the macto to bddDefault.

4ccd1a9

kkytola added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Aug 8, 2023

ADedecker reviewed Aug 8, 2023

View reviewed changes

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean Outdated Show resolved Hide resolved

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean Outdated Show resolved Hide resolved

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean Outdated Show resolved Hide resolved

ADedecker added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Aug 8, 2023

Apply suggestions from code review

58f1d4c

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

ADedecker added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Aug 8, 2023

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Aug 8, 2023

bors bot changed the title ~~feat: Add ConditionallyCompleteLinearOder versions of Monotone.map_limsSup_of_continuousAt etc.~~ [Merged by Bors] - feat: Add ConditionallyCompleteLinearOder versions of Monotone.map_limsSup_of_continuousAt etc. Aug 8, 2023

bors bot closed this Aug 8, 2023

bors bot deleted the kkytola/map_limsup_for_conditionally_complete_linear_orders branch August 8, 2023 15:11

alreadydone changed the title ~~[Merged by Bors] - feat: Add ConditionallyCompleteLinearOder versions of Monotone.map_limsSup_of_continuousAt etc.~~ [Merged by Bors] - feat: Add ConditionallyCompleteLinearOrder versions of Monotone.map_limsSup_of_continuousAt etc. Aug 9, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: Add ConditionallyCompleteLinearOrder versions of Monotone.map_limsSup_of_continuousAt etc. #6107

[Merged by Bors] - feat: Add ConditionallyCompleteLinearOrder versions of Monotone.map_limsSup_of_continuousAt etc. #6107

kkytola commented Jul 24, 2023 •

edited by j-loreaux

Loading

ADedecker Jul 24, 2023

ADedecker Jul 24, 2023

kkytola Jul 24, 2023 •

edited

Loading

kkytola Jul 24, 2023

ADedecker Jul 24, 2023

kkytola Jul 24, 2023

kkytola Jul 24, 2023 •

edited

Loading

ADedecker Jul 24, 2023

ADedecker Jul 24, 2023

j-loreaux Aug 8, 2023

ADedecker Aug 4, 2023

kkytola Aug 5, 2023

ADedecker Aug 5, 2023 •

edited

Loading

ADedecker left a comment

ADedecker commented Aug 8, 2023

github-actions bot commented Aug 8, 2023

j-loreaux commented Aug 8, 2023

bors bot commented Aug 8, 2023

[Merged by Bors] - feat: Add ConditionallyCompleteLinearOrder versions of Monotone.map_limsSup_of_continuousAt etc. #6107

[Merged by Bors] - feat: Add ConditionallyCompleteLinearOrder versions of Monotone.map_limsSup_of_continuousAt etc. #6107

Conversation

kkytola commented Jul 24, 2023 • edited by j-loreaux Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kkytola Jul 24, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kkytola Jul 24, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ADedecker Aug 5, 2023 • edited Loading

Choose a reason for hiding this comment

ADedecker left a comment

Choose a reason for hiding this comment

ADedecker commented Aug 8, 2023

github-actions bot commented Aug 8, 2023

j-loreaux commented Aug 8, 2023

bors bot commented Aug 8, 2023

kkytola commented Jul 24, 2023 •

edited by j-loreaux

Loading

kkytola Jul 24, 2023 •

edited

Loading

kkytola Jul 24, 2023 •

edited

Loading

ADedecker Aug 5, 2023 •

edited

Loading