mathlib3 documentation

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 #

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 : finset α × finset α) :

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 α] [add_comm_group α] (e : α) (x : finset α × finset α) :
@[simp]
theorem finset.add_dyson_e_transform_fst {α : Type u_1} [decidable_eq α] [add_comm_group α] (e : α) (x : finset α × finset α) :
@[simp]
@[simp]
theorem finset.mul_dyson_e_transform_fst {α : Type u_1} [decidable_eq α] [comm_group α] (e : α) (x : finset α × finset α) :
def finset.add_dyson_e_transform {α : Type u_1} [decidable_eq α] [add_comm_group α] (e : α) (x : finset α × finset α) :

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

Equations

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 : finset α × finset α) :

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 : finset α × finset α) :

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

Equations
@[simp]
@[simp]
@[simp]
theorem finset.mul_e_transform_left_snd {α : Type u_1} [decidable_eq α] [group α] (e : α) (x : finset α × finset α) :
@[simp]
theorem finset.add_e_transform_left_snd {α : Type u_1} [decidable_eq α] [add_group α] (e : α) (x : finset α × finset α) :
@[simp]
theorem finset.mul_e_transform_right_snd {α : Type u_1} [decidable_eq α] [group α] (e : α) (x : finset α × finset α) :
@[simp]
theorem finset.add_e_transform_right_snd {α : Type u_1} [decidable_eq α] [add_group α] (e : α) (x : finset α × finset α) :
@[simp]
@[simp]
def finset.mul_e_transform_right {α : Type u_1} [decidable_eq α] [group α] (e : α) (x : finset α × finset α) :

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 : finset α × finset α) :

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

Equations
@[simp]
@[simp]
@[protected]

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

@[protected]

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