e-transforms

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.mulDysonEtransform: 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.mulEtransformLeft/Finset.mulEtransformRight: 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.MulEtransform.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.addDysonEtransform {α : Type u_1} [DecidableEq α] [AddCommGroup α] (e : α) (x : Finset α × Finset α) : Finset α × Finset α

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

@[simp]

theorem Finset.addDysonEtransform_fst {α : Type u_1} [DecidableEq α] [AddCommGroup α] (e : α) (x : Finset α × Finset α) : (Finset.addDysonEtransform e x).fst = x.fst ∪ (e +ᵥ x.snd)

@[simp]

theorem Finset.mulDysonEtransform_snd {α : Type u_1} [DecidableEq α] [CommGroup α] (e : α) (x : Finset α × Finset α) : (Finset.mulDysonEtransform e x).snd = x.snd ∩ e⁻¹ • x.fst

@[simp]

theorem Finset.addDysonEtransform_snd {α : Type u_1} [DecidableEq α] [AddCommGroup α] (e : α) (x : Finset α × Finset α) : (Finset.addDysonEtransform e x).snd = x.snd ∩ (-e +ᵥ x.fst)

@[simp]

theorem Finset.mulDysonEtransform_fst {α : Type u_1} [DecidableEq α] [CommGroup α] (e : α) (x : Finset α × Finset α) : (Finset.mulDysonEtransform e x).fst = x.fst ∪ e • x.snd

def Finset.mulDysonEtransform {α : Type u_1} [DecidableEq α] [CommGroup α] (e : α) (x : Finset α × Finset α) : Finset α × Finset α

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

theorem Finset.addDysonEtransform.subset {α : Type u_1} [DecidableEq α] [AddCommGroup α] (e : α) (x : Finset α × Finset α) : (Finset.addDysonEtransform e x).fst + (Finset.addDysonEtransform e x).snd ⊆ x.fst + x.snd

theorem Finset.mulDysonEtransform.subset {α : Type u_1} [DecidableEq α] [CommGroup α] (e : α) (x : Finset α × Finset α) : (Finset.mulDysonEtransform e x).fst * (Finset.mulDysonEtransform e x).snd ⊆ x.fst * x.snd

theorem Finset.addDysonEtransform.card {α : Type u_1} [DecidableEq α] [AddCommGroup α] (e : α) (x : Finset α × Finset α) : Finset.card (Finset.addDysonEtransform e x).fst + Finset.card (Finset.addDysonEtransform e x).snd = Finset.card x.fst + Finset.card x.snd

theorem Finset.mulDysonEtransform.card {α : Type u_1} [DecidableEq α] [CommGroup α] (e : α) (x : Finset α × Finset α) : Finset.card (Finset.mulDysonEtransform e x).fst + Finset.card (Finset.mulDysonEtransform e x).snd = Finset.card x.fst + Finset.card x.snd

@[simp]

theorem Finset.addDysonEtransform_idem {α : Type u_1} [DecidableEq α] [AddCommGroup α] (e : α) (x : Finset α × Finset α) : Finset.addDysonEtransform e (Finset.addDysonEtransform e x) = Finset.addDysonEtransform e x

@[simp]

theorem Finset.mulDysonEtransform_idem {α : Type u_1} [DecidableEq α] [CommGroup α] (e : α) (x : Finset α × Finset α) : Finset.mulDysonEtransform e (Finset.mulDysonEtransform e x) = Finset.mulDysonEtransform e x

theorem Finset.addDysonEtransform.vadd_finset_snd_subset_fst {α : Type u_1} [DecidableEq α] [AddCommGroup α] {e : α} {x : Finset α × Finset α} : e +ᵥ (Finset.addDysonEtransform e x).snd ⊆ (Finset.addDysonEtransform e x).fst

theorem Finset.mulDysonEtransform.smul_finset_snd_subset_fst {α : Type u_1} [DecidableEq α] [CommGroup α] {e : α} {x : Finset α × Finset α} : e • (Finset.mulDysonEtransform e x).snd ⊆ (Finset.mulDysonEtransform e x).fst

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.addEtransformLeft {α : Type u_1} [DecidableEq α] [AddGroup α] (e : α) (x : Finset α × Finset α) : Finset α × Finset α

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

