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
farFromTriangleFreeto other graphs, to state and prove the Graph Removal Lemma.
def
SimpleGraph.FarFromTriangleFree
{α : Type u_1}
{𝕜 : Type u_2}
[Fintype α]
[LinearOrderedRing 𝕜]
(G : SimpleGraph α)
(ε : 𝕜)
:
A simple graph is ε-far from triangle-free if one must remove at least
ε * (card α) ^ 2 edges to make it triangle-free.
Equations
- SimpleGraph.FarFromTriangleFree G ε = SimpleGraph.DeleteFar G (fun (H : SimpleGraph α) => SimpleGraph.CliqueFree H 3) (ε * ↑(Fintype.card α ^ 2))
Instances For
theorem
SimpleGraph.farFromTriangleFree_iff
{α : Type u_1}
{𝕜 : Type u_2}
[Fintype α]
[LinearOrderedRing 𝕜]
{G : SimpleGraph α}
{ε : 𝕜}
:
SimpleGraph.FarFromTriangleFree G ε ↔ ∀ ⦃H : SimpleGraph α⦄ [inst : DecidableRel H.Adj],
H ≤ G →
SimpleGraph.CliqueFree H 3 →
ε * ↑(Fintype.card α ^ 2) ≤ ↑(SimpleGraph.edgeFinset G).card - ↑(SimpleGraph.edgeFinset H).card
theorem
SimpleGraph.farFromTriangleFree.le_card_sub_card
{α : Type u_1}
{𝕜 : Type u_2}
[Fintype α]
[LinearOrderedRing 𝕜]
{G : SimpleGraph α}
{ε : 𝕜}
:
SimpleGraph.FarFromTriangleFree G ε →
∀ ⦃H : SimpleGraph α⦄ [inst : DecidableRel H.Adj],
H ≤ G →
SimpleGraph.CliqueFree H 3 →
ε * ↑(Fintype.card α ^ 2) ≤ ↑(SimpleGraph.edgeFinset G).card - ↑(SimpleGraph.edgeFinset H).card
Alias of the forward direction of SimpleGraph.farFromTriangleFree_iff.
theorem
SimpleGraph.FarFromTriangleFree.mono
{α : Type u_1}
{𝕜 : Type u_2}
[Fintype α]
[LinearOrderedRing 𝕜]
{G : SimpleGraph α}
{ε : 𝕜}
{δ : 𝕜}
(hε : SimpleGraph.FarFromTriangleFree G ε)
(h : δ ≤ ε)
:
theorem
SimpleGraph.FarFromTriangleFree.cliqueFinset_nonempty'
{α : Type u_1}
{𝕜 : Type u_2}
[Fintype α]
[LinearOrderedRing 𝕜]
{G : SimpleGraph α}
{H : SimpleGraph α}
{ε : 𝕜}
(hH : H ≤ G)
(hG : SimpleGraph.FarFromTriangleFree G ε)
(hcard : ↑(SimpleGraph.edgeFinset G).card - ↑(SimpleGraph.edgeFinset H).card < ε * ↑(Fintype.card α ^ 2))
:
(SimpleGraph.cliqueFinset H 3).Nonempty
theorem
SimpleGraph.FarFromTriangleFree.nonpos
{α : Type u_1}
{𝕜 : Type u_2}
[Fintype α]
[LinearOrderedRing 𝕜]
{G : SimpleGraph α}
{ε : 𝕜}
[Nonempty α]
(h₀ : SimpleGraph.FarFromTriangleFree G ε)
(h₁ : SimpleGraph.CliqueFree G 3)
:
ε ≤ 0
theorem
SimpleGraph.CliqueFree.not_farFromTriangleFree
{α : Type u_1}
{𝕜 : Type u_2}
[Fintype α]
[LinearOrderedRing 𝕜]
{G : SimpleGraph α}
{ε : 𝕜}
[Nonempty α]
(hG : SimpleGraph.CliqueFree G 3)
(hε : 0 < ε)
:
theorem
SimpleGraph.FarFromTriangleFree.not_cliqueFree
{α : Type u_1}
{𝕜 : Type u_2}
[Fintype α]
[LinearOrderedRing 𝕜]
{G : SimpleGraph α}
{ε : 𝕜}
[Nonempty α]
(hG : SimpleGraph.FarFromTriangleFree G ε)
(hε : 0 < ε)
:
theorem
SimpleGraph.FarFromTriangleFree.cliqueFinset_nonempty
{α : Type u_1}
{𝕜 : Type u_2}
[Fintype α]
[LinearOrderedRing 𝕜]
{G : SimpleGraph α}
{ε : 𝕜}
[Nonempty α]
(hG : SimpleGraph.FarFromTriangleFree G ε)
(hε : 0 < ε)
:
(SimpleGraph.cliqueFinset G 3).Nonempty