Zulip Chat Archive

Stream: condensed mathematics

Topic: normed group quotient


view this post on Zulip Patrick Massot (Mar 12 2021 at 23:43):

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?

view this post on Zulip Patrick Massot (Mar 12 2021 at 23:45):

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

view this post on Zulip Riccardo Brasca (Mar 13 2021 at 00:20):

Definitely cleaner than the previous version!

view this post on Zulip 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.)

view this post on Zulip 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)].

view this post on Zulip Johan Commelin (Mar 13 2021 at 08:32):

good point, thanks!

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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: May 09 2021 at 23:10 UTC