Corners

This file defines corners, namely triples of the form (x, y), (x, y + d), (x + d, y), and the property of being corner-free the corners theorem and Roth's theorem.

References

• [Yaël Dillies, Bhavik Mehta, Formalising Szemerédi’s Regularity Lemma in Lean][srl_itp]
• Wikipedia, Corners theorem

theorem isCorner_iff {G : Type u_1} [AddCommMonoid G] (A : Set (G × G)) (x₁ : G) (y₁ : G) (x₂ : G) (y₂ : G) : IsCorner A x₁ y₁ x₂ y₂ ↔ (x₁, y₁) ∈ A ∧ (x₁, y₂) ∈ A ∧ (x₂, y₁) ∈ A ∧ x₁ + y₂ = x₂ + y₁

structure IsCorner {G : Type u_1} [AddCommMonoid G] (A : Set (G × G)) (x₁ : G) (y₁ : G) (x₂ : G) (y₂ : G) : Prop

A corner of a set A in an abelian group is a triple of points of the form (x, y), (x + d, y), (x, y + d). It is nontrivial if d ≠ 0.

Here we define it as triples (x₁, y₁), (x₂, y₁), (x₁, y₂) where x₁ + y₂ = x₂ + y₁ in order for the definition to make sense in commutative monoids, the motivating example being ℕ.

• fst_fst_mem : (x₁, y₁) ∈ A
• fst_snd_mem : (x₁, y₂) ∈ A
• snd_fst_mem : (x₂, y₁) ∈ A
• add_eq_add : x₁ + y₂ = x₂ + y₁

theorem IsCorner.fst_fst_mem {G : Type u_1} [AddCommMonoid G] {A : Set (G × G)} {x₁ : G} {y₁ : G} {x₂ : G} {y₂ : G} (self : IsCorner A x₁ y₁ x₂ y₂) : (x₁, y₁) ∈ A

theorem IsCorner.fst_snd_mem {G : Type u_1} [AddCommMonoid G] {A : Set (G × G)} {x₁ : G} {y₁ : G} {x₂ : G} {y₂ : G} (self : IsCorner A x₁ y₁ x₂ y₂) : (x₁, y₂) ∈ A

theorem IsCorner.snd_fst_mem {G : Type u_1} [AddCommMonoid G] {A : Set (G × G)} {x₁ : G} {y₁ : G} {x₂ : G} {y₂ : G} (self : IsCorner A x₁ y₁ x₂ y₂) : (x₂, y₁) ∈ A

theorem IsCorner.add_eq_add {G : Type u_1} [AddCommMonoid G] {A : Set (G × G)} {x₁ : G} {y₁ : G} {x₂ : G} {y₂ : G} (self : IsCorner A x₁ y₁ x₂ y₂) : x₁ + y₂ = x₂ + y₁

def IsCornerFree {G : Type u_1} [AddCommMonoid G] (A : Set (G × G)) : Prop

A corner-free set in an abelian group is a set containing no non-trivial corner.

Equations

• IsCornerFree A = ∀ ⦃x₁ y₁ x₂ y₂ : G⦄, IsCorner A x₁ y₁ x₂ y₂ → x₁ = x₂

theorem isCornerFree_iff {G : Type u_1} [AddCommMonoid G] {A : Set (G × G)} {s : Set G} (hAs : A ⊆ s ×ˢ s) : IsCornerFree A ↔ ∀ ⦃x₁ : G⦄, x₁ ∈ s → ∀ ⦃y₁ : G⦄, y₁ ∈ s → ∀ ⦃x₂ : G⦄, x₂ ∈ s → ∀ ⦃y₂ : G⦄, y₂ ∈ s → IsCorner A x₁ y₁ x₂ y₂ → x₁ = x₂

A convenient restatement of corner-freeness in terms of an ambient product set.

theorem IsCorner.mono {G : Type u_1} [AddCommMonoid G] {A : Set (G × G)} {B : Set (G × G)} {x₁ : G} {y₁ : G} {x₂ : G} {y₂ : G} (hAB : A ⊆ B) (hA : IsCorner A x₁ y₁ x₂ y₂) : IsCorner B x₁ y₁ x₂ y₂

