Triangles in graphs

A triangle in a simple graph is a 3-clique, namely a set of three vertices that are pairwise adjacent.

This module defines and proves properties about triangles in simple graphs.

Main declarations

• SimpleGraph.FarFromTriangleFree: Predicate for a graph such that one must remove a lot of edges from it for it to become triangle-free. This is the crux of the Triangle Removal Lemma.

TODO

• Generalise FarFromTriangleFree to other graphs, to state and prove the Graph Removal Lemma.

def SimpleGraph.EdgeDisjointTriangles {α : Type u_1} (G : SimpleGraph α) : Prop

A graph has edge-disjoint triangles if each edge belongs to at most one triangle.

Equations

• G.EdgeDisjointTriangles = (G.cliqueSet 3).Pairwise fun (x y : Finset α) => (↑x ∩ ↑y).Subsingleton

def SimpleGraph.LocallyLinear {α : Type u_1} (G : SimpleGraph α) : Prop

A graph is locally linear if each edge belongs to exactly one triangle.

Equations

• G.LocallyLinear = (G.EdgeDisjointTriangles ∧ ∀ ⦃x y : α⦄, G.Adj x y → ∃ (s : Finset α), G.IsNClique 3 s ∧ x ∈ s ∧ y ∈ s)

theorem SimpleGraph.LocallyLinear.edgeDisjointTriangles {α : Type u_1} {G : SimpleGraph α} : G.LocallyLinear → G.EdgeDisjointTriangles

theorem SimpleGraph.EdgeDisjointTriangles.mono {α : Type u_1} {G : SimpleGraph α} {H : SimpleGraph α} (h : G ≤ H) (hH : H.EdgeDisjointTriangles) : G.EdgeDisjointTriangles

@[simp]

theorem SimpleGraph.edgeDisjointTriangles_bot {α : Type u_1} : ⊥.EdgeDisjointTriangles

@[simp]

theorem SimpleGraph.locallyLinear_bot {α : Type u_1} : ⊥.LocallyLinear

theorem SimpleGraph.EdgeDisjointTriangles.map {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} (f : α ↪ β) (hG : G.EdgeDisjointTriangles) : (SimpleGraph.map f G).EdgeDisjointTriangles

theorem SimpleGraph.LocallyLinear.map {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} (f : α ↪ β) (hG : G.LocallyLinear) : (SimpleGraph.map f G).LocallyLinear

@[simp]

theorem SimpleGraph.locallyLinear_comap {α : Type u_1} {β : Type u_2} {G : SimpleGraph β} {e : α ≃ β} : (SimpleGraph.comap (⇑e) G).LocallyLinear ↔ G.LocallyLinear

theorem SimpleGraph.edgeDisjointTriangles_iff_mem_sym2_subsingleton {α : Type u_1} {G : SimpleGraph α} [DecidableEq α] : G.EdgeDisjointTriangles ↔ ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → {s : Finset α | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}.Subsingleton

theorem SimpleGraph.EdgeDisjointTriangles.mem_sym2_subsingleton {α : Type u_1} {G : SimpleGraph α} [DecidableEq α] : G.EdgeDisjointTriangles → ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → {s : Finset α | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}.Subsingleton

Alias of the forward direction of SimpleGraph.edgeDisjointTriangles_iff_mem_sym2_subsingleton.

instance SimpleGraph.EdgeDisjointTriangles.instDecidable {α : Type u_1} {G : SimpleGraph α} [DecidableEq α] [Fintype α] [DecidableRel G.Adj] : Decidable G.EdgeDisjointTriangles

Equations

• SimpleGraph.EdgeDisjointTriangles.instDecidable = decidable_of_iff ((↑(G.cliqueFinset 3)).Pairwise fun (x y : Finset α) => (x ∩ y).card ≤ 1) ⋯

instance SimpleGraph.LocallyLinear.instDecidable {α : Type u_1} {G : SimpleGraph α} [DecidableEq α] [Fintype α] [DecidableRel G.Adj] : Decidable G.LocallyLinear

Equations

• SimpleGraph.LocallyLinear.instDecidable = And.decidable

theorem SimpleGraph.EdgeDisjointTriangles.card_edgeFinset_le {α : Type u_1} {G : SimpleGraph α} [DecidableEq α] [Fintype α] [DecidableRel G.Adj] (hG : G.EdgeDisjointTriangles) : 3 * (G.cliqueFinset 3).card ≤ G.edgeFinset.card

