Graph Theory, example sheet 1

Here are the statements (and hopefully soon proofs!) of the questions from the first example sheet of the Cambridge Part II course Graph Theory.

If you solve a question in Lean, feel free to open a Pull Request on Github!

Question 1

Show that a graph $$G$$ which contains an odd circuit, contains an odd cycle.

theorem GraphTheory.ES1.q1 {α : Type u_2} (G : SimpleGraph α) (a : α) (w : G.Walk a a) (hw : Odd w.length) : ∃ (b : α) (p : G.Path b b), Odd (↑p).length

Question 2

Show there are infinitely many planar graphs for which $$e(G) = 3(|G| − 2)$$. Can you give a nice description of all graphs that satisfy this equality?

Question 3

Show that every graph $$G$$, with $$|G| > 2$$, has two vertices of the same degree.

theorem GraphTheory.ES1.q3 {α : Type u_2} [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] : ∃ (a : α) (b : α), a ≠ b ∧ G.degree a = G.degree b

Question 4

Show that in every connected graph with $$|G| ≥ 2$$ there exists a vertex $$v$$ so that $$G − v$$ is connected.

theorem GraphTheory.ES1.q4 {α : Type u_2} [Finite α] [Nontrivial α] (G : SimpleGraph α) (hG : G.Connected) : ∃ (a : α), (⊤.deleteVerts {a}).coe.Connected

Question 5

Show that if $$G$$ is acyclic and $$|G| ≥ 1$$, then $$e(G) ≤ n − 1$$.

theorem GraphTheory.ES1.q5 {α : Type u_2} [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] (hG : G.IsAcyclic) : G.edgeFinset.card ≤ Fintype.card α - 1

Question 6

The degree sequence of a graph $$G = ({x_1, . . . , x_n}, E)$$ is the sequence $$d(x_1), . . . , d(x_n)$$. For $$n ≥ 2$$, let $$1 ≤ d_1 ≤ d_2 ≤ \dots ≤ d_n$$ be integers. Show that $$(d_i)_{i = 1}^n$$ is a degree sequence of a tree if and only if $$\sum_{i=1}^n d_i = 2n − 2$$.

def GraphTheory.ES1.degreeSequence {α : Type u_2} [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] : Multiset ℕ

The finset of degrees of a finite graph.

Equations

• GraphTheory.ES1.degreeSequence G = Multiset.map (fun (a : α) => G.degree a) Finset.univ.val

theorem GraphTheory.ES1.q6 {α : Type u_2} [Fintype α] (s : Multiset ℕ) (hs : s.card = Fintype.card α) (h₀ : 0 ∉ s) : s.sum = 2 * Fintype.card α - 2 ↔ ∃ (G : SimpleGraph α) (x : DecidableRel G.Adj), degreeSequence G = s

Question 7

Let $$T_1, \dots, T_k$$ be subtrees of a tree $$T$$. Show that if $$V(T_i) ∩ V(T_j) ≠ ∅$$ for all $$i, j ∈ [k]$$ then $$V(T_1) ∩ \dots ∩ V(T_k) ≠ ∅$$.

theorem GraphTheory.ES1.q7 {ι : Type u_1} {α : Type u_2} (G : SimpleGraph α) (hG : G.IsAcyclic) (s : Finset ι) (f : ι → G.Subgraph) (hf : ∀ i ∈ s, (f i).coe.IsAcyclic) (h : ∀ i ∈ s, ∀ j ∈ s, f i ⊓ f j ≠ ⊥) : s.inf f ≠ ⊥

Question 8

The average degree of a graph $$G = (V, E)$$ is $$n^{-1} \sum_{x ∈ V} d(x)$$. Show that if the average degree of $$G$$ is $$d$$ then $$G$$ contains a subgraph with minimum degree $≥ d/2$$.

def GraphTheory.ES1.averageDegree {α : Type u_2} [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] : ℚ

The average degree of a simple graph is the average of its degrees.

Equations

• GraphTheory.ES1.averageDegree G = ∑ a : α, ↑(G.degree a) / ↑(Fintype.card α)

theorem GraphTheory.ES1.q8 {α : Type u_2} [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] : ∃ (H : G.Subgraph) (x : DecidableRel H.Adj), ∀ (a : α), averageDegree G / 2 ≤ ↑(H.degree a)

Question 9

Say that a graph $$G = (V, E)$$ can be decomposed into cycles if $$E$$ can be partitioned $$E = E_1 ∪ \dots ∪ E_k$$, where each $$E_i$$ is the edge set of a cycle. Show that $$G$$ can be decomposed into cycles if and only if all degrees of $$G$$ are even.

theorem GraphTheory.ES1.q9 {α : Type u_2} [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] : (∃ (𝒜 : Finset ((a : α) × G.Path a a)), (∀ (p q : (a : α) × G.Path a a), (↑p.snd).edges.Disjoint (↑q.snd).edges) ∧ ∀ (e : Sym2 α), ∃ p ∈ 𝒜, e ∈ (↑p.snd).edges) ↔ ∀ (a : α), Even (G.degree a)

Question 10

The clique number of a graph $$G$$ is the largest $$t$$ so that $$G$$ contains a complete graph on $$t$$ vertices. Show that the possible clique numbers for a regular graph on $$n$$ vertices are $$1, 2, \dots, n/2$$ and $$n$$.

