Zulip Chat Archive

While trying to work on Johan's optimistic lemma this afternoon, I noticed the normed group quotient file was not super clean. I pushed a modification in this branch, especially this commit, but maybe the gain is not so clear. What do you think?

Patrick Massot (Mar 12 2021 at 23:45):

github is a bit confused by the diff, looking at the new file is probably clearer.

Riccardo Brasca (Mar 13 2021 at 00:20):

Definitely cleaner than the previous version!

Johan Commelin (Mar 13 2021 at 04:36):

@Patrick Massot LGTM! Thanks :octopus: And thanks to @Riccardo Brasca for writing the first version! Feel free to merge it into master when you think you are done.
The gain is pretty clear: we can now PR this to mathlib.
(Just one comment, I think some of the results about is_quotient should be in the is_quotient namespace, but were not.)

Sebastien Gouezel (Mar 13 2021 at 08:05):

Note that is_closed is now a class, so you can also remove the [fact (is_closed S)].

Johan Commelin (Mar 13 2021 at 08:32):

good point, thanks!

Riccardo Brasca (Mar 13 2021 at 08:34):

Before PR we can prove that the operator norm of the projection is 1 (this is maybe false if the subspace is the whole thing). I can do it on Monday

Riccardo Brasca (Mar 24 2021 at 22:02):

I've added norm_quotient_mk, the fact that the operator norm of the projection to the quotient is 1, here
https://github.com/leanprover-community/lean-liquid/commit/6341bd538feed5bcbd85d36d53f97d6d09b91fd1

This doesn't seem to be necessary for the LTE, but it's very natural to have if we want to include normed_group_quotient in mathlib. The proof has been surprisingly annoying... if someone wants to golf it he is very welcome :grinning_face_with_smiling_eyes:

Riccardo Brasca (Apr 06 2021 at 07:45):

#6977 Is on the queue! After the next mathlib bump I can start working on semi_normed_group in the LTE.

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib