Trails and Eulerian trails

This module contains additional theory about trails, including Eulerian trails (also known as Eulerian circuits).

Main definitions

• SimpleGraph.Walk.IsEulerian is the predicate that a trail is an Eulerian trail.
• SimpleGraph.Walk.IsTrail.even_countP_edges_iff gives a condition on the number of edges in a trail that can be incident to a given vertex.
• SimpleGraph.Walk.IsEulerian.even_degree_iff gives a condition on the degrees of vertices when there exists an Eulerian trail.
• SimpleGraph.Walk.IsEulerian.card_odd_degree gives the possible numbers of odd-degree vertices when there exists an Eulerian trail.

TODO

• Prove that there exists an Eulerian trail when the conclusion to SimpleGraph.Walk.IsEulerian.card_odd_degree holds.

Tags

Eulerian trails

@[reducible, inline]

abbrev SimpleGraph.Walk.IsTrail.edgesFinset {V : Type u_1} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : p.IsTrail) : Finset (Sym2 V)

The edges of a trail as a finset, since each edge in a trail appears exactly once.

Equations

• h.edgesFinset = { val := ↑p.edges, nodup := ⋯ }

theorem SimpleGraph.Walk.IsTrail.even_countP_edges_iff {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u v : V} {p : G.Walk u v} (ht : p.IsTrail) (x : V) : Even (List.countP (fun (e : Sym2 V) => decide (x ∈ e)) p.edges) ↔ u ≠ v → x ≠ u ∧ x ≠ v

def SimpleGraph.Walk.IsEulerian {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) : Prop

An Eulerian trail (also known as an "Eulerian path") is a walk p that visits every edge exactly once. The lemma SimpleGraph.Walk.IsEulerian.IsTrail shows that these are trails.

Combine with p.IsCircuit to get an Eulerian circuit (also known as an "Eulerian cycle").

Equations

• p.IsEulerian = ∀ e ∈ G.edgeSet, List.count e p.edges = 1

theorem SimpleGraph.Walk.IsEulerian.isTrail {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u v : V} {p : G.Walk u v} (h : p.IsEulerian) : p.IsTrail

theorem SimpleGraph.Walk.IsEulerian.mem_edges_iff {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u v : V} {p : G.Walk u v} (h : p.IsEulerian) {e : Sym2 V} : e ∈ p.edges ↔ e ∈ G.edgeSet

def SimpleGraph.Walk.IsEulerian.fintypeEdgeSet {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u v : V} {p : G.Walk u v} (h : p.IsEulerian) : Fintype ↑G.edgeSet

The edge set of an Eulerian graph is finite.

Equations

• h.fintypeEdgeSet = Fintype.ofFinset ⋯.edgesFinset ⋯

theorem SimpleGraph.Walk.IsTrail.isEulerian_of_forall_mem {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u v : V} {p : G.Walk u v} (h : p.IsTrail) (hc : ∀ e ∈ G.edgeSet, e ∈ p.edges) : p.IsEulerian

theorem SimpleGraph.Walk.isEulerian_iff {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) : p.IsEulerian ↔ p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges

theorem SimpleGraph.Walk.IsEulerian.edgesFinset_eq {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] [Fintype ↑G.edgeSet] {u v : V} {p : G.Walk u v} (h : p.IsEulerian) : ⋯.edgesFinset = G.edgeFinset

theorem SimpleGraph.Walk.IsEulerian.even_degree_iff {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {x u v : V} {p : G.Walk u v} (ht : p.IsEulerian) [Fintype V] [DecidableRel G.Adj] : Even (G.degree x) ↔ u ≠ v → x ≠ u ∧ x ≠ v

theorem SimpleGraph.Walk.IsEulerian.card_filter_odd_degree {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] [Fintype V] [DecidableRel G.Adj] {u v : V} {p : G.Walk u v} (ht : p.IsEulerian) {s : Finset V} (h : s = Finset.filter (fun (v : V) => Odd (G.degree v)) Finset.univ) : s.card = 0 ∨ s.card = 2

theorem SimpleGraph.Walk.IsEulerian.card_odd_degree {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] [Fintype V] [DecidableRel G.Adj] {u v : V} {p : G.Walk u v} (ht : p.IsEulerian) : Fintype.card ↑{v : V | Odd (G.degree v)} = 0 ∨ Fintype.card ↑{v : V | Odd (G.degree v)} = 2