Doubling and difference constants

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

def Finset.mulConst {G : Type u_1} [Group G] [DecidableEq G] (A B : Finset G) : ℚ≥0

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.

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

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.

def Finset.divConst {G : Type u_1} [Group G] [DecidableEq G] (A B : Finset G) : ℚ≥0

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.

def Finset.subConst {G : Type u_1} [AddGroup G] [DecidableEq G] (A B : Finset G) : ℚ≥0

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.

def Combinatorics.Additive.«termσₘ[_,_]».«delab_app.Finset.mulConst» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

def Combinatorics.Additive.«termσₘ[_,_]» : Lean.ParserDescr

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

def Combinatorics.Additive.«termσₘ[_]» : Lean.ParserDescr

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

def Combinatorics.Additive.«termσₘ[_]».«delab_app.Finset.mulConst» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

def Combinatorics.Additive.«termσ[_,_]».«delab_app.Finset.addConst» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

def Combinatorics.Additive.«termσ[_,_]» : Lean.ParserDescr

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

def Combinatorics.Additive.«termσ[_]».«delab_app.Finset.addConst» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

def Combinatorics.Additive.«termσ[_]» : Lean.ParserDescr

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

def Combinatorics.Additive.«termδₘ[_,_]».«delab_app.Finset.divConst» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

def Combinatorics.Additive.«termδₘ[_,_]» : Lean.ParserDescr

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

def Combinatorics.Additive.«termδₘ[_]».«delab_app.Finset.divConst» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

def Combinatorics.Additive.«termδₘ[_]» : Lean.ParserDescr

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

def Combinatorics.Additive.«termδ[_,_]» : Lean.ParserDescr

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

def Combinatorics.Additive.«termδ[_,_]».«delab_app.Finset.subConst» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

def Combinatorics.Additive.«termδ[_]».«delab_app.Finset.subConst» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

def Combinatorics.Additive.«termδ[_]» : Lean.ParserDescr

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

@[simp]

theorem Finset.mulConst_mul_card {G : Type u_1} [Group G] [DecidableEq G] (A B : Finset G) : A.mulConst B * ↑A.card = ↑(A * B).card

@[simp]

theorem Finset.addConst_mul_card {G : Type u_1} [AddGroup G] [DecidableEq G] (A B : Finset G) : A.addConst B * ↑A.card = ↑(A + B).card

@[simp]

theorem Finset.divConst_mul_card {G : Type u_1} [Group G] [DecidableEq G] (A B : Finset G) : A.divConst B * ↑A.card = ↑(A / B).card

@[simp]

theorem Finset.subConst_mul_card {G : Type u_1} [AddGroup G] [DecidableEq G] (A B : Finset G) : A.subConst B * ↑A.card = ↑(A - B).card

@[simp]

theorem Finset.card_mul_mulConst {G : Type u_1} [Group G] [DecidableEq G] (A B : Finset G) : ↑A.card * A.mulConst B = ↑(A * B).card

@[simp]

theorem Finset.card_mul_addConst {G : Type u_1} [AddGroup G] [DecidableEq G] (A B : Finset G) : ↑A.card * A.addConst B = ↑(A + B).card

@[simp]

theorem Finset.card_mul_divConst {G : Type u_1} [Group G] [DecidableEq G] (A B : Finset G) : ↑A.card * A.divConst B = ↑(A / B).card

@[simp]

theorem Finset.card_mul_subConst {G : Type u_1} [AddGroup G] [DecidableEq G] (A B : Finset G) : ↑A.card * A.subConst B = ↑(A - B).card

@[simp]

theorem Finset.mulConst_empty_left {G : Type u_1} [Group G] [DecidableEq G] (B : Finset G) : ∅.mulConst B = 0

@[simp]

theorem Finset.addConst_empty_left {G : Type u_1} [AddGroup G] [DecidableEq G] (B : Finset G) : ∅.addConst 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.subConst_empty_left {G : Type u_1} [AddGroup G] [DecidableEq G] (B : Finset G) : ∅.subConst B = 0

@[simp]

theorem Finset.mulConst_empty_right {G : Type u_1} [Group G] [DecidableEq G] (A : Finset G) : A.mulConst ∅ = 0

@[simp]

theorem Finset.addConst_empty_right {G : Type u_1} [AddGroup G] [DecidableEq G] (A : Finset G) : A.addConst ∅ = 0

@[simp]

theorem Finset.divConst_empty_right {G : Type u_1} [Group G] [DecidableEq G] (A : Finset G) : A.divConst ∅ = 0

@[simp]

theorem Finset.subConst_empty_right {G : Type u_1} [AddGroup G] [DecidableEq G] (A : Finset G) : A.subConst ∅ = 0

@[simp]

theorem Finset.mulConst_inv_right {G : Type u_1} [Group G] [DecidableEq G] (A B : Finset G) : A.mulConst B⁻¹ = A.divConst B

@[simp]

theorem Finset.addConst_neg_right {G : Type u_1} [AddGroup G] [DecidableEq G] (A B : Finset G) : A.addConst (-B) = A.subConst B

@[simp]

theorem Finset.divConst_inv_right {G : Type u_1} [Group G] [DecidableEq G] (A B : Finset G) : A.divConst B⁻¹ = A.mulConst B

