Triangles in graphs #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
simple_graph.far_from_triangle_free: Predicate for a graph to have enough triangles that, to remove all of them, one must one must remove a lot of edges. This is the crux of the Triangle Removal lemma.
TODO #
- Generalise
far_from_triangle_freeto other graphs, to state and prove the Graph Removal Lemma. - Find a better name for
far_from_triangle_free. Added 4/26/2022. Remove this TODO if it gets old.
def
simple_graph.far_from_triangle_free
{α : Type u_1}
{𝕜 : Type u_2}
[fintype α]
[linear_ordered_field 𝕜]
(G : simple_graph α)
(ε : 𝕜) :
Prop
A simple graph is ε-triangle-free far if one must remove at least ε * (card α)^2 edges to
make it triangle-free.
Equations
- G.far_from_triangle_free ε = G.delete_far (λ (H : simple_graph α), H.clique_free 3) (ε * ↑(fintype.card α ^ 2))
theorem
simple_graph.far_from_triangle_free_iff
{α : Type u_1}
{𝕜 : Type u_2}
[fintype α]
[linear_ordered_field 𝕜]
{G : simple_graph α}
{ε : 𝕜} :
G.far_from_triangle_free ε ↔ ∀ ⦃H : simple_graph α⦄ [_inst_3 : decidable_rel H.adj], H ≤ G → H.clique_free 3 → ε * ↑(fintype.card α ^ 2) ≤ ↑(G.edge_finset.card) - ↑(H.edge_finset.card)
theorem
simple_graph.far_from_triangle_free.le_card_sub_card
{α : Type u_1}
{𝕜 : Type u_2}
[fintype α]
[linear_ordered_field 𝕜]
{G : simple_graph α}
{ε : 𝕜} :
G.far_from_triangle_free ε → ∀ ⦃H : simple_graph α⦄ [_inst_3 : decidable_rel H.adj], H ≤ G → H.clique_free 3 → ε * ↑(fintype.card α ^ 2) ≤ ↑(G.edge_finset.card) - ↑(H.edge_finset.card)
Alias of the forward direction of simple_graph.far_from_triangle_free_iff.
theorem
simple_graph.far_from_triangle_free.mono
{α : Type u_1}
{𝕜 : Type u_2}
[fintype α]
[linear_ordered_field 𝕜]
{G : simple_graph α}
{ε δ : 𝕜}
(hε : G.far_from_triangle_free ε)
(h : δ ≤ ε) :
theorem
simple_graph.far_from_triangle_free.clique_finset_nonempty'
{α : Type u_1}
{𝕜 : Type u_2}
[fintype α]
[linear_ordered_field 𝕜]
{G H : simple_graph α}
{ε : 𝕜}
(hH : H ≤ G)
(hG : G.far_from_triangle_free ε)
(hcard : ↑(G.edge_finset.card) - ↑(H.edge_finset.card) < ε * ↑(fintype.card α ^ 2)) :
(H.clique_finset 3).nonempty
theorem
simple_graph.far_from_triangle_free.nonpos
{α : Type u_1}
{𝕜 : Type u_2}
[fintype α]
[linear_ordered_field 𝕜]
{G : simple_graph α}
{ε : 𝕜}
[nonempty α]
(h₀ : G.far_from_triangle_free ε)
(h₁ : G.clique_free 3) :
ε ≤ 0
theorem
simple_graph.clique_free.not_far_from_triangle_free
{α : Type u_1}
{𝕜 : Type u_2}
[fintype α]
[linear_ordered_field 𝕜]
{G : simple_graph α}
{ε : 𝕜}
[nonempty α]
(hG : G.clique_free 3)
(hε : 0 < ε) :
theorem
simple_graph.far_from_triangle_free.not_clique_free
{α : Type u_1}
{𝕜 : Type u_2}
[fintype α]
[linear_ordered_field 𝕜]
{G : simple_graph α}
{ε : 𝕜}
[nonempty α]
(hG : G.far_from_triangle_free ε)
(hε : 0 < ε) :
¬G.clique_free 3
theorem
simple_graph.far_from_triangle_free.clique_finset_nonempty
{α : Type u_1}
{𝕜 : Type u_2}
[fintype α]
[linear_ordered_field 𝕜]
{G : simple_graph α}
{ε : 𝕜}
[nonempty α]
(hG : G.far_from_triangle_free ε)
(hε : 0 < ε) :
(G.clique_finset 3).nonempty