theorem GraphTheory.ES1.q10 {α : Type u_2} [Fintype α] (n : ℕ) : (∃ (G : SimpleGraph α) (x : DecidableRel G.Adj) (k : ℕ), G.IsRegularOfDegree k ∧ G.cliqueNum = n) ↔ n ≤ Fintype.card α / 2 ∨ n = Fintype.card α

Question 11

Show that the Petersen graph is non-planar.

Question 12

Let $$G = (V, E)$$ be a graph. Show that there is a partition $$V = A ∪ B$$ so all the vertices in the graphs $$G[A]$$ and $$G[B]$$ are of even degree.

theorem GraphTheory.ES1.q12 {α : Type u_2} [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (s : Finset α) : ∃ (u : Finset α) (v : Finset α), Disjoint u v ∧ u ∪ v = s ∧ (∀ a ∈ u, Even (Cardinal.mk ↥({b ∈ u | G.Adj a b}))) ∧ ∀ a ∈ v, Even (Cardinal.mk ↥({b ∈ v | G.Adj a b}))

Question 13

A $$m × n$$ Latin rectangle is a $$m × n$$ matrix, with each entry from $${1, . . . , n}$$, such that no two entries in the same row or column are the same. Prove that every $$m × n$$ Latin rectangle may be extended to a $$n × n$$ Latin square.

def GraphTheory.ES1.IsLatin {α : Type u_2} {β : Type u_3} {γ : Type u_4} (f : α → β → γ) : Prop

A Latin rectangle is a binary function whose transversals are all injective.

Equations

• GraphTheory.ES1.IsLatin f = ((∀ (a : α), Function.Injective (f a)) ∧ ∀ (b : β), Function.Injective fun (a : α) => f a b)

theorem GraphTheory.ES1.q13 {α : Type u_2} {β : Type u_3} [Finite α] (g : β ↪ α) (f : β → α → α) (hf : IsLatin f) : ∃ (f' : α → α → α), f' ∘ ⇑g = f ∧ IsLatin f

Question 14

Let $$G = (X ∪ Y, E)$$ be a countably infinite bipartite graph with the property that $$|N(A)| ≥ |A|$$ for all $$A ⊆ X$$. Give an example to show that $$G$$ need not contain a matching from $$X$$ to $$Y$$ . On the other hand, show that if all of the degrees of $$G$$ are finite then $$G$$ does contain a matching from $$X$$ to $$Y$$. Does this remain true if $$G$$ is uncountable and all degrees of $$X$$ are finite (while degrees in $$Y$$ have no restriction)?

theorem GraphTheory.ES1.q14_part1 : ∃ (r : SetRel ℕ ℕ), (∀ (A : Finset ℕ), ↑A.card ≤ Cardinal.mk ↑(r.image ↑A)) ∧ ∀ (f : ℕ → ℕ), Function.Injective f → ∃ (n : ℕ), (n, f n) ∉ r

theorem GraphTheory.ES1.q14_part2 {α : Type u_2} {β : Type u_3} [DecidableEq β] [Countable α] [Countable β] (r : SetRel α β) [(a : α) → Fintype ↑(r.image {a})] (hr : ∀ (A : Finset α), A.card ≤ Fintype.card ↑(r.image ↑A)) : ∃ (f : α → β), Function.Injective f ∧ ∀ (a : α), (a, f a) ∈ r

theorem GraphTheory.ES1.q14_part3 {α : Type u_2} {β : Type u_3} [DecidableEq β] (r : SetRel α β) [(a : α) → Fintype ↑(r.image {a})] (hr : ∀ (A : Finset α), A.card ≤ Fintype.card ↑(r.image ↑A)) : ∃ (f : α → β), Function.Injective f ∧ ∀ (a : α), (a, f a) ∈ r

Question 15

Let $$(X, d_X)$$ be a metric space. We say that a function $$f : X → ℝ^2$$ has distortion $$≤ D$$ if there exists an $$r > 0$$ so that $$rd_X(x, y) ≤ ‖f(x) − f(y)‖_2 ≤ Drd_X(x, y)$$. Show that there is some constant $$c > 0$$ such that for all $$n$$ there is a metric space $$M = ({x_1, \dots, x_n}, d_M)$$ on $$n$$ points so that every function $$f : M → ℝ^2$$ has distortion $$> cn^{1/2}$$. Does there exist some constant $$c > 0$$ such that for all $$n$$ there is a metric space $$M = ({x_1, \dots, x_n}, d_M)$$ on $$n$$ points so that every function $$f : M → ℝ^2$$ has distortion $$> cn$$?

noncomputable def GraphTheory.ES1.distortion {α : Type u_2} {β : Type u_3} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β) : ℝ

The distortion of a function f between metric spaces is the ratio between the maximum and minimum of dist (f a) (f b) / dist a b.

Equations

• GraphTheory.ES1.distortion f = (⨆ (a : α), ⨆ (b : α), dist (f a) (f b) / dist a b) / ⨅ (a : α), ⨅ (b : α), dist (f a) (f b) / dist a b

theorem GraphTheory.ES1.q15_part1 : ∃ (ε : ℝ), 0 < ε ∧ ∀ (α : Type u_5) [inst : Fintype α], ∃ (x : MetricSpace α), ∀ (f : α → ℝ × ℝ), ε * √↑(Fintype.card α) ≤ distortion f

theorem GraphTheory.ES1.q15_part2 : ∃ (ε : ℝ), 0 < ε ∧ ∀ (α : Type u_5) [inst : Fintype α], ∃ (x : MetricSpace α), ∀ (f : α → ℝ × ℝ), ε * ↑(Fintype.card α) ≤ distortion f