Documentation

Mathlib.Combinatorics.Additive.ETransform

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 #

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

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

Equations
Instances For
    @[simp]
    theorem Finset.mulDysonETransform_snd {α : Type u_1} [DecidableEq α] [CommGroup α] (e : α) (x : Finset α × Finset α) :
    @[simp]
    theorem Finset.addDysonETransform_snd {α : Type u_1} [DecidableEq α] [AddCommGroup α] (e : α) (x : Finset α × Finset α) :
    (Finset.addDysonETransform e x).2 = x.2 (-e +ᵥ x.1)
    @[simp]
    theorem Finset.mulDysonETransform_fst {α : Type u_1} [DecidableEq α] [CommGroup α] (e : α) (x : Finset α × Finset α) :
    @[simp]
    theorem Finset.addDysonETransform_fst {α : Type u_1} [DecidableEq α] [AddCommGroup α] (e : α) (x : Finset α × Finset α) :
    (Finset.addDysonETransform e x).1 = x.1 (e +ᵥ x.2)
    def Finset.mulDysonETransform {α : Type u_1} [DecidableEq α] [CommGroup α] (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
    Instances For
      theorem Finset.addDysonETransform.card {α : Type u_1} [DecidableEq α] [AddCommGroup α] (e : α) (x : Finset α × Finset α) :
      (Finset.addDysonETransform e x).1.card + (Finset.addDysonETransform e x).2.card = x.1.card + x.2.card
      theorem Finset.mulDysonETransform.card {α : Type u_1} [DecidableEq α] [CommGroup α] (e : α) (x : Finset α × Finset α) :
      (Finset.mulDysonETransform e x).1.card + (Finset.mulDysonETransform e x).2.card = x.1.card + x.2.card

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

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

      Equations
      Instances For
        @[simp]
        theorem Finset.addETransformLeft_fst {α : Type u_1} [DecidableEq α] [AddGroup α] (e : α) (x : Finset α × Finset α) :
        @[simp]
        theorem Finset.mulETransformLeft_snd {α : Type u_1} [DecidableEq α] [Group α] (e : α) (x : Finset α × Finset α) :
        @[simp]
        theorem Finset.addETransformLeft_snd {α : Type u_1} [DecidableEq α] [AddGroup α] (e : α) (x : Finset α × Finset α) :
        (Finset.addETransformLeft e x).2 = x.2 (-e +ᵥ x.2)
        @[simp]
        theorem Finset.mulETransformLeft_fst {α : Type u_1} [DecidableEq α] [Group α] (e : α) (x : Finset α × Finset α) :
        def Finset.mulETransformLeft {α : Type u_1} [DecidableEq α] [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
        Instances For
          def Finset.addETransformRight {α : Type u_1} [DecidableEq α] [AddGroup α] (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
          Instances For
            @[simp]
            theorem Finset.addETransformRight_fst {α : Type u_1} [DecidableEq α] [AddGroup α] (e : α) (x : Finset α × Finset α) :
            @[simp]
            theorem Finset.addETransformRight_snd {α : Type u_1} [DecidableEq α] [AddGroup α] (e : α) (x : Finset α × Finset α) :
            (Finset.addETransformRight e x).2 = x.2 (-e +ᵥ x.2)
            @[simp]
            theorem Finset.mulETransformRight_fst {α : Type u_1} [DecidableEq α] [Group α] (e : α) (x : Finset α × Finset α) :
            @[simp]
            theorem Finset.mulETransformRight_snd {α : Type u_1} [DecidableEq α] [Group α] (e : α) (x : Finset α × Finset α) :
            def Finset.mulETransformRight {α : Type u_1} [DecidableEq α] [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
            Instances For
              @[simp]
              @[simp]
              theorem Finset.addETransformLeft.card {α : Type u_1} [DecidableEq α] [AddGroup α] (e : α) (x : Finset α × Finset α) :
              (Finset.addETransformLeft e x).1.card + (Finset.addETransformRight e x).1.card = 2 * x.1.card
              theorem Finset.mulETransformLeft.card {α : Type u_1} [DecidableEq α] [Group α] (e : α) (x : Finset α × Finset α) :
              (Finset.mulETransformLeft e x).1.card + (Finset.mulETransformRight e x).1.card = 2 * x.1.card
              theorem Finset.addETransformRight.card {α : Type u_1} [DecidableEq α] [AddGroup α] (e : α) (x : Finset α × Finset α) :
              (Finset.addETransformLeft e x).2.card + (Finset.addETransformRight e x).2.card = 2 * x.2.card
              theorem Finset.mulETransformRight.card {α : Type u_1} [DecidableEq α] [Group α] (e : α) (x : Finset α × Finset α) :
              (Finset.mulETransformLeft e x).2.card + (Finset.mulETransformRight e x).2.card = 2 * x.2.card
              theorem Finset.AddETransform.card {α : Type u_1} [DecidableEq α] [AddGroup α] (e : α) (x : Finset α × Finset α) :
              (Finset.addETransformLeft e x).1.card + (Finset.addETransformLeft e x).2.card + ((Finset.addETransformRight e x).1.card + (Finset.addETransformRight e x).2.card) = x.1.card + x.2.card + (x.1.card + x.2.card)

              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.mulETransformLeft e x).1.card + (Finset.mulETransformLeft e x).2.card + ((Finset.mulETransformRight e x).1.card + (Finset.mulETransformRight e x).2.card) = x.1.card + x.2.card + (x.1.card + x.2.card)

              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 α) :
              @[simp]
              @[simp]
              theorem Finset.addETransformRight_neg {α : Type u_1} [DecidableEq α] [AddCommGroup α] (e : α) (x : Finset α × Finset α) :
              @[simp]