Mantel’s theorem goes back to 1907 and is a foundational result in extremal graph theory. It can be viewed as the first non-trivial case of Turán’s theorem and essentially states that any triangle-free graph can contain at most 50% of all possible edges.

Mantel's Theorem. Suppose \(G\) is a graph on \(n\) vertices without triangles. Then \(G\) has at most \(\lfloor n^2/4 \rfloor\) edges, and equality holds if and only if \(G\) is the complete bipartite graph \(K_{\lfloor n/2 \rfloor, \lceil n/2 \rceil}\).

For now, we will limit ourselves to establishing the upper bound on the number of edges and leave the characterization of the extremal example for a future post. Here we will follow the proof using Cauchy’s inequality and the handshaking lemma, which Aigner and Ziegler attribute to Mantel himself.

Proof. Let \(V = \{1, \dots, n\}\) be the vertex set and \(E\) the edge set of \(G\). By \(d_i\) we denote the degree of \(i\), hence \(\sum_{i \in V} d_i = 2|E|\). Suppose ij is an edge. Since \(G\) has no triangles, we find \(d_i + d_j \leq n\) since no vertex is a neighbor of both \(i\) and \(j\). It follows that \[\sum_{ij \in E} d_i + d_j \leq n |E|.\] Note that \(d_i\) appears exactly \(d_i\) times in the sum, so we get \[n |E| \ge \sum_{ij \in E} (d_i + d_j) = \sum_{i \in V} d_i^2,\] and hence with Cauchy's inequality applied to the vectors \((d_1, \ldots, d_n)\) and \((1, \ldots, 1)\), \[n |E| \ge \sum_{i \in V} d_i^2 \ge \frac{(\sum d_i)^2}{n} = \frac{4 |E|^2}{n},\] and the result follows.
Aigner, M., & Ziegler, G. M. (5th ed.). Proofs from THE BOOK, p. 145.

As for the handshaking lemma, we first set up some notation, i.e., we use # to denote the cardinality of a set, V and E to denote the vertex1 and edge set2 of a given (G : SimpleGraph α), I(v) and d(v) to respectively denote the set of edges incident to a vertex v as well as its degree, and finally n to denote the order of G.

1
2
3
4
5
6

prefix:100 "#" => Finset.card
local notation "V" => @Finset.univ α _
local notation "E" => G.edgeFinset
local notation "I(" v ")" => G.incidenceFinset v
local notation "d(" v ")" => G.degree v
local notation "n" => Fintype.card α

Using this, we can now easily state (our simplified version of) Mantel’s theorem.

1

theorem mantel (h: G.CliqueFree 3) : #E ≤ (n^2 / 4) := by

At first it might seem like we cheated: \(n^2 / 4\) is not \( \lfloor n^2 / 4 \rfloor \)! But all involved quantities, that is #E, n^2, and 4 are integer, so n^2 / 4 in fact corresponds to the integer \(\lfloor n^2 / 4 \rfloor\) mathlib’s documentation of HDiv.

The proof now starts with “Suppose (ij) is an edge. Since (G) has no triangles, we find \(d_i + d_j \leq n\) since no vertex is a neighbor of both \(i\) and \(j\).” The statement of this fact is easily written down, but for its proof we need to be slightly more detailed.

