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 (seefinset.mul_e_transform.card). In particular, one of the two transforms increases the sum of the cardinalities and the other one decreases it. Seele_or_lt_of_add_le_addand 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 : finset α × finset α) :
The Dyson e-transform. Turns (s, t) into (s ∪ e • t, t ∩ e⁻¹ • s). This reduces the
product of the two sets.
@[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]
theorem
finset.mul_dyson_e_transform_snd
{α : Type u_1}
[decidable_eq α]
[comm_group α]
(e : α)
(x : finset α × finset α) :
@[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.
theorem
finset.add_dyson_e_transform.subset
{α : Type u_1}
[decidable_eq α]
[add_comm_group α]
(e : α)
(x : finset α × finset α) :
(finset.add_dyson_e_transform e x).fst + (finset.add_dyson_e_transform e x).snd ⊆ x.fst + x.snd
theorem
finset.mul_dyson_e_transform.subset
{α : Type u_1}
[decidable_eq α]
[comm_group α]
(e : α)
(x : finset α × finset α) :
(finset.mul_dyson_e_transform e x).fst * (finset.mul_dyson_e_transform e x).snd ⊆ x.fst * x.snd
theorem
finset.add_dyson_e_transform.card
{α : Type u_1}
[decidable_eq α]
[add_comm_group α]
(e : α)
(x : finset α × finset α) :
theorem
finset.mul_dyson_e_transform.card
{α : Type u_1}
[decidable_eq α]
[comm_group α]
(e : α)
(x : finset α × finset α) :
@[simp]
theorem
finset.mul_dyson_e_transform_idem
{α : Type u_1}
[decidable_eq α]
[comm_group α]
(e : α)
(x : finset α × finset α) :
@[simp]
theorem
finset.add_dyson_e_transform_idem
{α : Type u_1}
[decidable_eq α]
[add_comm_group α]
(e : α)
(x : finset α × finset α) :
theorem
finset.mul_dyson_e_transform.smul_finset_snd_subset_fst
{α : Type u_1}
[decidable_eq α]
[comm_group α]
{e : α}
{x : finset α × finset α} :
e • (finset.mul_dyson_e_transform e x).snd ⊆ (finset.mul_dyson_e_transform e x).fst
theorem
finset.add_dyson_e_transform.vadd_finset_snd_subset_fst
{α : Type u_1}
[decidable_eq α]
[add_comm_group α]
{e : α}
{x : finset α × finset α} :
e +ᵥ (finset.add_dyson_e_transform e x).snd ⊆ (finset.add_dyson_e_transform 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.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.
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.
@[simp]
theorem
finset.mul_e_transform_left_fst
{α : Type u_1}
[decidable_eq α]
[group α]
(e : α)
(x : finset α × finset α) :
(finset.mul_e_transform_left e x).fst = x.fst ∩ mul_opposite.op e • x.fst
@[simp]
theorem
finset.add_e_transform_left_fst
{α : Type u_1}
[decidable_eq α]
[add_group α]
(e : α)
(x : finset α × finset α) :
(finset.add_e_transform_left e x).fst = x.fst ∩ (add_opposite.op e +ᵥ x.fst)
@[simp]
theorem
finset.add_e_transform_right_fst
{α : Type u_1}
[decidable_eq α]
[add_group α]
(e : α)
(x : finset α × finset α) :
(finset.add_e_transform_right e x).fst = x.fst ∪ (add_opposite.op e +ᵥ x.fst)
@[simp]
theorem
finset.mul_e_transform_right_fst
{α : Type u_1}
[decidable_eq α]
[group α]
(e : α)
(x : finset α × finset α) :
(finset.mul_e_transform_right e x).fst = x.fst ∪ mul_opposite.op e • x.fst
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.
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.
@[simp]
theorem
finset.add_e_transform_left_zero
{α : Type u_1}
[decidable_eq α]
[add_group α]
(x : finset α × finset α) :
finset.add_e_transform_left 0 x = x
@[simp]
theorem
finset.mul_e_transform_left_one
{α : Type u_1}
[decidable_eq α]
[group α]
(x : finset α × finset α) :
finset.mul_e_transform_left 1 x = x
@[simp]
theorem
finset.mul_e_transform_right_one
{α : Type u_1}
[decidable_eq α]
[group α]
(x : finset α × finset α) :
@[simp]
theorem
finset.add_e_transform_right_zero
{α : Type u_1}
[decidable_eq α]
[add_group α]
(x : finset α × finset α) :
theorem
finset.add_e_transform_left.fst_add_snd_subset
{α : Type u_1}
[decidable_eq α]
[add_group α]
(e : α)
(x : finset α × finset α) :
(finset.add_e_transform_left e x).fst + (finset.add_e_transform_left e x).snd ⊆ x.fst + x.snd
theorem
finset.mul_e_transform_left.fst_mul_snd_subset
{α : Type u_1}
[decidable_eq α]
[group α]
(e : α)
(x : finset α × finset α) :
(finset.mul_e_transform_left e x).fst * (finset.mul_e_transform_left e x).snd ⊆ x.fst * x.snd
theorem
finset.add_e_transform_right.fst_add_snd_subset
{α : Type u_1}
[decidable_eq α]
[add_group α]
(e : α)
(x : finset α × finset α) :
(finset.add_e_transform_right e x).fst + (finset.add_e_transform_right e x).snd ⊆ x.fst + x.snd
theorem
finset.mul_e_transform_right.fst_mul_snd_subset
{α : Type u_1}
[decidable_eq α]
[group α]
(e : α)
(x : finset α × finset α) :
(finset.mul_e_transform_right e x).fst * (finset.mul_e_transform_right e x).snd ⊆ x.fst * x.snd
theorem
finset.mul_e_transform_left.card
{α : Type u_1}
[decidable_eq α]
[group α]
(e : α)
(x : finset α × finset α) :
theorem
finset.add_e_transform_left.card
{α : Type u_1}
[decidable_eq α]
[add_group α]
(e : α)
(x : finset α × finset α) :
theorem
finset.mul_e_transform_right.card
{α : Type u_1}
[decidable_eq α]
[group α]
(e : α)
(x : finset α × finset α) :
theorem
finset.add_e_transform_right.card
{α : Type u_1}
[decidable_eq α]
[add_group α]
(e : α)
(x : finset α × finset α) :
@[protected]
theorem
add_e_transform.card
{α : Type u_1}
[decidable_eq α]
[add_group α]
(e : α)
(x : finset α × finset α) :
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 : finset α × finset α) :
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 α]
[add_comm_group α]
(e : α)
(x : finset α × finset α) :
@[simp]
theorem
finset.mul_e_transform_left_inv
{α : Type u_1}
[decidable_eq α]
[comm_group α]
(e : α)
(x : finset α × finset α) :
@[simp]
theorem
finset.add_e_transform_right_neg
{α : Type u_1}
[decidable_eq α]
[add_comm_group α]
(e : α)
(x : finset α × finset α) :
@[simp]
theorem
finset.mul_e_transform_right_inv
{α : Type u_1}
[decidable_eq α]
[comm_group α]
(e : α)
(x : finset α × finset α) :