Title: Degree sequences in triangle-free graphs Authors: P. Erdős, S. Fajtlowicz and W. Staton, Published in Discrete Mathematics 92 (1991) 85–88.

def IsCompactSequenceOn (d : ℕ → ℕ) (S : Set ℕ) : Prop

A sequence of natural numbers is compact on a set S if consecutive terms at distance 2 differ by 1 for all k ∈ S.

Equations

• IsCompactSequenceOn d S = ∀ k ∈ S, d (k + 2) = d k + 1

noncomputable def SimpleGraph.degreeFreq {α : Type u_1} [Fintype α] (G : SimpleGraph α) (d : ℕ) : ℕ

The number of vertices of G having degree d.

Equations

• G.degreeFreq d = {v : α | G.degree v = d}.card

theorem lemma1_a (d : ℕ → ℕ) (k : ℕ) (h_mono : Monotone d) (h_no_three : ∀ (k : ℕ), d (k + 2) ≠ d k) : 1 ≤ d (k + 2) - d k

Lemma 1 (a) If a sequence d is nondecreasing and no three terms are equal, then terms at distance 2 differ by at least 1.

theorem lemma1_b (d : ℕ → ℕ) (k r : ℕ) (h_mono : Monotone d) (h_pos : ∀ (k : ℕ), 0 < d k) (h_no_three : ∀ (i : ℕ), d (i + 2) ≠ d i) : r ≤ d (k + 2 * r) - d k

Lemma 1 (b) If a sequence d is nondecreasing and no three terms are equal, then terms at distance 2 * r differ by at least r.

theorem lemma2_a (d : ℕ → ℕ) (n : ℕ) (h_mono : Monotone d) (h_pos : ∀ (k : ℕ), 0 < d k) (h_no_three : ∀ (i : ℕ), d (i + 2) ≠ d i) : 2 * n * n ≤ ∑ i ∈ Finset.Icc (2 * n + 1) (4 * n), d i - ∑ i ∈ Finset.Icc 1 (2 * n), d i

Lemma 2 (a) Inequality involving sums of terms of a nondecreasing sequence with no three terms equal.

theorem lemma2_b (d : ℕ → ℕ) (n : ℕ) (h_mono : Monotone d) (h_pos : ∀ (k : ℕ), 0 < d k) (h_no_three : ∀ (i : ℕ), d (i + 2) ≠ d i) : 2 * n * n + 2 * n + 1 ≤ ∑ i ∈ Finset.Icc (2 * n + 1) (4 * n + 1), d i - ∑ i ∈ Finset.Icc 1 (2 * n), d i

Lemma 2 (b) Inequality involving sums of terms of a nondecreasing sequence with no three terms equal.

theorem lemma2_c (d : ℕ → ℕ) (n : ℕ) (h_mono : Monotone d) (h_pos : ∀ (k : ℕ), 0 < d k) (h_no_three : ∀ (i : ℕ), d (i + 2) ≠ d i) : 2 * n * n + 2 * n ≤ ∑ i ∈ Finset.Icc (2 * n + 2) (4 * n + 2), d i - ∑ i ∈ Finset.Icc 1 (2 * n + 1), d i

Lemma 2 (c) Inequality involving sums of terms of a nondecreasing sequence with no three terms equal.

theorem lemma2_d (d : ℕ → ℕ) (n : ℕ) (h_mono : Monotone d) (h_pos : ∀ (k : ℕ), 0 < d k) (h_no_three : ∀ (i : ℕ), d (i + 2) ≠ d i) : 2 * n * n + 4 * n + 2 ≤ ∑ i ∈ Finset.Icc (2 * n + 2) (4 * n + 3), d i - ∑ i ∈ Finset.Icc 1 (2 * n + 1), d i

Lemma 2 (d) Inequality involving sums of terms of a nondecreasing sequence with no three terms equal.

noncomputable def SimpleGraph.degreeSequence {α : Type u_1} [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] : List ℕ

The degree sequence of a graph, sorted in nondecreasing order.

Equations

• G.degreeSequence = Multiset.sort (fun (x1 x2 : ℕ) => x1 ≤ x2) (Multiset.map (fun (v : α) => G.degree v) Finset.univ.val)

def SimpleGraph.HasCompactdegreeSequence {α : Type u_1} [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] : Prop

The degree sequence of G is compact if it satisfies IsCompactSequenceOn for all valid indices k such that k + 2 < Fintype.card α.

Equations

• G.HasCompactdegreeSequence = IsCompactSequenceOn (fun (k : ℕ) => G.degreeSequence.getD k 0) {k : ℕ | k + 2 < Fintype.card α}

theorem SimpleGraph.theorem1 {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (h₁ : G.CliqueFree 3) (h₂ : G.f = 2) : G.IsBipartite ∧ G.minDegree = 1 ∧ G.HasCompactdegreeSequence

Theorem 1. If a triangle-free graph has f = 2, then it is bipartite, has minimum degree 1, and its degree sequence is compact.

theorem SimpleGraph.lemma3 (n : ℕ) (hn : 0 < n) : ∃ (G : SimpleGraph (Fin (8 * n))) (x : DecidableRel G.Adj), G.IsBipartite ∧ G.minDegree = n + 1 ∧ G.f = 3

Lemma 3. For every n there exists a bipartite graph with 8 n vertices, minimum degree n + 1, and f = 3.

theorem SimpleGraph.lemma4 {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (h₁ : G.CliqueFree 3) (v : α) : ∃ (β : Type u_2) (x : Fintype β) (H : SimpleGraph β) (x_1 : DecidableRel H.Adj) (i : G ↪g H), H.CliqueFree 3 ∧ H.degree (i v) = G.degree v + 1 ∧ (∀ (w : α), w ≠ v → H.degree (i w) = G.degree w) ∧ let J := induce (Set.range ⇑i).compl H; J.f = 3 ∧ J.minDegree ≥ 2 * Fintype.card α

Lemma 4. Let G be a triangle-free graph with n vertices and let v be a vertex of G. There exists a triangle-free graph H containing G as an induced subgraph such that: (i) the degree of v in H is one more than its degree in G; (ii) for every vertex w of G other than v the degree of w in H is the same as its degree in G; (iii) if J is the subgraph of H induced by the vertices not in G, then f(J)=3 and δ(J) ≥ 2n.

theorem SimpleGraph.theorem2 {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.CliqueFree 3) : ∃ (β : Type u_2) (x : Fintype β) (H : SimpleGraph β) (x : DecidableRel H.Adj) (i : G ↪g H), H.CliqueFree 3 ∧ H.f = 3

Theorem 2. Every triangle-free graph is an induced subgraph of one with f = 3.

noncomputable def SimpleGraph.F (n : ℕ) : ℕ

F n is the smallest number of vertices of a triangle-free graph with chromatic number n and f = 3.

Equations

• SimpleGraph.F n = sInf {p : ℕ | ∃ (G : SimpleGraph (Fin p)) (x : DecidableRel G.Adj), G.CliqueFree 3 ∧ G.chromaticNumber = ↑n ∧ G.f = 3}

theorem SimpleGraph.F_three : F 3 = 7

theorem SimpleGraph.F_four_le : F 4 ≤ 19