Sets with very small doubling #
This file characterises sets with no doubling (finsets A such that #(A ^ 2) = #A) as the sets
which are either empty or translates of a subgroup.
For the converse, use the existing facts from the pointwise API: ∅ ^ 2 = ∅ (Finset.empty_pow),
(a • H) ^ 2 = a ^ 2 • H ^ 2 = a ^ 2 • H (smul_pow, coe_set_pow)
TODO #
- Do we need a version stated using the doubling constant (
Finset.mulConst)? - Add characterisation for sets with doubling < 3/2
theorem
Finset.smul_stabilizer_of_no_doubling
{G : Type u_1}
[Group G]
[DecidableEq G]
{A : Finset G}
{a : G}
(hA : (A * A).card ≤ A.card)
(ha : a ∈ A)
:
a • ↑(MulAction.stabilizer G A) = ↑A
A non-empty set with no doubling is the left translate of its stabilizer.
theorem
Finset.vadd_stabilizer_of_no_doubling
{G : Type u_1}
[AddGroup G]
[DecidableEq G]
{A : Finset G}
{a : G}
(hA : (A + A).card ≤ A.card)
(ha : a ∈ A)
:
a +ᵥ ↑(AddAction.stabilizer G A) = ↑A
A non-empty set with no doubling is the left-translate of its stabilizer.
theorem
Finset.op_smul_stabilizer_of_no_doubling
{G : Type u_1}
[Group G]
[DecidableEq G]
{A : Finset G}
{a : G}
(hA : (A * A).card ≤ A.card)
(ha : a ∈ A)
:
MulOpposite.op a • ↑(MulAction.stabilizer G A) = ↑A
A non-empty set with no doubling is the right translate of its stabilizer.
theorem
Finset.op_vadd_stabilizer_of_no_doubling
{G : Type u_1}
[AddGroup G]
[DecidableEq G]
{A : Finset G}
{a : G}
(hA : (A + A).card ≤ A.card)
(ha : a ∈ A)
:
AddOpposite.op a +ᵥ ↑(AddAction.stabilizer G A) = ↑A
A non-empty set with no doubling is the right translate of its stabilizer.