1
2
3
4
5
6

  have adj_degree_bnd (i j : α) (hij: G.Adj i j) : d(i) + d(j) ≤ n := by
    by_contra hc; simp at hc
    obtain ⟨k, h⟩ := Finset.inter_nonempty_of_card_lt_card_add_card (by simp) (by simp) hc
    simp at h
    obtain ⟨hik, hjk⟩ := h
    exact h {k, j, i} ⟨by aesop (add safe G.adj_symm), by simp [hij.ne', hik.ne', hjk.ne']⟩

The proof follows by contradiction, i.e., using by_contra we assume that d(i) + d(j) > n. Of course, since there are only n vertices, this means that by pigeon-hole-principle, or by inter_nonempty_of_card_lt_card_add_card to be precise, the vertices i and j have a common neighbor k. But now, \(\{i,j,k\}\) would of course form a triangle, contradicting that G is assumed to betriangle-free.

For the next step we will need the sum \(\sum_{ij \in E} d(i) + d(j)\). There is a minor detail in this notation that is easily overlooked but that Lean does not let us get away with: the term d(i) + d(j) is only well-defined if it is independent of the order of i and j. This is of course true by commutativity, so we give Lean that information in a definition of the sum_deg of an edge. By the just established fact that two adjacent vertices i and j satisfy d(i) + d(j) ≤ n, sum_deg is of course also upper bounded by n.

1
2
3
4

  let sum_deg (e : Sym2 α) : ℕ := Sym2.lift ⟨λ x y ↦ d(x) + d(y), by simp [Nat.add_comm]⟩ e

  have adj_degree_bnd' (e : Sym2 α) (he: e ∈ E) : sum_deg e ≤ n := by
    induction e with | _ v w => simp at he; exact adj_degree_bnd v w (by simp [he])

Let us now address the statement that “\(d_i\) appears exactly \(d_i\) times in the sum, so we get \(\sum_{ij \in E} (d_i + d_j) = \sum_{i \in V} d_i^2\)”, which again requires a bit more detail to formally prove. The decisive step here uses Finset.sum_sum_bipartiteAbove_eq_sum_sum_bipartiteBelow, a weighted double counting lemma [17651] .

1
2
3
4
5
6
7

  have sum_sum_deg_eq_sum_deg_sq : ∑ e ∈ E, sum_deg e = ∑ v ∈ V, d(v)^2 := by
    calc  ∑ e ∈ E, sum_deg e
      _ = ∑ e ∈ E, ∑ v ∈ e, d(v)                  := Finset.sum_congr rfl (λ e he ↦ by induction e with | _ v w => simp at he; simp [sum_deg, he.ne])
      _ = ∑ e ∈ E, ∑ v ∈ {v' ∈ V | v' ∈ e}, d(v)  := Finset.sum_congr rfl (by intro e _; exact congrFun (congrArg Finset.sum (by ext; simp)) _)
      _ = ∑ v ∈ V, ∑ _ ∈ {e ∈ E | v ∈ e}, d(v)    := Finset.sum_sum_bipartiteAbove_eq_sum_sum_bipartiteBelow _ E V _
      _ = ∑ v ∈ V, ∑ _ ∈ I(v), d(v)               := Finset.sum_congr rfl (λ v ↦ by simp [G.incidenceFinset_eq_filter v])
      _ = ∑ v ∈ V, d(v)^2                         := by simp [Nat.pow_two]

This finally allows us to get to the meat of the argument, namely the following calculation. We have slightly modified it from the template by multplying with n to avoid moving from natural numbers to rationals. The most important step is the application of Cauchy’s inequality, or more specifically sum_mul_sq_le_sq_mul_sq3, and the handshaking lemma in the form of sum_degrees_eq_twice_card_edges.

1
2
3
4
5
6
7
8

  have := calc #E * n^2
    _ = (n * (∑ e ∈ E, 1)) * n               := by simp [Nat.pow_two, Nat.mul_assoc, Nat.mul_comm]
    _ = (∑ _ ∈ E, n) * n                     := by rw [Finset.mul_sum]; simp
    _ ≥ (∑ e ∈ E, sum_deg e) * n             := Nat.mul_le_mul_right n (Finset.sum_le_sum adj_degree_bnd')
    _ = (∑ v ∈ V, d(v)^2) * (∑ v ∈ V, 1^2)   := by simp [sum_sum_deg_eq_sum_deg_sq]
    _ ≥ (∑ v ∈ V, d(v) * 1)^2                := (Finset.sum_mul_sq_le_sq_mul_sq V (λ v ↦ d(v)) 1)
    _ = (2 * #E)^2                           := by simp [G.sum_degrees_eq_twice_card_edges]
    _ = 4 * #E^2                             := by ring

Aigner and Ziegler conclude with “… and the result follows.” Lean however does not let us get away with so easily. We first massage our ineqality into the right form through a series of rw.

1
2
3

  rw [Nat.pow_two (#E)] at this
  rw [(Nat.mul_assoc 4 (#E) (#E)).symm] at this
  rw [Nat.mul_comm (4 * #E) (#E)] at this

We then conclude by simply dividing by 4 * #E… which is only possibly if #E is not zero! So we need to do a case distinction using by_cases and only then are we able to get the desired statement.

1
2
3
4
5
6

  by_cases hE : #E = 0
  · simp [hE]
  · apply Nat.zero_lt_of_ne_zero at hE
    apply Nat.le_of_mul_le_mul_left this at hE
    rw [Nat.mul_comm] at hE
    exact (Nat.le_div_iff_mul_le (Nat.zero_lt_succ 3)).mpr hE

This concludes the proof. 🎉

  1. Technically the vertices of (G : SimpleGraph α) are fully characterized by the type α, which should satisfy [Fintype α] in order for G to be a finite graph, and the explicit use of the set of all vertices V is superfluous. In many cases one could in fact simply replace ∑ v ∈ V with ∑ v : α or even just ∑ v and be closer to the ‘correct’ way of formulating the statement. ↩

  2. The edge set however truly needs to be a set, since the underlying type Sym2 α simply corresponds to all possible edges, including loops, in a complete graph with vertices of type α. ↩

  3. There is a large number of Cauchy’s inequalities in mathlib, but for our purposes this Finset version is the most useful one. ↩