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.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)
:
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'))
:
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'))
:
theorem
Finset.disjoint_vadd_addStab
{α : Type u_1}
[AddCommGroup α]
[DecidableEq α]
{s t : Finset α}
{a : α}
(hst : s ⊆ t)
(has : ¬a +ᵥ s.addStab ⊆ t)
:
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)
:
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)
:
Kneser's theorem #
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)
:
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)
:
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.