@[simp]

theorem Finset.addEtransformLeft_snd {α : Type u_1} [DecidableEq α] [AddGroup α] (e : α) (x : Finset α × Finset α) : (Finset.addEtransformLeft e x).snd = x.snd ∪ (-e +ᵥ x.snd)

@[simp]

theorem Finset.mulEtransformLeft_fst {α : Type u_1} [DecidableEq α] [Group α] (e : α) (x : Finset α × Finset α) : (Finset.mulEtransformLeft e x).fst = x.fst ∩ MulOpposite.op e • x.fst

@[simp]

theorem Finset.mulEtransformLeft_snd {α : Type u_1} [DecidableEq α] [Group α] (e : α) (x : Finset α × Finset α) : (Finset.mulEtransformLeft e x).snd = x.snd ∪ e⁻¹ • x.snd

@[simp]

theorem Finset.addEtransformLeft_fst {α : Type u_1} [DecidableEq α] [AddGroup α] (e : α) (x : Finset α × Finset α) : (Finset.addEtransformLeft e x).fst = x.fst ∩ (AddOpposite.op e +ᵥ x.fst)

def Finset.mulEtransformLeft {α : Type u_1} [DecidableEq α] [Group α] (e : α) (x : Finset α × Finset α) : Finset α × Finset α

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

def Finset.addEtransformRight {α : Type u_1} [DecidableEq α] [AddGroup α] (e : α) (x : Finset α × Finset α) : Finset α × Finset α

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

@[simp]

theorem Finset.mulEtransformRight_fst {α : Type u_1} [DecidableEq α] [Group α] (e : α) (x : Finset α × Finset α) : (Finset.mulEtransformRight e x).fst = x.fst ∪ MulOpposite.op e • x.fst

@[simp]

theorem Finset.addEtransformRight_fst {α : Type u_1} [DecidableEq α] [AddGroup α] (e : α) (x : Finset α × Finset α) : (Finset.addEtransformRight e x).fst = x.fst ∪ (AddOpposite.op e +ᵥ x.fst)

@[simp]

theorem Finset.addEtransformRight_snd {α : Type u_1} [DecidableEq α] [AddGroup α] (e : α) (x : Finset α × Finset α) : (Finset.addEtransformRight e x).snd = x.snd ∩ (-e +ᵥ x.snd)

@[simp]

theorem Finset.mulEtransformRight_snd {α : Type u_1} [DecidableEq α] [Group α] (e : α) (x : Finset α × Finset α) : (Finset.mulEtransformRight e x).snd = x.snd ∩ e⁻¹ • x.snd

def Finset.mulEtransformRight {α : Type u_1} [DecidableEq α] [Group α] (e : α) (x : Finset α × Finset α) : Finset α × Finset α

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

@[simp]

theorem Finset.addEtransformLeft_zero {α : Type u_1} [DecidableEq α] [AddGroup α] (x : Finset α × Finset α) : Finset.addEtransformLeft 0 x = x

@[simp]

theorem Finset.mulEtransformLeft_one {α : Type u_1} [DecidableEq α] [Group α] (x : Finset α × Finset α) : Finset.mulEtransformLeft 1 x = x

@[simp]

theorem Finset.addEtransformRight_zero {α : Type u_1} [DecidableEq α] [AddGroup α] (x : Finset α × Finset α) : Finset.addEtransformRight 0 x = x

@[simp]

theorem Finset.mulEtransformRight_one {α : Type u_1} [DecidableEq α] [Group α] (x : Finset α × Finset α) : Finset.mulEtransformRight 1 x = x

theorem Finset.addEtransformLeft.fst_add_snd_subset {α : Type u_1} [DecidableEq α] [AddGroup α] (e : α) (x : Finset α × Finset α) : (Finset.addEtransformLeft e x).fst + (Finset.addEtransformLeft e x).snd ⊆ x.fst + x.snd

theorem Finset.mulEtransformLeft.fst_mul_snd_subset {α : Type u_1} [DecidableEq α] [Group α] (e : α) (x : Finset α × Finset α) : (Finset.mulEtransformLeft e x).fst * (Finset.mulEtransformLeft e x).snd ⊆ x.fst * x.snd

