Stream: condensed mathematics
Topic: normed group quotient
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?
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):
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):
norm_quotient_mk, the fact that the operator norm of the projection to the quotient is
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: May 09 2021 at 23:10 UTC