Skip to content

Commit

Permalink
chore: Fix capitalisation of e-transforms (#8203)
Browse files Browse the repository at this point in the history 
Everything was wrong here.
  • Loading branch information
@YaelDillies
YaelDillies committed Nov 7, 2023
1 parent a051ac5 commit 251baaf
Show file tree
Hide file tree
Showing 2 changed files with 66 additions and 66 deletions.
2 changes: 1 addition & 1 deletion Mathlib.lean
View file
Expand Up @@ -1260,8 +1260,8 @@ import Mathlib.CategoryTheory.Whiskering
import Mathlib.CategoryTheory.WithTerminal
import Mathlib.CategoryTheory.Yoneda
import Mathlib.Combinatorics.Additive.Behrend
import Mathlib.Combinatorics.Additive.ETransform
import Mathlib.Combinatorics.Additive.Energy
import Mathlib.Combinatorics.Additive.Etransform
import Mathlib.Combinatorics.Additive.PluenneckeRuzsa
import Mathlib.Combinatorics.Additive.RuzsaCovering
import Mathlib.Combinatorics.Additive.SalemSpencer
Expand Down
130 changes: 65 additions & 65 deletions ...ib/Combinatorics/Additive/Etransform.lean → ...ib/Combinatorics/Additive/ETransform.lean
View file
Expand Up @@ -16,11 +16,11 @@ as internals of other proofs.
## Main declarations
* `Finset.mulDysonEtransform`: The Dyson e-transform. Replaces `(s, t)` by
* `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
* `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
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.
Expand Down Expand Up @@ -49,49 +49,49 @@ variable [CommGroup α] (e : α) (x : Finset α × Finset α)
product of the two sets. -/
@[to_additive (attr := simps) "The **Dyson e-transform**.
Turns `(s, t)` into `(s ∪ e +ᵥ t, t ∩ -e +ᵥ s)`. This reduces the sum of the two sets."]
def mulDysonEtransform : Finset α × Finset α :=
def mulDysonETransform : Finset α × Finset α :=
(x.1 ∪ e • x.2, x.2 ∩ e⁻¹ • x.1)
#align finset.mul_dyson_e_transform Finset.mulDysonEtransform
#align finset.add_dyson_e_transform Finset.addDysonEtransform
#align finset.mul_dyson_e_transform Finset.mulDysonETransform
#align finset.add_dyson_e_transform Finset.addDysonETransform

@[to_additive]
theorem mulDysonEtransform.subset :
(mulDysonEtransform e x).1 * (mulDysonEtransform e x).2 ⊆ x.1 * x.2 := by
theorem mulDysonETransform.subset :
(mulDysonETransform e x).1 * (mulDysonETransform e x).2 ⊆ x.1 * x.2 := by
refine' union_mul_inter_subset_union.trans (union_subset Subset.rfl _)
rw [mul_smul_comm, smul_mul_assoc, inv_smul_smul, mul_comm]
#align finset.mul_dyson_e_transform.subset Finset.mulDysonEtransform.subset
#align finset.add_dyson_e_transform.subset Finset.addDysonEtransform.subset
#align finset.mul_dyson_e_transform.subset Finset.mulDysonETransform.subset
#align finset.add_dyson_e_transform.subset Finset.addDysonETransform.subset

@[to_additive]
theorem mulDysonEtransform.card :
(mulDysonEtransform e x).1.card + (mulDysonEtransform e x).2.card = x.1.card + x.2.card := by
theorem mulDysonETransform.card :
(mulDysonETransform e x).1.card + (mulDysonETransform e x).2.card = x.1.card + x.2.card := by
dsimp
rw [← card_smul_finset e (_ ∩ _), smul_finset_inter, smul_inv_smul, inter_comm,
card_union_add_card_inter, card_smul_finset]
#align finset.mul_dyson_e_transform.card Finset.mulDysonEtransform.card
#align finset.add_dyson_e_transform.card Finset.addDysonEtransform.card
#align finset.mul_dyson_e_transform.card Finset.mulDysonETransform.card
#align finset.add_dyson_e_transform.card Finset.addDysonETransform.card

@[to_additive (attr := simp)]
theorem mulDysonEtransform_idem :
mulDysonEtransform e (mulDysonEtransform e x) = mulDysonEtransform e x := by
theorem mulDysonETransform_idem :
mulDysonETransform e (mulDysonETransform e x) = mulDysonETransform e x := by
ext : 1 <;> dsimp
· rw [smul_finset_inter, smul_inv_smul, inter_comm, union_eq_left]
exact inter_subset_union
· rw [smul_finset_union, inv_smul_smul, union_comm, inter_eq_left]
exact inter_subset_union
#align finset.mul_dyson_e_transform_idem Finset.mulDysonEtransform_idem
#align finset.add_dyson_e_transform_idem Finset.addDysonEtransform_idem
#align finset.mul_dyson_e_transform_idem Finset.mulDysonETransform_idem
#align finset.add_dyson_e_transform_idem Finset.addDysonETransform_idem

variable {e x}

@[to_additive]
theorem mulDysonEtransform.smul_finset_snd_subset_fst :
e • (mulDysonEtransform e x).2 ⊆ (mulDysonEtransform e x).1 := by
theorem mulDysonETransform.smul_finset_snd_subset_fst :
e • (mulDysonETransform e x).2 ⊆ (mulDysonETransform e x).1 := by
dsimp
rw [smul_finset_inter, smul_inv_smul, inter_comm]
exact inter_subset_union
#align finset.mul_dyson_e_transform.smul_finset_snd_subset_fst Finset.mulDysonEtransform.smul_finset_snd_subset_fst
#align finset.add_dyson_e_transform.vadd_finset_snd_subset_fst Finset.addDysonEtransform.vadd_finset_snd_subset_fst
#align finset.mul_dyson_e_transform.smul_finset_snd_subset_fst Finset.mulDysonETransform.smul_finset_snd_subset_fst
#align finset.add_dyson_e_transform.vadd_finset_snd_subset_fst Finset.addDysonETransform.vadd_finset_snd_subset_fst

end CommGroup

Expand All @@ -114,70 +114,70 @@ variable [Group α] (e : α) (x : Finset α × Finset α)
product of the two sets. -/
@[to_additive (attr := simps) "An **e-transform**.
Turns `(s, t)` into `(s ∩ s +ᵥ e, t ∪ -e +ᵥ t)`. This reduces the sum of the two sets."]
def mulEtransformLeft : Finset α × Finset α :=
def mulETransformLeft : Finset α × Finset α :=
(x.1 ∩ op e • x.1, x.2 ∪ e⁻¹ • x.2)
#align finset.mul_e_transform_left Finset.mulEtransformLeft
#align finset.add_e_transform_left Finset.addEtransformLeft
#align finset.mul_e_transform_left Finset.mulETransformLeft
#align finset.add_e_transform_left Finset.addETransformLeft

/-- An **e-transform**. Turns `(s, t)` into `(s ∪ s • e, t ∩ e⁻¹ • t)`. This reduces the
product of the two sets. -/
@[to_additive (attr := simps) "An **e-transform**.
Turns `(s, t)` into `(s ∪ s +ᵥ e, t ∩ -e +ᵥ t)`. This reduces the sum of the two sets."]
def mulEtransformRight : Finset α × Finset α :=
def mulETransformRight : Finset α × Finset α :=
(x.1 ∪ op e • x.1, x.2 ∩ e⁻¹ • x.2)
#align finset.mul_e_transform_right Finset.mulEtransformRight
#align finset.add_e_transform_right Finset.addEtransformRight
#align finset.mul_e_transform_right Finset.mulETransformRight
#align finset.add_e_transform_right Finset.addETransformRight

@[to_additive (attr := simp)]
theorem mulEtransformLeft_one : mulEtransformLeft 1 x = x := by simp [mulEtransformLeft]
#align finset.mul_e_transform_left_one Finset.mulEtransformLeft_one
#align finset.add_e_transform_left_zero Finset.addEtransformLeft_zero
theorem mulETransformLeft_one : mulETransformLeft 1 x = x := by simp [mulETransformLeft]
#align finset.mul_e_transform_left_one Finset.mulETransformLeft_one
#align finset.add_e_transform_left_zero Finset.addETransformLeft_zero

@[to_additive (attr := simp)]
theorem mulEtransformRight_one : mulEtransformRight 1 x = x := by simp [mulEtransformRight]
#align finset.mul_e_transform_right_one Finset.mulEtransformRight_one
#align finset.add_e_transform_right_zero Finset.addEtransformRight_zero
theorem mulETransformRight_one : mulETransformRight 1 x = x := by simp [mulETransformRight]
#align finset.mul_e_transform_right_one Finset.mulETransformRight_one
#align finset.add_e_transform_right_zero Finset.addETransformRight_zero

@[to_additive]
theorem mulEtransformLeft.fst_mul_snd_subset :
(mulEtransformLeft e x).1 * (mulEtransformLeft e x).2 ⊆ x.1 * x.2 := by
theorem mulETransformLeft.fst_mul_snd_subset :
(mulETransformLeft e x).1 * (mulETransformLeft e x).2 ⊆ x.1 * x.2 := by
refine' inter_mul_union_subset_union.trans (union_subset Subset.rfl _)
rw [op_smul_finset_mul_eq_mul_smul_finset, smul_inv_smul]
#align finset.mul_e_transform_left.fst_mul_snd_subset Finset.mulEtransformLeft.fst_mul_snd_subset
#align finset.add_e_transform_left.fst_add_snd_subset Finset.addEtransformLeft.fst_add_snd_subset
#align finset.mul_e_transform_left.fst_mul_snd_subset Finset.mulETransformLeft.fst_mul_snd_subset
#align finset.add_e_transform_left.fst_add_snd_subset Finset.addETransformLeft.fst_add_snd_subset

@[to_additive]
theorem mulEtransformRight.fst_mul_snd_subset :
(mulEtransformRight e x).1 * (mulEtransformRight e x).2 ⊆ x.1 * x.2 := by
theorem mulETransformRight.fst_mul_snd_subset :
(mulETransformRight e x).1 * (mulETransformRight e x).2 ⊆ x.1 * x.2 := by
refine' union_mul_inter_subset_union.trans (union_subset Subset.rfl _)
rw [op_smul_finset_mul_eq_mul_smul_finset, smul_inv_smul]
#align finset.mul_e_transform_right.fst_mul_snd_subset Finset.mulEtransformRight.fst_mul_snd_subset
#align finset.add_e_transform_right.fst_add_snd_subset Finset.addEtransformRight.fst_add_snd_subset
#align finset.mul_e_transform_right.fst_mul_snd_subset Finset.mulETransformRight.fst_mul_snd_subset
#align finset.add_e_transform_right.fst_add_snd_subset Finset.addETransformRight.fst_add_snd_subset

@[to_additive]
theorem mulEtransformLeft.card :
(mulEtransformLeft e x).1.card + (mulEtransformRight e x).1.card = 2 * x.1.card :=
theorem mulETransformLeft.card :
(mulETransformLeft e x).1.card + (mulETransformRight e x).1.card = 2 * x.1.card :=
(card_inter_add_card_union _ _).trans <| by rw [card_smul_finset, two_mul]
#align finset.mul_e_transform_left.card Finset.mulEtransformLeft.card
#align finset.add_e_transform_left.card Finset.addEtransformLeft.card
#align finset.mul_e_transform_left.card Finset.mulETransformLeft.card
#align finset.add_e_transform_left.card Finset.addETransformLeft.card

@[to_additive]
theorem mulEtransformRight.card :
(mulEtransformLeft e x).2.card + (mulEtransformRight e x).2.card = 2 * x.2.card :=
theorem mulETransformRight.card :
(mulETransformLeft e x).2.card + (mulETransformRight e x).2.card = 2 * x.2.card :=
(card_union_add_card_inter _ _).trans <| by rw [card_smul_finset, two_mul]
#align finset.mul_e_transform_right.card Finset.mulEtransformRight.card
#align finset.add_e_transform_right.card Finset.addEtransformRight.card
#align finset.mul_e_transform_right.card Finset.mulETransformRight.card
#align finset.add_e_transform_right.card Finset.addETransformRight.card

/-- This statement is meant to be combined with `le_or_lt_of_add_le_add` and similar lemmas. -/
@[to_additive AddEtransform.card "This statement is meant to be combined with
@[to_additive AddETransform.card "This statement is meant to be combined with
`le_or_lt_of_add_le_add` and similar lemmas."]
protected theorem MulEtransform.card :
(mulEtransformLeft e x).1.card + (mulEtransformLeft e x).2.card +
((mulEtransformRight e x).1.card + (mulEtransformRight e x).2.card) =
protected theorem MulETransform.card :
(mulETransformLeft e x).1.card + (mulETransformLeft e x).2.card +
((mulETransformRight e x).1.card + (mulETransformRight e x).2.card) =
x.1.card + x.2.card + (x.1.card + x.2.card) := by
rw [add_add_add_comm, mulEtransformLeft.card, mulEtransformRight.card, ← mul_add, two_mul]
#align finset.mul_e_transform.card Finset.MulEtransform.card
#align finset.add_e_transform.card Finset.AddEtransform.card
rw [add_add_add_comm, mulETransformLeft.card, mulETransformRight.card, ← mul_add, two_mul]
#align finset.mul_e_transform.card Finset.MulETransform.card
#align finset.add_e_transform.card Finset.AddETransform.card

end Group

Expand All @@ -186,16 +186,16 @@ section CommGroup
variable [CommGroup α] (e : α) (x : Finset α × Finset α)

@[to_additive (attr := simp)]
theorem mulEtransformLeft_inv : mulEtransformLeft e⁻¹ x = (mulEtransformRight e x.swap).swap := by
simp [-op_inv, op_smul_eq_smul, mulEtransformLeft, mulEtransformRight]
#align finset.mul_e_transform_left_inv Finset.mulEtransformLeft_inv
#align finset.add_e_transform_left_neg Finset.addEtransformLeft_neg
theorem mulETransformLeft_inv : mulETransformLeft e⁻¹ x = (mulETransformRight e x.swap).swap := by
simp [-op_inv, op_smul_eq_smul, mulETransformLeft, mulETransformRight]
#align finset.mul_e_transform_left_inv Finset.mulETransformLeft_inv
#align finset.add_e_transform_left_neg Finset.addETransformLeft_neg

@[to_additive (attr := simp)]
theorem mulEtransformRight_inv : mulEtransformRight e⁻¹ x = (mulEtransformLeft e x.swap).swap := by
simp [-op_inv, op_smul_eq_smul, mulEtransformLeft, mulEtransformRight]
#align finset.mul_e_transform_right_inv Finset.mulEtransformRight_inv
#align finset.add_e_transform_right_neg Finset.addEtransformRight_neg
theorem mulETransformRight_inv : mulETransformRight e⁻¹ x = (mulETransformLeft e x.swap).swap := by
simp [-op_inv, op_smul_eq_smul, mulETransformLeft, mulETransformRight]
#align finset.mul_e_transform_right_inv Finset.mulETransformRight_inv
#align finset.add_e_transform_right_neg Finset.addETransformRight_neg

end CommGroup

Expand Down

0 comments on commit 251baaf

Please sign in to comment.