@[simp]

theorem Finset.subConst_neg_right {G : Type u_1} [AddGroup G] [DecidableEq G] (A B : Finset G) : A.subConst (-B) = A.addConst B

theorem Finset.one_le_mulConst {G : Type u_1} [Group G] [DecidableEq G] {A B : Finset G} (hA : A.Nonempty) (hB : B.Nonempty) : 1 ≤ A.mulConst B

theorem Finset.nonneg_addConst {G : Type u_1} [AddGroup G] [DecidableEq G] {A B : Finset G} (hA : A.Nonempty) (hB : B.Nonempty) : 1 ≤ A.addConst B

theorem Finset.one_le_mulConst_self {G : Type u_1} [Group G] [DecidableEq G] {A : Finset G} (hA : A.Nonempty) : 1 ≤ A.mulConst A

theorem Finset.nonneg_addConst_self {G : Type u_1} [AddGroup G] [DecidableEq G] {A : Finset G} (hA : A.Nonempty) : 1 ≤ A.addConst A

theorem Finset.one_le_divConst {G : Type u_1} [Group G] [DecidableEq G] {A B : Finset G} (hA : A.Nonempty) (hB : B.Nonempty) : 1 ≤ A.divConst B

theorem Finset.nonneg_subConst {G : Type u_1} [AddGroup G] [DecidableEq G] {A B : Finset G} (hA : A.Nonempty) (hB : B.Nonempty) : 1 ≤ A.subConst B

theorem Finset.one_le_divConst_self {G : Type u_1} [Group G] [DecidableEq G] {A : Finset G} (hA : A.Nonempty) : 1 ≤ A.divConst A

theorem Finset.nonneg_subConst_self {G : Type u_1} [AddGroup G] [DecidableEq G] {A : Finset G} (hA : A.Nonempty) : 1 ≤ A.subConst A

theorem Finset.mulConst_le_card {G : Type u_1} [Group G] [DecidableEq G] {A B : Finset G} : A.mulConst B ≤ ↑B.card

theorem Finset.addConst_le_card {G : Type u_1} [AddGroup G] [DecidableEq G] {A B : Finset G} : A.addConst B ≤ ↑B.card

theorem Finset.divConst_le_card {G : Type u_1} [Group G] [DecidableEq G] {A B : Finset G} : A.divConst B ≤ ↑B.card

theorem Finset.subConst_le_card {G : Type u_1} [AddGroup G] [DecidableEq G] {A B : Finset G} : A.subConst B ≤ ↑B.card

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

Dense sets have small doubling.

theorem Finset.addConst_le_inv_dens {G : Type u_1} [AddGroup G] [DecidableEq G] {A B : Finset G} [Fintype G] : A.addConst B ≤ A.dens⁻¹

Dense sets have small doubling.

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

Dense sets have small difference constant.

theorem Finset.subConst_le_inv_dens {G : Type u_1} [AddGroup G] [DecidableEq G] {A B : Finset G} [Fintype G] : A.subConst 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 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 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 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 B : Finset G) : ↑(A.divConst B) = ↑(A / B).card / ↑A.card

theorem Finset.cast_addConst_mul_card {G' : Type u_2} [AddGroup G'] [DecidableEq G'] {𝕜 : Type u_3} [Semifield 𝕜] [CharZero 𝕜] (A B : Finset G') : ↑(A.addConst B) * ↑A.card = ↑(A + B).card

theorem Finset.cast_subConst_mul_card {G' : Type u_2} [AddGroup G'] [DecidableEq G'] {𝕜 : Type u_3} [Semifield 𝕜] [CharZero 𝕜] (A B : Finset G') : ↑(A.subConst B) * ↑A.card = ↑(A - B).card

theorem Finset.card_mul_cast_addConst {G' : Type u_2} [AddGroup G'] [DecidableEq G'] {𝕜 : Type u_3} [Semifield 𝕜] [CharZero 𝕜] (A B : Finset G') : ↑A.card * ↑(A.addConst B) = ↑(A + B).card

theorem Finset.card_mul_cast_subConst {G' : Type u_2} [AddGroup G'] [DecidableEq G'] {𝕜 : Type u_3} [Semifield 𝕜] [CharZero 𝕜] (A 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 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 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 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 B : Finset G) : ↑A.card * ↑(A.divConst B) = ↑(A / B).card

theorem Finset.divConst_le_mulConst_sq {G : Type u_1} [Group 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.

theorem Finset.subConst_le_addConst_sq {G : Type u_1} [AddGroup 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.

@[simp]

theorem Finset.mulConst_inv_left {G : Type u_1} [CommGroup G] [DecidableEq G] (A B : Finset G) : A⁻¹.mulConst B = A.divConst B

@[simp]

theorem Finset.addConst_neg_left {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A B : Finset G) : (-A).addConst B = A.subConst B

@[simp]

theorem Finset.divConst_inv_left {G : Type u_1} [CommGroup G] [DecidableEq G] (A B : Finset G) : A⁻¹.divConst B = A.mulConst B

@[simp]

theorem Finset.subConst_neg_left {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A B : Finset G) : (-A).subConst B = A.addConst B

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.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.