# mathlib3documentation

combinatorics.additive.e_transform

# e-transforms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

e-transforms are a family of transformations of pairs of finite sets that aim to reduce the size of the sumset while keeping some invariant the same. This file defines a few of them, to be used as internals of other proofs.

## Main declarations #

• finset.mul_dyson_e_transform: The Dyson e-transform. Replaces (s, t) by (s ∪ e • t, t ∩ e⁻¹ • s). The additive version preserves |s ∩ [1, m]| + |t ∩ [1, m - e]|.
• finset.mul_e_transform_left/finset.mul_e_transform_right: Replace (s, t) by (s ∩ s • e, t ∪ e⁻¹ • t) and (s ∪ s • e, t ∩ e⁻¹ • t). Preserve (together) the sum of the cardinalities (see finset.mul_e_transform.card). In particular, one of the two transforms increases the sum of the cardinalities and the other one decreases it. See le_or_lt_of_add_le_add and around.

## TODO #

Prove the invariance property of the Dyson e-transform.

### Dyson e-transform #

def finset.mul_dyson_e_transform {α : Type u_1} [decidable_eq α] [comm_group α] (e : α) (x : × ) :
×

The Dyson e-transform. Turns (s, t) into (s ∪ e • t, t ∩ e⁻¹ • s). This reduces the product of the two sets.

Equations
@[simp]
theorem finset.add_dyson_e_transform_snd {α : Type u_1} [decidable_eq α] (e : α) (x : × ) :
= x.snd (-e +ᵥ x.fst)
@[simp]
theorem finset.add_dyson_e_transform_fst {α : Type u_1} [decidable_eq α] (e : α) (x : × ) :
= x.fst (e +ᵥ x.snd)
@[simp]
theorem finset.mul_dyson_e_transform_snd {α : Type u_1} [decidable_eq α] [comm_group α] (e : α) (x : × ) :
@[simp]
theorem finset.mul_dyson_e_transform_fst {α : Type u_1} [decidable_eq α] [comm_group α] (e : α) (x : × ) :
= x.fst e x.snd
def finset.add_dyson_e_transform {α : Type u_1} [decidable_eq α] (e : α) (x : × ) :
×

The Dyson e-transform. Turns (s, t) into (s ∪ e +ᵥ t, t ∩ -e +ᵥ s). This reduces the sum of the two sets.

Equations
theorem finset.add_dyson_e_transform.subset {α : Type u_1} [decidable_eq α] (e : α) (x : × ) :
x.fst + x.snd
theorem finset.mul_dyson_e_transform.subset {α : Type u_1} [decidable_eq α] [comm_group α] (e : α) (x : × ) :
x.fst * x.snd
theorem finset.add_dyson_e_transform.card {α : Type u_1} [decidable_eq α] (e : α) (x : × ) :
theorem finset.mul_dyson_e_transform.card {α : Type u_1} [decidable_eq α] [comm_group α] (e : α) (x : × ) :
@[simp]
theorem finset.mul_dyson_e_transform_idem {α : Type u_1} [decidable_eq α] [comm_group α] (e : α) (x : × ) :
@[simp]
theorem finset.add_dyson_e_transform_idem {α : Type u_1} [decidable_eq α] (e : α) (x : × ) :

### Two unnamed e-transforms #

The following two transforms both reduce the product/sum of the two sets. Further, one of them must decrease the sum of the size of the sets (and then the other increases it).

This pair of transforms doesn't seem to be named in the literature. It is used by Sanders in his bound on Roth numbers, and by DeVos in his proof of Cauchy-Davenport.

def finset.add_e_transform_left {α : Type u_1} [decidable_eq α] [add_group α] (e : α) (x : × ) :
×

An e-transform. Turns (s, t) into (s ∩ s +ᵥ e, t ∪ -e +ᵥ t). This reduces the sum of the two sets.

Equations
def finset.mul_e_transform_left {α : Type u_1} [decidable_eq α] [group α] (e : α) (x : × ) :
×

An e-transform. Turns (s, t) into (s ∩ s • e, t ∪ e⁻¹ • t). This reduces the product of the two sets.