theorem Finset.addEtransformRight.fst_add_snd_subset {α : Type u_1} [DecidableEq α] [AddGroup α] (e : α) (x : Finset α × Finset α) : (Finset.addEtransformRight e x).fst + (Finset.addEtransformRight e x).snd ⊆ x.fst + x.snd

theorem Finset.mulEtransformRight.fst_mul_snd_subset {α : Type u_1} [DecidableEq α] [Group α] (e : α) (x : Finset α × Finset α) : (Finset.mulEtransformRight e x).fst * (Finset.mulEtransformRight e x).snd ⊆ x.fst * x.snd

theorem Finset.addEtransformLeft.card {α : Type u_1} [DecidableEq α] [AddGroup α] (e : α) (x : Finset α × Finset α) : Finset.card (Finset.addEtransformLeft e x).fst + Finset.card (Finset.addEtransformRight e x).fst = 2 * Finset.card x.fst

theorem Finset.mulEtransformLeft.card {α : Type u_1} [DecidableEq α] [Group α] (e : α) (x : Finset α × Finset α) : Finset.card (Finset.mulEtransformLeft e x).fst + Finset.card (Finset.mulEtransformRight e x).fst = 2 * Finset.card x.fst

theorem Finset.addEtransformRight.card {α : Type u_1} [DecidableEq α] [AddGroup α] (e : α) (x : Finset α × Finset α) : Finset.card (Finset.addEtransformLeft e x).snd + Finset.card (Finset.addEtransformRight e x).snd = 2 * Finset.card x.snd

theorem Finset.mulEtransformRight.card {α : Type u_1} [DecidableEq α] [Group α] (e : α) (x : Finset α × Finset α) : Finset.card (Finset.mulEtransformLeft e x).snd + Finset.card (Finset.mulEtransformRight e x).snd = 2 * Finset.card x.snd

theorem Finset.AddEtransform.card {α : Type u_1} [DecidableEq α] [AddGroup α] (e : α) (x : Finset α × Finset α) : Finset.card (Finset.addEtransformLeft e x).fst + Finset.card (Finset.addEtransformLeft e x).snd + (Finset.card (Finset.addEtransformRight e x).fst + Finset.card (Finset.addEtransformRight e x).snd) = Finset.card x.fst + Finset.card x.snd + (Finset.card x.fst + Finset.card x.snd)

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

theorem Finset.MulEtransform.card {α : Type u_1} [DecidableEq α] [Group α] (e : α) (x : Finset α × Finset α) : Finset.card (Finset.mulEtransformLeft e x).fst + Finset.card (Finset.mulEtransformLeft e x).snd + (Finset.card (Finset.mulEtransformRight e x).fst + Finset.card (Finset.mulEtransformRight e x).snd) = Finset.card x.fst + Finset.card x.snd + (Finset.card x.fst + Finset.card x.snd)

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

@[simp]

theorem Finset.addEtransformLeft_neg {α : Type u_1} [DecidableEq α] [AddCommGroup α] (e : α) (x : Finset α × Finset α) : Finset.addEtransformLeft (-e) x = Prod.swap (Finset.addEtransformRight e (Prod.swap x))

@[simp]

theorem Finset.mulEtransformLeft_inv {α : Type u_1} [DecidableEq α] [CommGroup α] (e : α) (x : Finset α × Finset α) : Finset.mulEtransformLeft e⁻¹ x = Prod.swap (Finset.mulEtransformRight e (Prod.swap x))

@[simp]

theorem Finset.addEtransformRight_neg {α : Type u_1} [DecidableEq α] [AddCommGroup α] (e : α) (x : Finset α × Finset α) : Finset.addEtransformRight (-e) x = Prod.swap (Finset.addEtransformLeft e (Prod.swap x))

@[simp]

theorem Finset.mulEtransformRight_inv {α : Type u_1} [DecidableEq α] [CommGroup α] (e : α) (x : Finset α × Finset α) : Finset.mulEtransformRight e⁻¹ x = Prod.swap (Finset.mulEtransformLeft e (Prod.swap x))