Relation of covering by cosets

This file defines a predicate for a set to be covered by at most K cosets of another set.

This is a fundamental relation to study in additive combinatorics.

def CovBySMul (M : Type u_1) {X : Type u_3} [Monoid M] [MulAction M X] (K : ℝ) (A B : Set X) : Prop

Predicate for a set A to be covered by at most K cosets of another set B under the action by the monoid M.

Equations

• CovBySMul M K A B = ∃ (F : Finset M), ↑F.card ≤ K ∧ A ⊆ ↑F • B

def CovByVAdd (M : Type u_1) {X : Type u_3} [AddMonoid M] [AddAction M X] (K : ℝ) (A B : Set X) : Prop

Predicate for a set A to be covered by at most K cosets of another set B under the action by the monoid M.

Equations

• CovByVAdd M K A B = ∃ (F : Finset M), ↑F.card ≤ K ∧ A ⊆ ↑F +ᵥ B

@[simp]

theorem CovBySMul.rfl {M : Type u_1} {X : Type u_3} [Monoid M] [MulAction M X] {A : Set X} : CovBySMul M 1 A A

@[simp]

theorem CovByVAdd.rfl {M : Type u_1} {X : Type u_3} [AddMonoid M] [AddAction M X] {A : Set X} : CovByVAdd M 1 A A

@[simp]

theorem CovBySMul.of_subset {M : Type u_1} {X : Type u_3} [Monoid M] [MulAction M X] {A B : Set X} (hAB : A ⊆ B) : CovBySMul M 1 A B

@[simp]

theorem CovByVAdd.of_subset {M : Type u_1} {X : Type u_3} [AddMonoid M] [AddAction M X] {A B : Set X} (hAB : A ⊆ B) : CovByVAdd M 1 A B

theorem CovBySMul.nonneg {M : Type u_1} {X : Type u_3} [Monoid M] [MulAction M X] {K : ℝ} {A B : Set X} : CovBySMul M K A B → 0 ≤ K

theorem CovByVAdd.nonneg {M : Type u_1} {X : Type u_3} [AddMonoid M] [AddAction M X] {K : ℝ} {A B : Set X} : CovByVAdd M K A B → 0 ≤ K

@[simp]

theorem covBySMul_zero {M : Type u_1} {X : Type u_3} [Monoid M] [MulAction M X] {A B : Set X} : CovBySMul M 0 A B ↔ A = ∅

@[simp]

theorem covByVAdd_zero {M : Type u_1} {X : Type u_3} [AddMonoid M] [AddAction M X] {A B : Set X} : CovByVAdd M 0 A B ↔ A = ∅

theorem CovBySMul.mono {M : Type u_1} {X : Type u_3} [Monoid M] [MulAction M X] {K L : ℝ} {A B : Set X} (hKL : K ≤ L) : CovBySMul M K A B → CovBySMul M L A B

theorem CovByVAdd.mono {M : Type u_1} {X : Type u_3} [AddMonoid M] [AddAction M X] {K L : ℝ} {A B : Set X} (hKL : K ≤ L) : CovByVAdd M K A B → CovByVAdd M L A B

theorem CovBySMul.trans {M : Type u_1} {N : Type u_2} {X : Type u_3} [Monoid M] [Monoid N] [MulAction M X] [MulAction N X] {K L : ℝ} {A B C : Set X} [SMul M N] [IsScalarTower M N X] (hAB : CovBySMul M K A B) (hBC : CovBySMul N L B C) : CovBySMul N (K * L) A C

theorem CovByVAdd.trans {M : Type u_1} {N : Type u_2} {X : Type u_3} [AddMonoid M] [AddMonoid N] [AddAction M X] [AddAction N X] {K L : ℝ} {A B C : Set X} [VAdd M N] [VAddAssocClass M N X] (hAB : CovByVAdd M K A B) (hBC : CovByVAdd N L B C) : CovByVAdd N (K * L) A C

theorem CovBySMul.subset_left {M : Type u_1} {X : Type u_3} [Monoid M] [MulAction M X] {K : ℝ} {A₁ A₂ B : Set X} (hA : A₁ ⊆ A₂) (hAB : CovBySMul M K A₂ B) : CovBySMul M K A₁ B

theorem CovByVAdd.subset_left {M : Type u_1} {X : Type u_3} [AddMonoid M] [AddAction M X] {K : ℝ} {A₁ A₂ B : Set X} (hA : A₁ ⊆ A₂) (hAB : CovByVAdd M K A₂ B) : CovByVAdd M K A₁ B

theorem CovBySMul.subset_right {M : Type u_1} {X : Type u_3} [Monoid M] [MulAction M X] {K : ℝ} {A B₁ B₂ : Set X} (hB : B₁ ⊆ B₂) (hAB : CovBySMul M K A B₁) : CovBySMul M K A B₂

theorem CovByVAdd.subset_right {M : Type u_1} {X : Type u_3} [AddMonoid M] [AddAction M X] {K : ℝ} {A B₁ B₂ : Set X} (hB : B₁ ⊆ B₂) (hAB : CovByVAdd M K A B₁) : CovByVAdd M K A B₂

theorem CovBySMul.subset {M : Type u_1} {X : Type u_3} [Monoid M] [MulAction M X] {K : ℝ} {A₁ A₂ B₁ B₂ : Set X} (hA : A₁ ⊆ A₂) (hB : B₁ ⊆ B₂) (hAB : CovBySMul M K A₂ B₁) : CovBySMul M K A₁ B₂

theorem CovByVAdd.subset {M : Type u_1} {X : Type u_3} [AddMonoid M] [AddAction M X] {K : ℝ} {A₁ A₂ B₁ B₂ : Set X} (hA : A₁ ⊆ A₂) (hB : B₁ ⊆ B₂) (hAB : CovByVAdd M K A₂ B₁) : CovByVAdd M K A₁ B₂