Zulip Chat Archive
Stream: maths
Topic: Kneser's addition theorem
Yaël Dillies (Dec 31 2022 at 23:00):
Just in time for the New Year, @Mantas Baksys and I unsorried our proof of Kneser's addition theorem. This is an additive combinatorics generalisation of the classical Cauchy-Davenport theorem.
Junyan Xu (Jan 01 2023 at 01:39):
branch#kneser, I suppose
Junyan Xu (Jan 01 2023 at 01:40):
Still seeing some sorries
Yaël Dillies (Jan 01 2023 at 10:15):
Oh yeah but those sorries are in the Cauchy-Davenport file (which is not imported by Kneser) because I'm trying to derive it from a proof of a generalisation of Karolyi's theorem.
Yaël Dillies (Jan 01 2023 at 10:15):
Kneser itself really is sorry-free.
Yaël Dillies (Jan 01 2023 at 10:24):
The way to trust me is by seeing that https://github.com/leanprover-community/mathlib/commit/60428e1cf74b2ad1fcbbce7479a0054185d212c5 builds (but doesn't lint)
Angeliki Koutsoukou Argyraki (Jan 01 2023 at 13:46):
are you going to derive the so-called "strict" version of Kneser too? @Mantas Baksys and I got the strict one too in Isabelle here https://www.isa-afp.org/entries/Kneser_Cauchy_Davenport.html
Mantas Baksys (Jan 01 2023 at 13:57):
Yes, absolutely! The strict version shouldn't take too much work from here
Yaël Dillies (Jan 09 2023 at 13:09):
Mantas Baksys said:
The strict version shouldn't take too much work from here
This was an understatement. It took me 10 minutes. And now Cauchy-Davenport too is sorry-free!
Last updated: Dec 20 2023 at 11:08 UTC