Kneser's addition lemma

This file proves Kneser's lemma. This states that |s + H| + |t + H| - |H| ≤ |s + t| where s, t are finite nonempty sets in a commutative group and H is the stabilizer of s + t. Further, if the inequality is strict, then we in fact have |s + H| + |t + H| ≤ |s + t|.

Main declarations

• Finset.mul_kneser: Kneser's lemma.
• Finset.mul_strict_kneser: Strict Kneser lemma.

References

• [Imre Ruzsa, Sumsets and structure][ruzsa2009]
• Matt DeVos, A short proof of Kneser's addition lemma

Auxiliary results

theorem Finset.le_card_union_add_card_mulStab_union {α : Type u_1} [CommGroup α] [DecidableEq α] {s t : Finset α} : min (s.card + s.mulStab.card) (t.card + t.mulStab.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card

theorem Finset.le_card_union_add_card_addStab_union {α : Type u_1} [AddCommGroup α] [DecidableEq α] {s t : Finset α} : min (s.card + s.addStab.card) (t.card + t.addStab.card) ≤ (s ∪ t).card + (s ∪ t).addStab.card

theorem Finset.le_card_sup_add_card_mulStab_sup {α : Type u_1} [CommGroup α] [DecidableEq α] {ι : Type u_2} {s : Finset ι} {f : ι → Finset α} (hs : s.Nonempty) : (s.inf' hs fun (i : ι) => (f i).card + (f i).mulStab.card) ≤ (s.sup f).card + (s.sup f).mulStab.card

theorem Finset.le_card_sup_add_card_addStab_sup {α : Type u_1} [AddCommGroup α] [DecidableEq α] {ι : Type u_2} {s : Finset ι} {f : ι → Finset α} (hs : s.Nonempty) : (s.inf' hs fun (i : ι) => (f i).card + (f i).addStab.card) ≤ (s.sup f).card + (s.sup f).addStab.card

Kneser's lemma

theorem Finset.le_card_mul_add_card_mulStab_mul {α : Type u_1} [CommGroup α] [DecidableEq α] {s t : Finset α} (hs : s.Nonempty) (ht : t.Nonempty) : s.card + t.card ≤ (s * t).card + (s * t).mulStab.card

theorem Finset.le_card_add_add_card_addStab_add {α : Type u_1} [AddCommGroup α] [DecidableEq α] {s t : Finset α} (hs : s.Nonempty) (ht : t.Nonempty) : s.card + t.card ≤ (s + t).card + (s + t).addStab.card

theorem Finset.mul_kneser' {α : Type u_1} [CommGroup α] [DecidableEq α] (s t : Finset α) : (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card

Kneser's multiplication lemma: A lower bound on the size of s * t in terms of its stabilizer.

theorem Finset.add_kneser' {α : Type u_1} [AddCommGroup α] [DecidableEq α] (s t : Finset α) : (s + (s + t).addStab).card + (t + (s + t).addStab).card ≤ (s + t).card + (s + t).addStab.card

Kneser's addition lemma: A lower bound on the size of s + t in terms of its stabilizer.

theorem Finset.mul_strict_kneser' {α : Type u_1} [CommGroup α] [DecidableEq α] {s t : Finset α} (h : (s * (s * t).mulStab).card + (t * (s * t).mulStab).card < (s * t).card + (s * t).mulStab.card) : (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card

The strict version of Kneser's multiplication theorem. If the LHS of Finset.mul_kneser does not equal the RHS, then it is in fact much smaller.

theorem Finset.add_strict_kneser' {α : Type u_1} [AddCommGroup α] [DecidableEq α] {s t : Finset α} (h : (s + (s + t).addStab).card + (t + (s + t).addStab).card < (s + t).card + (s + t).addStab.card) : (s + (s + t).addStab).card + (t + (s + t).addStab).card ≤ (s + t).card

The strict version of Kneser's addition theorem. If the LHS of Finset.add_kneser does not equal the RHS, then it is in fact much smaller.