Equations
@[simp]
theorem finset.mul_e_transform_left_fst {α : Type u_1} [decidable_eq α] [group α] (e : α) (x : × ) :
= x.fst
@[simp]
theorem finset.add_e_transform_left_fst {α : Type u_1} [decidable_eq α] [add_group α] (e : α) (x : × ) :
= x.fst +ᵥ x.fst)
@[simp]
theorem finset.mul_e_transform_left_snd {α : Type u_1} [decidable_eq α] [group α] (e : α) (x : × ) :
@[simp]
theorem finset.add_e_transform_left_snd {α : Type u_1} [decidable_eq α] [add_group α] (e : α) (x : × ) :
= x.snd (-e +ᵥ x.snd)
@[simp]
theorem finset.mul_e_transform_right_snd {α : Type u_1} [decidable_eq α] [group α] (e : α) (x : × ) :
@[simp]
theorem finset.add_e_transform_right_snd {α : Type u_1} [decidable_eq α] [add_group α] (e : α) (x : × ) :
= x.snd (-e +ᵥ x.snd)
@[simp]
theorem finset.add_e_transform_right_fst {α : Type u_1} [decidable_eq α] [add_group α] (e : α) (x : × ) :
= x.fst +ᵥ x.fst)
@[simp]
theorem finset.mul_e_transform_right_fst {α : Type u_1} [decidable_eq α] [group α] (e : α) (x : × ) :
= x.fst
def finset.mul_e_transform_right {α : Type u_1} [decidable_eq α] [group α] (e : α) (x : × ) :
×

An e-transform. Turns (s, t) into (s ∪ s • e, t ∩ e⁻¹ • t). This reduces the product of the two sets.

Equations
def finset.add_e_transform_right {α : Type u_1} [decidable_eq α] [add_group α] (e : α) (x : × ) :
×

An e-transform. Turns (s, t) into (s ∪ s +ᵥ e, t ∩ -e +ᵥ t). This reduces the sum of the two sets.

Equations
@[simp]
theorem finset.add_e_transform_left_zero {α : Type u_1} [decidable_eq α] [add_group α] (x : × ) :
@[simp]
theorem finset.mul_e_transform_left_one {α : Type u_1} [decidable_eq α] [group α] (x : × ) :
@[simp]
theorem finset.mul_e_transform_right_one {α : Type u_1} [decidable_eq α] [group α] (x : × ) :
@[simp]
theorem finset.add_e_transform_right_zero {α : Type u_1} [decidable_eq α] [add_group α] (x : × ) :
theorem finset.add_e_transform_left.fst_add_snd_subset {α : Type u_1} [decidable_eq α] [add_group α] (e : α) (x : × ) :
x.fst + x.snd
theorem finset.mul_e_transform_left.fst_mul_snd_subset {α : Type u_1} [decidable_eq α] [group α] (e : α) (x : × ) :
x.fst * x.snd
theorem finset.add_e_transform_right.fst_add_snd_subset {α : Type u_1} [decidable_eq α] [add_group α] (e : α) (x : × ) :
x.fst + x.snd
theorem finset.mul_e_transform_right.fst_mul_snd_subset {α : Type u_1} [decidable_eq α] [group α] (e : α) (x : × ) :
x.fst * x.snd
theorem finset.mul_e_transform_left.card {α : Type u_1} [decidable_eq α] [group α] (e : α) (x : × ) :
= 2 * x.fst.card
theorem finset.add_e_transform_left.card {α : Type u_1} [decidable_eq α] [add_group α] (e : α) (x : × ) :
= 2 * x.fst.card
theorem finset.mul_e_transform_right.card {α : Type u_1} [decidable_eq α] [group α] (e : α) (x : × ) :
= 2 * x.snd.card
theorem finset.add_e_transform_right.card {α : Type u_1} [decidable_eq α] [add_group α] (e : α) (x : × ) :
= 2 * x.snd.card
@[protected]
theorem add_e_transform.card {α : Type u_1} [decidable_eq α] [add_group α] (e : α) (x : × ) :
+ .fst.card + .card) = x.fst.card + x.snd.card + (x.fst.card + x.snd.card)

This statement is meant to be combined with le_or_lt_of_add_le_add and similar lemmas.

@[protected]
theorem finset.mul_e_transform.card {α : Type u_1} [decidable_eq α] [group α] (e : α) (x : × ) :
+ .fst.card + .card) = x.fst.card + x.snd.card + (x.fst.card + x.snd.card)

This statement is meant to be combined with le_or_lt_of_add_le_add and similar lemmas.

@[simp]
theorem finset.add_e_transform_left_neg {α : Type u_1} [decidable_eq α] (e : α) (x : × ) :
@[simp]
theorem finset.mul_e_transform_left_inv {α : Type u_1} [decidable_eq α] [comm_group α] (e : α) (x : × ) :
@[simp]
theorem finset.add_e_transform_right_neg {α : Type u_1} [decidable_eq α] (e : α) (x : × ) :
@[simp]
theorem finset.mul_e_transform_right_inv {α : Type u_1} [decidable_eq α] [comm_group α] (e : α) (x : × ) :