theorem IsCornerFree.mono {G : Type u_1} [AddCommMonoid G] {A : Set (G × G)} {B : Set (G × G)} (hAB : A ⊆ B) (hB : IsCornerFree B) : IsCornerFree A

@[simp]

theorem not_isCorner_empty {G : Type u_1} [AddCommMonoid G] {x₁ : G} {y₁ : G} {x₂ : G} {y₂ : G} : ¬IsCorner ∅ x₁ y₁ x₂ y₂

@[simp]

theorem Set.Subsingleton.isCornerFree {G : Type u_1} [AddCommMonoid G] {A : Set (G × G)} (hA : A.Subsingleton) : IsCornerFree A

theorem isCornerFree_empty {G : Type u_1} [AddCommMonoid G] : IsCornerFree ∅

theorem isCornerFree_singleton {G : Type u_1} [AddCommMonoid G] (x : G × G) : IsCornerFree {x}

theorem IsCorner.image {G : Type u_1} {H : Type u_2} [AddCommMonoid G] [AddCommMonoid H] {A : Set (G × G)} {s : Set G} {t : Set H} {f : G → H} {x₁ : G} {y₁ : G} {x₂ : G} {y₂ : G} (hf : IsAddFreimanHom 2 s t f) (hAs : A ⊆ s ×ˢ s) (hA : IsCorner A x₁ y₁ x₂ y₂) : IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂)

Corners are preserved under 2-Freiman homomorphisms. -

theorem IsCornerFree.of_image {G : Type u_1} {H : Type u_2} [AddCommMonoid G] [AddCommMonoid H] {A : Set (G × G)} {s : Set G} {t : Set H} {f : G → H} (hf : IsAddFreimanHom 2 s t f) (hf' : Set.InjOn f s) (hAs : A ⊆ s ×ˢ s) (hA : IsCornerFree (Prod.map f f '' A)) : IsCornerFree A

Corners are preserved under 2-Freiman homomorphisms. -

theorem isCorner_image {G : Type u_1} {H : Type u_2} [AddCommMonoid G] [AddCommMonoid H] {A : Set (G × G)} {s : Set G} {t : Set H} {f : G → H} {x₁ : G} {y₁ : G} {x₂ : G} {y₂ : G} (hf : IsAddFreimanIso 2 s t f) (hAs : A ⊆ s ×ˢ s) (hx₁ : x₁ ∈ s) (hy₁ : y₁ ∈ s) (hx₂ : x₂ ∈ s) (hy₂ : y₂ ∈ s) : IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂) ↔ IsCorner A x₁ y₁ x₂ y₂

theorem isCornerFree_image {G : Type u_1} {H : Type u_2} [AddCommMonoid G] [AddCommMonoid H] {A : Set (G × G)} {s : Set G} {t : Set H} {f : G → H} (hf : IsAddFreimanIso 2 s t f) (hAs : A ⊆ s ×ˢ s) : IsCornerFree (Prod.map f f '' A) ↔ IsCornerFree A

theorem IsCorner.of_image {G : Type u_1} {H : Type u_2} [AddCommMonoid G] [AddCommMonoid H] {A : Set (G × G)} {s : Set G} {t : Set H} {f : G → H} {x₁ : G} {y₁ : G} {x₂ : G} {y₂ : G} (hf : IsAddFreimanIso 2 s t f) (hAs : A ⊆ s ×ˢ s) (hx₁ : x₁ ∈ s) (hy₁ : y₁ ∈ s) (hx₂ : x₂ ∈ s) (hy₂ : y₂ ∈ s) : IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂) → IsCorner A x₁ y₁ x₂ y₂

Alias of the forward direction of isCorner_image.

theorem IsCornerFree.image {G : Type u_1} {H : Type u_2} [AddCommMonoid G] [AddCommMonoid H] {A : Set (G × G)} {s : Set G} {t : Set H} {f : G → H} (hf : IsAddFreimanIso 2 s t f) (hAs : A ⊆ s ×ˢ s) : IsCornerFree A → IsCornerFree (Prod.map f f '' A)

Alias of the reverse direction of isCornerFree_image.