Mantel's Theorem via the Inequality of the Arithmetic and Geometric Mean
Acknowledgements. Mathlib contains a proof of Turán’s theorem due to Jeremy Tan, which implies Mantel’s theorem. The code presented here was implemented from scratch to closely follow the natural language version of the proof as presented by Martin Aigner and Günter Ziegler in their book ‘Proofs from THE BOOK’.
In this post, we provide another proof for Mantel’s theorem. Let’s recall the statement from the previous post:
Again, we focus on proving the upper bound for now. The following proof is supposed to be folklore, and uses the inequality of the arithmetic and geometric mean.
The theorem statement is the same as the one we’ve seen in the previous post:
1 |
theorem mantel (h: G.CliqueFree 3) : #E ≤ (n^2 / 4) := by |
The proof begins with the words “Let \(\alpha\) be the size of a largest independent set \(A\), and set \(\beta = n - \alpha\)”. \(\alpha\) is also refered to as the coclique number and obtain the existence of a maximum independent set \(A\) attaining that number from maximumIndependentSet_exists [18446]
[18694]
:
1 2 3 |
let α := SimpleGraph.cocliqueNum G let ⟨A, maxA⟩ := G.maximumIndependentSet_exists have hA : #A = α := maximumIndependentSet_card_eq_cocliqueNum _ _ maxA |
We then continue “and set \(\beta = n - \alpha\) ”.
1 2 |
let β := n - α have hαβ: α + β = n := Nat.add_sub_of_le (le_of_eq_of_le (hA.symm) (card_le_card (subset_univ _))) |
Note that we are again using subtraction in Nat, so the proof that α + β = n requires us to show that in fact α ≤ n, which follows by card_le_card and subset_univ. The proof thenmakes some brief statements that are used to justify the final inequality chain, beginning with “Since \(G\) is triangle-free, the neighbors of a vertex \(i\) form an independent set, and we infer \(d_i \leq \alpha\) for all \(i\).” The first half of that is the exact statement of theorem isIndependentSet_neighborSet_if_triangleFree [18694]
, but we’ll have to adjust it to finite sets to use it in our proof.
1 2 |
have nbhd_ind_of_triangle_free : ∀ (i : γ), G.IsIndependentSet N(i) := by simp [Set.coe_toFinset, G.isIndependentSet_neighborSet_if_triangleFree h, neighborFinset] |
The second half of the sentence, “we infer \(d_i \leq \alpha\) for all \(i\)”, requires us to use two more theorems about independent sets. The first is card_le_cocliqueNum [18446]
[18447]
, stating that the cardinality of any independent set is less than or equal to the coclique number. The second is maximumIndependentSet_card_eq_cocliqueNum [18446]
[18447]
, stating that the cardinality of a maximum independent set is precisely said coclique number. Combining them with our previous lemma using transitivity of inequality and equality, we obtain:
1 2 3 |
have degree_le_alpha : ∀ (i : γ) , d(i) ≤ α := fun i =>
hA ▸ (le_of_le_of_eq (nbhd_ind_of_triangle_free i).card_le_cocliqueNum
(G.maximumIndependentSet_card_eq_cocliqueNum A maxA).symm)
|
The next step is to prove the inequality \(|E| \leq \sum_{i \in B} d_i\). The proof states “The set \(B = V \setminus A\) of size \(\\beta\) meets every edge of \(G\)”, which is the statement of the theorem compl_independentSet_meets_every_edge [18608]
. Since we’re about to prove the next step in lean using a chain of inequalities with the calc tactic, we will turn the statement about “meeting every edge” into an inequality:
1 2 3 4 5 6 |
let B := V \ A
have hB : #B = β := by have := card_sdiff (subset_univ A); simp_all [hαβ]
have one_ge_num_incident_verts : ∀ e ∈ E, 1 ≤ #{ i ∈ B | i ∈ e } := by
simp only [one_le_card, mem_edgeFinset]
exact G.compl_independentSet_meets_every_edge maxA.independentSet
|
Equipped with this, we can prove our lemma using calc:
1 2 3 4 5 6 7 8 9 |
have count_edges_by_B := by calc
#E = ∑ e ∈ E, 1 := by simp
_ ≤ ∑ e ∈ E, #{ i ∈ B | i ∈ e } := sum_le_sum one_ge_num_incident_verts
_ = ∑ e ∈ E, ∑ i ∈ {i ∈ B | i ∈ e}, 1 := by simp
_ = ∑ i ∈ B, ∑ e ∈ {e ∈ E | i ∈ e}, 1 := sum_sum_bipartiteAbove_eq_sum_sum_bipartiteBelow _ _
_ = ∑ i ∈ B, #{e ∈ E | i ∈ e} := by simp
_ = ∑ i ∈ B, d(i) := sum_congr rfl fun i _ => by
rw [(G.card_incidenceFinset_eq_degree i).symm,
G.incidenceFinset_eq_filter]
|
Note that, like in the previous post, we use the weighted double counting lemma Finset.sum_sum_bipartiteAbove_eq_sum_sum_bipartiteBelow[17651]
. We are now equipped to prove the final chain of inequalities: \[|E| \leq \sum_{i \in B} d_i \leq \alpha \beta \leq \left( \frac{ \alpha + \beta}{2} \right)^2 = \frac{n^2}{4}. \]
Since rational numbers are more involved to deal with, we start with proving the first two steps, using the lemmata about meeting all edges and bounded degree:
1 2 3 4 |
have card_E_bound := calc
#E ≤ ∑ i ∈ B, d(i) := by exact count_edges_by_B
_ ≤ ∑ _ ∈ B, α := sum_le_sum fun _ _ => degree_le_alpha _
_ = α * β := by simp [Nat.mul_comm, hB]
|
The remaining two steps are first proven multiplied by four, so we can stick to natural numbers and deal with the division in the end. This is where we use the inequality of the arithmetic and geometric mean that gives this post its name, by invoking four_mul_le_pow_two_add from Mathlib.Analysis.MeanInequalities [17877]
.
1 2 3 |
4 * #E ≤ 4 * α * β := by linarith
_ ≤ (α + β)^2 := four_mul_le_pow_two_add _ _
_ = n^2 := by simp only [hαβ, Nat.sub_add_cancel]
|
Finally, all that’s left to do is divide both sides by four [18694] , and we’re done!
1 |
exact (Nat.le_div_iff_mul_le_comm Nat.ofNat_pos).mpr four_times_card_E_bd |
This concludes the proof. 🎉