theorem SimpleGraph.LocallyLinear.card_edgeFinset {α : Type u_1} {G : SimpleGraph α} [DecidableEq α] [Fintype α] [DecidableRel G.Adj] (hG : G.LocallyLinear) : G.edgeFinset.card = 3 * (G.cliqueFinset 3).card

def SimpleGraph.FarFromTriangleFree {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] (G : SimpleGraph α) (ε : 𝕜) [Fintype α] [DecidableRel G.Adj] : Prop

A simple graph is ε-far from triangle-free if one must remove at least ε * (card α) ^ 2 edges to make it triangle-free.

Equations

• G.FarFromTriangleFree ε = G.DeleteFar (fun (H : SimpleGraph α) => H.CliqueFree 3) (ε * ↑(Fintype.card α ^ 2))

theorem SimpleGraph.farFromTriangleFree_iff {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableRel G.Adj] : G.FarFromTriangleFree ε ↔ ∀ ⦃H : SimpleGraph α⦄ [inst : DecidableRel H.Adj], H ≤ G → H.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑G.edgeFinset.card - ↑H.edgeFinset.card

theorem SimpleGraph.farFromTriangleFree.le_card_sub_card {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableRel G.Adj] : G.FarFromTriangleFree ε → ∀ ⦃H : SimpleGraph α⦄ [inst : DecidableRel H.Adj], H ≤ G → H.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑G.edgeFinset.card - ↑H.edgeFinset.card

Alias of the forward direction of SimpleGraph.farFromTriangleFree_iff.

theorem SimpleGraph.FarFromTriangleFree.mono {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} {δ : 𝕜} [Fintype α] [DecidableRel G.Adj] (hε : G.FarFromTriangleFree ε) (h : δ ≤ ε) : G.FarFromTriangleFree δ

theorem SimpleGraph.FarFromTriangleFree.cliqueFinset_nonempty' {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {H : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableEq α] [DecidableRel G.Adj] [DecidableRel H.Adj] (hH : H ≤ G) (hG : G.FarFromTriangleFree ε) (hcard : ↑G.edgeFinset.card - ↑H.edgeFinset.card < ε * ↑(Fintype.card α ^ 2)) : (H.cliqueFinset 3).Nonempty

theorem SimpleGraph.farFromTriangleFree_of_disjoint_triangles {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (tris : Finset (Finset α)) (htris : tris ⊆ G.cliqueFinset 3) (pd : (↑tris).Pairwise fun (x y : Finset α) => (↑x ∩ ↑y).Subsingleton) (tris_big : ε * ↑(Fintype.card α ^ 2) ≤ ↑tris.card) : G.FarFromTriangleFree ε

If there are ε * (card α)^2 disjoint triangles, then the graph is ε-far from being triangle-free.

theorem SimpleGraph.EdgeDisjointTriangles.farFromTriangleFree {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (hG : G.EdgeDisjointTriangles) (tris_big : ε * ↑(Fintype.card α ^ 2) ≤ ↑(G.cliqueFinset 3).card) : G.FarFromTriangleFree ε

theorem SimpleGraph.FarFromTriangleFree.lt_half {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableEq α] [DecidableRel G.Adj] [Nonempty α] (hG : G.FarFromTriangleFree ε) : ε < 2⁻¹

theorem SimpleGraph.FarFromTriangleFree.lt_one {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableEq α] [DecidableRel G.Adj] [Nonempty α] (hG : G.FarFromTriangleFree ε) : ε < 1

theorem SimpleGraph.FarFromTriangleFree.nonpos {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableRel G.Adj] [Nonempty α] (h₀ : G.FarFromTriangleFree ε) (h₁ : G.CliqueFree 3) : ε ≤ 0

theorem SimpleGraph.CliqueFree.not_farFromTriangleFree {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableRel G.Adj] [Nonempty α] (hG : G.CliqueFree 3) (hε : 0 < ε) : ¬G.FarFromTriangleFree ε

theorem SimpleGraph.FarFromTriangleFree.not_cliqueFree {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableRel G.Adj] [Nonempty α] (hG : G.FarFromTriangleFree ε) (hε : 0 < ε) : ¬G.CliqueFree 3

theorem SimpleGraph.FarFromTriangleFree.cliqueFinset_nonempty {α : Type u_1} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {G : SimpleGraph α} {ε : 𝕜} [Fintype α] [DecidableEq α] [DecidableRel G.Adj] [Nonempty α] (hG : G.FarFromTriangleFree ε) (hε : 0 < ε) : (G.cliqueFinset 3).Nonempty