Kneser's addition theorem

This file proves Kneser's theorem. 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 theorem.
• Finset.mul_strict_kneser: Strict Kneser theorem.

References

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

Auxiliary results

theorem Finset.mulStab_mul_ssubset_mulStab {α : Type u_1} [CommGroup α] [DecidableEq α] {s t C : Finset α} {a b : α} (hs₁ : (s ∩ a • C.mulStab).Nonempty) (ht₁ : (t ∩ b • C.mulStab).Nonempty) (hab : ¬(a * b) • C.mulStab ⊆ s * t) : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊂ C.mulStab

theorem Finset.addStab_add_ssubset_addStab {α : Type u_1} [AddCommGroup α] [DecidableEq α] {s t C : Finset α} {a b : α} (hs₁ : (s ∩ (a +ᵥ C.addStab)).Nonempty) (ht₁ : (t ∩ (b +ᵥ C.addStab)).Nonempty) (hab : ¬(a + b) +ᵥ C.addStab ⊆ s + t) : (s ∩ (a +ᵥ C.addStab) + t ∩ (b +ᵥ C.addStab)).addStab ⊂ C.addStab

theorem Finset.mulStab_union {α : Type u_1} [CommGroup α] [DecidableEq α] {s t C : Finset α} {a b : α} (hs₁ : (s ∩ a • C.mulStab).Nonempty) (ht₁ : (t ∩ b • C.mulStab).Nonempty) (hab : ¬(a * b) • C.mulStab ⊆ s * t) (hC : Disjoint C (s ∩ a • C.mulStab * (t ∩ b • C.mulStab))) : (C ∪ s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab = (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab

theorem Finset.addStab_union {α : Type u_1} [AddCommGroup α] [DecidableEq α] {s t C : Finset α} {a b : α} (hs₁ : (s ∩ (a +ᵥ C.addStab)).Nonempty) (ht₁ : (t ∩ (b +ᵥ C.addStab)).Nonempty) (hab : ¬(a + b) +ᵥ C.addStab ⊆ s + t) (hC : Disjoint C (s ∩ (a +ᵥ C.addStab) + t ∩ (b +ᵥ C.addStab))) : (C ∪ (s ∩ (a +ᵥ C.addStab) + t ∩ (b +ᵥ C.addStab))).addStab = (s ∩ (a +ᵥ C.addStab) + t ∩ (b +ᵥ C.addStab)).addStab

theorem Finset.mul_aux1 {α : Type u_1} [CommGroup α] [DecidableEq α] {s s' t t' C : Finset α} (ih : (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card) (hconv : (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card) (hnotconv : (C ∪ s' * t').card + (C ∪ s' * t').mulStab.card < (s ∩ t).card + ((s ∪ t) * (C ∪ s' * t').mulStab).card) (hCun : (C ∪ s' * t').mulStab = (s' * t').mulStab) (hdisj : Disjoint C (s' * t')) : ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s' * t').mulStab).card < ↑C.mulStab.card - ↑(s' * (s' * t').mulStab).card - ↑(t' * (s' * t').mulStab).card

theorem Finset.add_aux1 {α : Type u_1} [AddCommGroup α] [DecidableEq α] {s s' t t' C : Finset α} (ih : (s' + (s' + t').addStab).card + (t' + (s' + t').addStab).card ≤ (s' + t').card + (s' + t').addStab.card) (hconv : (s ∩ t).card + (s ∪ t + C.addStab).card ≤ C.card + C.addStab.card) (hnotconv : (C ∪ (s' + t')).card + (C ∪ (s' + t')).addStab.card < (s ∩ t).card + (s ∪ t + (C ∪ (s' + t')).addStab).card) (hCun : (C ∪ (s' + t')).addStab = (s' + t').addStab) (hdisj : Disjoint C (s' + t')) : ↑(s ∪ t + C.addStab).card - ↑(s ∪ t + (s' + t').addStab).card < ↑C.addStab.card - ↑(s' + (s' + t').addStab).card - ↑(t' + (s' + t').addStab).card

theorem Finset.disjoint_smul_mulStab {α : Type u_1} [CommGroup α] [DecidableEq α] {s t : Finset α} {a : α} (hst : s ⊆ t) (has : ¬a • s.mulStab ⊆ t) : Disjoint s (a • s.mulStab)

theorem Finset.disjoint_vadd_addStab {α : Type u_1} [AddCommGroup α] [DecidableEq α] {s t : Finset α} {a : α} (hst : s ⊆ t) (has : ¬a +ᵥ s.addStab ⊆ t) : Disjoint s (a +ᵥ s.addStab)

theorem Finset.disjoint_mul_sub_card_le {α : Type u_1} [CommGroup α] [DecidableEq α] {a : α} (b : α) {s t C : Finset α} (has : a ∈ s) (hsC : Disjoint t (a • C.mulStab)) (hst : (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab ⊆ C.mulStab) : ↑C.mulStab.card - ↑(s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab).card ≤ ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab).card

theorem Finset.disjoint_add_sub_card_le {α : Type u_1} [AddCommGroup α] [DecidableEq α] {a : α} (b : α) {s t C : Finset α} (has : a ∈ s) (hsC : Disjoint t (a +ᵥ C.addStab)) (hst : (s ∩ (a +ᵥ C.addStab) + t ∩ (b +ᵥ C.addStab)).addStab ⊆ C.addStab) : ↑C.addStab.card - ↑(s ∩ (a +ᵥ C.addStab) + (s ∩ (a +ᵥ C.addStab) + t ∩ (b +ᵥ C.addStab)).addStab).card ≤ ↑(s ∪ t + C.addStab).card - ↑(s ∪ t + (s ∩ (a +ᵥ C.addStab) + t ∩ (b +ᵥ C.addStab)).addStab).card

theorem Finset.inter_mul_sub_card_le {α : Type u_1} [CommGroup α] [DecidableEq α] {a : α} {s t C : Finset α} (has : a ∈ s) (hst : (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab ⊆ C.mulStab) : ↑C.mulStab.card - ↑(s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card - ↑(t ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card ≤ ↑((s ∪ t) * C.mulStab).card - ↑((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card

theorem Finset.inter_add_sub_card_le {α : Type u_1} [AddCommGroup α] [DecidableEq α] {a : α} {s t C : Finset α} (has : a ∈ s) (hst : (s ∩ (a +ᵥ C.addStab) + t ∩ (a +ᵥ C.addStab)).addStab ⊆ C.addStab) : ↑C.addStab.card - ↑(s ∩ (a +ᵥ C.addStab) + (s ∩ (a +ᵥ C.addStab) + t ∩ (a +ᵥ C.addStab)).addStab).card - ↑(t ∩ (a +ᵥ C.addStab) + (s ∩ (a +ᵥ C.addStab) + t ∩ (a +ᵥ C.addStab)).addStab).card ≤ ↑(s ∪ t + C.addStab).card - ↑(s ∪ t + (s ∩ (a +ᵥ C.addStab) + t ∩ (a +ᵥ C.addStab)).addStab).card

Kneser's theorem

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 theorem: 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 theorem: 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.