Documentation

Mathlib.Combinatorics.Additive.DoublingConst

Doubling and difference constants #

This file defines the doubling and difference constants of two finsets in a group.

def Finset.addConst {G : Type u_1} [AddGroup G] [DecidableEq G] (A : Finset G) (B : Finset G) :

The doubling constant σ[A, B] of two finsets A and B in a group is |A + B| / |A|.

The notation σ[A, B] is available in scope Combinatorics.Additive.

Equations
  • A.addConst B = (A + B).card / A.card
Instances For
    def Finset.mulConst {G : Type u_1} [Group G] [DecidableEq G] (A : Finset G) (B : Finset G) :

    The doubling constant σₘ[A, B] of two finsets A and B in a group is |A * B| / |A|.

    The notation σₘ[A, B] is available in scope Combinatorics.Additive.

    Equations
    • A.mulConst B = (A * B).card / A.card
    Instances For
      def Finset.subConst {G : Type u_1} [AddGroup G] [DecidableEq G] (A : Finset G) (B : Finset G) :

      The difference constant σ[A, B] of two finsets A and B in a group is |A - B| / |A|.

      The notation δ[A, B] is available in scope Combinatorics.Additive.

      Equations
      • A.subConst B = (A - B).card / A.card
      Instances For
        def Finset.divConst {G : Type u_1} [Group G] [DecidableEq G] (A : Finset G) (B : Finset G) :

        The difference constant δₘ[A, B] of two finsets A and B in a group is |A / B| / |A|.

        The notation δₘ[A, B] is available in scope Combinatorics.Additive.

        Equations
        • A.divConst B = (A / B).card / A.card
        Instances For

          The doubling constant σₘ[A, B] of two finsets A and B in a group is |A * B| / |A|.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Pretty printer defined by notation3 command.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              The doubling constant σₘ[A] of a finset A in a group is |A * A| / |A|.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Pretty printer defined by notation3 command.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  The doubling constant σ[A, B] of two finsets A and B in a group is |A + B| / |A|.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    Pretty printer defined by notation3 command.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      The doubling constant σ[A] of a finset A in a group is |A + A| / |A|.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        Pretty printer defined by notation3 command.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          The difference constant σₘ[A, B] of two finsets A and B in a group is |A / B| / |A|.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

                            Pretty printer defined by notation3 command.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

                              The difference constant σₘ[A] of a finset A in a group is |A / A| / |A|.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

                                Pretty printer defined by notation3 command.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  The difference constant σ[A, B] of two finsets A and B in a group is |A - B| / |A|.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    Pretty printer defined by notation3 command.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For

                                      Pretty printer defined by notation3 command.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

                                        The difference constant σ[A] of a finset A in a group is |A - A| / |A|.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[simp]
                                          theorem Finset.addConst_mul_card {G : Type u_1} [AddGroup G] [DecidableEq G] (A : Finset G) (B : Finset G) :
                                          A.addConst B * A.card = (A + B).card
                                          @[simp]
                                          theorem Finset.mulConst_mul_card {G : Type u_1} [Group G] [DecidableEq G] (A : Finset G) (B : Finset G) :
                                          A.mulConst B * A.card = (A * B).card
                                          @[simp]
                                          theorem Finset.subConst_mul_card {G : Type u_1} [AddGroup G] [DecidableEq G] (A : Finset G) (B : Finset G) :
                                          A.subConst B * A.card = (A - B).card
                                          @[simp]
                                          theorem Finset.divConst_mul_card {G : Type u_1} [Group G] [DecidableEq G] (A : Finset G) (B : Finset G) :
                                          A.divConst B * A.card = (A / B).card
                                          @[simp]
                                          theorem Finset.card_mul_addConst {G : Type u_1} [AddGroup G] [DecidableEq G] (A : Finset G) (B : Finset G) :
                                          A.card * A.addConst B = (A + B).card
                                          @[simp]
                                          theorem Finset.card_mul_mulConst {G : Type u_1} [Group G] [DecidableEq G] (A : Finset G) (B : Finset G) :
                                          A.card * A.mulConst B = (A * B).card
                                          @[simp]
                                          theorem Finset.card_mul_subConst {G : Type u_1} [AddGroup G] [DecidableEq G] (A : Finset G) (B : Finset G) :
                                          A.card * A.subConst B = (A - B).card
                                          @[simp]
                                          theorem Finset.card_mul_divConst {G : Type u_1} [Group G] [DecidableEq G] (A : Finset G) (B : Finset G) :
                                          A.card * A.divConst B = (A / B).card
                                          @[simp]
                                          theorem Finset.addConst_empty_left {G : Type u_1} [AddGroup G] [DecidableEq G] (B : Finset G) :
                                          .addConst B = 0
                                          @[simp]
                                          theorem Finset.mulConst_empty_left {G : Type u_1} [Group G] [DecidableEq G] (B : Finset G) :
                                          .mulConst B = 0
                                          @[simp]
                                          theorem Finset.subConst_empty_left {G : Type u_1} [AddGroup G] [DecidableEq G] (B : Finset G) :
                                          .subConst B = 0
                                          @[simp]
                                          theorem Finset.divConst_empty_left {G : Type u_1} [Group G] [DecidableEq G] (B : Finset G) :
                                          .divConst B = 0
                                          @[simp]
                                          theorem Finset.addConst_empty_right {G : Type u_1} [AddGroup G] [DecidableEq G] (A : Finset G) :
                                          A.addConst = 0
                                          @[simp]
                                          theorem Finset.mulConst_empty_right {G : Type u_1} [Group G] [DecidableEq G] (A : Finset G) :
                                          A.mulConst = 0
                                          @[simp]
                                          theorem Finset.subConst_empty_right {G : Type u_1} [AddGroup G] [DecidableEq G] (A : Finset G) :
                                          A.subConst = 0
                                          @[simp]
                                          theorem Finset.divConst_empty_right {G : Type u_1} [Group G] [DecidableEq G] (A : Finset G) :
                                          A.divConst = 0
                                          @[simp]
                                          theorem Finset.addConst_neg_right {G : Type u_1} [AddGroup G] [DecidableEq G] (A : Finset G) (B : Finset G) :
                                          A.addConst (-B) = A.subConst B
                                          @[simp]
                                          theorem Finset.mulConst_inv_right {G : Type u_1} [Group G] [DecidableEq G] (A : Finset G) (B : Finset G) :
                                          A.mulConst B⁻¹ = A.divConst B
                                          @[simp]
                                          theorem Finset.subConst_neg_right {G : Type u_1} [AddGroup G] [DecidableEq G] (A : Finset G) (B : Finset G) :
                                          A.subConst (-B) = A.addConst B
                                          @[simp]
                                          theorem Finset.divConst_inv_right {G : Type u_1} [Group G] [DecidableEq G] (A : Finset G) (B : Finset G) :
                                          A.divConst B⁻¹ = A.mulConst B
                                          theorem Finset.addConst_le_inv_dens {G : Type u_1} [AddGroup G] [DecidableEq G] {A : Finset G} {B : Finset G} [Fintype G] :
                                          A.addConst B A.dens⁻¹

                                          Dense sets have small doubling.

                                          theorem Finset.mulConst_le_inv_dens {G : Type u_1} [Group G] [DecidableEq G] {A : Finset G} {B : Finset G} [Fintype G] :
                                          A.mulConst B A.dens⁻¹

                                          Dense sets have small doubling.

                                          theorem Finset.subConst_le_inv_dens {G : Type u_1} [AddGroup G] [DecidableEq G] {A : Finset G} {B : Finset G} [Fintype G] :
                                          A.subConst B A.dens⁻¹

                                          Dense sets have small difference constant.

                                          theorem Finset.divConst_le_inv_dens {G : Type u_1} [Group G] [DecidableEq G] {A : Finset G} {B : Finset G} [Fintype G] :
                                          A.divConst B A.dens⁻¹

                                          Dense sets have small difference constant.

                                          theorem Finset.cast_addConst {G' : Type u_2} [AddGroup G'] [DecidableEq G'] {𝕜 : Type u_3} [Semifield 𝕜] [CharZero 𝕜] (A : Finset G') (B : Finset G') :
                                          (A.addConst B) = (A + B).card / A.card
                                          theorem Finset.cast_subConst {G' : Type u_2} [AddGroup G'] [DecidableEq G'] {𝕜 : Type u_3} [Semifield 𝕜] [CharZero 𝕜] (A : Finset G') (B : Finset G') :
                                          (A.subConst B) = (A - B).card / A.card
                                          theorem Finset.cast_mulConst {G : Type u_1} [Group G] [DecidableEq G] {𝕜 : Type u_3} [Semifield 𝕜] [CharZero 𝕜] (A : Finset G) (B : Finset G) :
                                          (A.mulConst B) = (A * B).card / A.card
                                          theorem Finset.cast_divConst {G : Type u_1} [Group G] [DecidableEq G] {𝕜 : Type u_3} [Semifield 𝕜] [CharZero 𝕜] (A : Finset G) (B : Finset G) :
                                          (A.divConst B) = (A / B).card / A.card
                                          @[simp]
                                          theorem Finset.cast_addConst_mul_card {G' : Type u_2} [AddGroup G'] [DecidableEq G'] {𝕜 : Type u_3} [Semifield 𝕜] [CharZero 𝕜] (A : Finset G') (B : Finset G') :
                                          (A.addConst B) * A.card = (A + B).card
                                          @[simp]
                                          theorem Finset.cast_subConst_mul_card {G' : Type u_2} [AddGroup G'] [DecidableEq G'] {𝕜 : Type u_3} [Semifield 𝕜] [CharZero 𝕜] (A : Finset G') (B : Finset G') :
                                          (A.subConst B) * A.card = (A - B).card
                                          @[simp]
                                          theorem Finset.card_mul_cast_addConst {G' : Type u_2} [AddGroup G'] [DecidableEq G'] {𝕜 : Type u_3} [Semifield 𝕜] [CharZero 𝕜] (A : Finset G') (B : Finset G') :
                                          A.card * (A.addConst B) = (A + B).card
                                          @[simp]
                                          theorem Finset.card_mul_cast_subConst {G' : Type u_2} [AddGroup G'] [DecidableEq G'] {𝕜 : Type u_3} [Semifield 𝕜] [CharZero 𝕜] (A : Finset G') (B : Finset G') :
                                          A.card * (A.subConst B) = (A - B).card
                                          @[simp]
                                          theorem Finset.cast_mulConst_mul_card {G : Type u_1} [Group G] [DecidableEq G] {𝕜 : Type u_3} [Semifield 𝕜] [CharZero 𝕜] (A : Finset G) (B : Finset G) :
                                          (A.mulConst B) * A.card = (A * B).card
                                          @[simp]
                                          theorem Finset.cast_divConst_mul_card {G : Type u_1} [Group G] [DecidableEq G] {𝕜 : Type u_3} [Semifield 𝕜] [CharZero 𝕜] (A : Finset G) (B : Finset G) :
                                          (A.divConst B) * A.card = (A / B).card
                                          @[simp]
                                          theorem Finset.card_mul_cast_mulConst {G : Type u_1} [Group G] [DecidableEq G] {𝕜 : Type u_3} [Semifield 𝕜] [CharZero 𝕜] (A : Finset G) (B : Finset G) :
                                          A.card * (A.mulConst B) = (A * B).card
                                          @[simp]
                                          theorem Finset.card_mul_cast_divConst {G : Type u_1} [Group G] [DecidableEq G] {𝕜 : Type u_3} [Semifield 𝕜] [CharZero 𝕜] (A : Finset G) (B : Finset G) :
                                          A.card * (A.divConst B) = (A / B).card
                                          @[simp]
                                          theorem Finset.addConst_neg_left {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (B : Finset G) :
                                          (-A).addConst B = A.subConst B
                                          @[simp]
                                          theorem Finset.mulConst_inv_left {G : Type u_1} [CommGroup G] [DecidableEq G] (A : Finset G) (B : Finset G) :
                                          A⁻¹.mulConst B = A.divConst B
                                          @[simp]
                                          theorem Finset.subConst_neg_left {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (B : Finset G) :
                                          (-A).subConst B = A.addConst B
                                          @[simp]
                                          theorem Finset.divConst_inv_left {G : Type u_1} [CommGroup G] [DecidableEq G] (A : Finset G) (B : Finset G) :
                                          A⁻¹.divConst B = A.mulConst B
                                          theorem Finset.addConst_le_subConst_sq {G : Type u_1} [AddCommGroup G] [DecidableEq G] {A : Finset G} :
                                          A.addConst A A.subConst A ^ 2

                                          If A has small difference, then it has small doubling, with the constant squared.

                                          This is a consequence of the Ruzsa triangle inequality.

                                          theorem Finset.mulConst_le_divConst_sq {G : Type u_1} [CommGroup G] [DecidableEq G] {A : Finset G} :
                                          A.mulConst A A.divConst A ^ 2

                                          If A has small difference, then it has small doubling, with the constant squared.

                                          This is a consequence of the Ruzsa triangle inequality.

                                          theorem Finset.subConst_le_addConst_sq {G : Type u_1} [AddCommGroup G] [DecidableEq G] {A : Finset G} :
                                          A.subConst A A.addConst A ^ 2

                                          If A has small doubling, then it has small difference, with the constant squared.

                                          This is a consequence of the Ruzsa triangle inequality.

                                          theorem Finset.divConst_le_mulConst_sq {G : Type u_1} [CommGroup G] [DecidableEq G] {A : Finset G} :
                                          A.divConst A A.mulConst A ^ 2

                                          If A has small doubling, then it has small difference, with the constant squared.

                                          This is a consequence of the Ruzsa triangle inequality.