add latex proof for Mantel

FormalBook/Chapter_20.lean

@@ -54,9 +54,6 @@ open Classical
     - Second proof
 -/
 
--- porting note: waiting for
--- https://leanprover-community.github.io/mathlib-port-status/file/analysis/inner_product_space/basic
-
 section Inequalities
 
 -- Not quite sure what we actually need here, want to have ℝ-vector space with inner product.
@@ -88,7 +85,7 @@ theorem cauchy_schwarz_inequality (a b : V) : ⟪ a, b ⟫ ^ 2 ≤ ‖a‖ ^ 2 *
         use -x
         rw [← add_zero (-x•a), ← hx]
         simp only [neg_smul, neg_add_cancel_left]
-      have : ∀ (x : ℝ), 0 < ‖x • a + b‖^2 := by
+      have : ∀ (x : ℝ), 0 < ‖x • a + b‖ ^ 2 := by
         exact fun x ↦ sq_pos_of_pos (this x)
       have : ∀ (x : ℝ), 0 <  x ^ 2 * ‖a‖ ^ 2 + 2 * x * ⟪a, b⟫ + ‖b‖ ^ 2 := by
         convert this
@@ -99,7 +96,6 @@ theorem cauchy_schwarz_inequality (a b : V) : ⟪ a, b ⟫ ^ 2 ≤ ‖a‖ ^ 2 *
           0 <  x ^ 2 * ‖a‖ ^ 2 + 2 * x * ⟪a, b⟫ + ‖b‖ ^ 2 := this x
           _ = ‖a‖ ^ 2 * (x * x)  + 2 * ⟪a, b⟫ * x + ‖b‖ ^ 2  := by ring_nf
       have ha_sq : ‖a‖ ^ 2 ≠ 0 := by aesop
-
       have := discrim_lt_zero ha_sq this
       unfold discrim at this
       have  : (2 * inner a b) ^ 2 < 4 * ‖a‖ ^ 2 * ‖b‖ ^ 2 := by linarith
@@ -155,6 +151,7 @@ local notation "I(" v ")" => G.incidenceFinset v
 local notation "d(" v ")" => G.degree v
 local notation "n" => Fintype.card α
 
+-- TODO: equality #E = (n^2 / 4) iff G = K_{n/2, n/2}
 theorem mantel (h: G.CliqueFree 3) : #E ≤ (n^2 / 4) := by
 
   -- The degrees of two adjacent vertices cannot sum to more than n

blueprint/src/chapter/chapter20.tex

@@ -98,12 +98,33 @@ \chapter{In praise of inequalities}
 
 \begin{theorem}
   \label{ch20theorem3proof1}
+  \lean{mantel}
   Suppose $G$ is a graph on $n$ vertices without triangles. Then $G$
   has at most $\frac{n^2}{4}$ edges, and equality holds only when $n$ is even and $G$ is the
   complete bipartite graph $K_{n/2, n/2}$.
 \end{theorem}
 \begin{proof}
-  TODO
+  This proof, using Cauchy's inequality, is due to Mantel.
+  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|$
+  (see chapter \ref{chapter28}). 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| \geq \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, \dots, d_n)$ and $(1, \dots, 1)$,
+  \[
+  n|E| \geq \sum_{i \in V} d_i^2 \geq \frac{\left( \sum d_i \right)^2}{n} = \frac{4|E|^2}{n},
+  \]
+  and the result follows. In the case of equality we find $d_i = d_j$ for all $i, j$, and further $d_i = \frac{n}{2}$ (since $d_i + d_j = n$). Since $G$ is triangle-free, $G = K_{n/2, n/2}$ is immediately seen from this. \qed
+
 \end{proof}
 
 \begin{theorem}

blueprint/src/chapter/chapter28.tex

@@ -1,5 +1,5 @@
 \chapter{Pigeon-hole and double counting}
-
+\label{chapter28}
 \begin{theorem}[Pigeon-hole princinple]
   \label{pigeon_hole_principle}
   \lean{pigeon_hole_principle}