Turán’s Theorem Formalization
0.1 Concentrating support on a clique - Improve Operartion
Given a finite simple graph \(G=(V,E)\), a weight distribution is a function
A probability distribution on the vertex Set.
For \(w\in W\), the total edge weight is
In words: sum the edge values over all edges of the graph.
Given a weight function \(w\), define \(w^*\) such that \(\mathrm{supp}(w^*) \subseteq \mathrm{supp}(w)\) and
That is \(w^*\) is a distribution with non-decreasing total edge weight with the original support of \(w\) preserved.
Given distinct vertices \(v_j \neq v_i\), define \(w' := \texttt{Improve}(W, v_j, v_i)\) by moving all weight from \(v_j\) to \(v_i\):
The sum over edges \(E\) of the function \(\texttt{vp}\) splits as
That is the total sum decomposes into parts incident to \(v_i\), incident to \(v_j\), and the rest.
The increment in the sum over edges incident to \(v_i\) is
where \(N(v_i)\) is the neighborhood of \(v_i\).
The sum over edges incident to \(v_j\) after the transfer satisfies
For edges \(e\) not incident to \(v_i\) or \(v_j\),
Edges outside \(v_i\) and \(v_j\) neighborhoods remain unchanged under the operation.
Given non adjacent vertices \(v_i\), \(v_j\) and assuming that the neightborsum of weights at \(s_i\) is equal or greater than that of \(s_j\), we have
that is the total edge weight does not decrease after applying Improve.
The new distribution \(w'\) has a strictly smaller support:
The support of \(w^*\) forms a clique:
In words: every two distinct vertices with positive weight in \(w^*\) are adjacent.
0.2 The Enhance Operation
Given distinct non-adjacent vertices \(v_j, v_i\), define \(w^+\) by transferring \(\varepsilon {\gt} 0\) weight from \(v_j\) to \(v_i\):
with the condition \(\{ v_j, v_i\} \notin E\). The Enhance transfers weight between non-adjacent vertices to increase edge weight.
The edge set \(E\) partitions as
where
In words: edges are split into the incidence set to \(v_i\), the one to \(v_j\), and the rest.
Under Theorem 12, the change in the sum over edges incident to \(v_i\) satisfies
That is the gain vertex’s edge contribution increases by \(\varepsilon \) times the sum of its neighbors’ weights.
Under Theorem 12, the sum over edges incident to \(v_j\) satisfies
That is the loose vertex’s incident edge contributions become zero after Enhance.
Define a bijection
mapping edges incident to \(v_j\) (except \(s(v_j,v_i)\)) to edges incident to \(v_i\) (except \(s(v_j,v_i)\)). In words: this bijection pairs edges incident to \(v_j\) with edges incident to \(v_i\) within the clique.
For any edge \(e\) incident to \(v_j\) (excluding \(s(v_j, v_i)\)), the "other" vertex weight satisfies
In words: the bijection preserves weights at the other endpoints of edges.
The total weight transfer balances the edge contributions:
In words: the combined edge contributions of loose and gain vertices do not decrease after Enhance.
For edges \(e \in E_{\mathrm{rest}}\),
In words: edges not incident to \(v_i\) or \(v_j\) remain unaffected by Enhance.
The total edge contribution satisfies:
That is, the total contribution from gain and loose vertices does not decrease.
For any vertex \(v \notin \{ v_i, v_j\} \), the edge contributions satisfy
In words: vertices outside gain and loose retain their edge contributions after Enhance.
For a given distribution \(w\in W\) Applying Enhance (\(w^+\)) strictly increases the total edge weight:
That is, the Enhance operation strictly improves the total edge weight contribution.
0.3 Equalizing the weights on the clique - EnhanceD
For a given distribution \(w\), \(K\) is the maximal number of uniform vertices achievable without decreasing the total edge weight
.
There exists \(w_M\) with \(\mathrm{supp}(w_M) \subseteq \mathrm{supp}(w)\), \(w_M.\mathrm{fw} \geq W.\mathrm{fw}\), and with at least \(m\) vertices having weight \(1/m\). In words: a maximiser \(w_M\) achieving the maximal uniform vertex count exists.
Given \(w\in \mathcal{W}\) whose support induces a clique, define
to be the witness provided by Theorem 24: it preserves the zero set of \(W\), its support is a clique, satisfies \(f(w_M)\ge f(w)\), and achieves the maximal number \(K=\texttt{max\_ uniform\_ support}(w)\) of vertices with weight \(1/k\) (where \(k=|\operatorname {supp}(w)|\)).
Define
In words: \(\mathsf{the\_ \varepsilon }\) is the difference between the largest vertex weight and the average \(1/k\).
Let \(v_{\max }\) and \(v_{\min }\) be vertices attaining the maximal and minimal weights of \(w\), respectively. Set \(\varepsilon := \mathsf{the\_ \varepsilon }\) and define
In words: \(w^+\) transfers the carefully chosen \(\varepsilon \) from the heaviest to the lightest vertex.
For any vertex \(v\) with \(w(v) = \frac{1}{|\mathrm{supp}(w)|}\),
In words: vertices already at uniform weight remain unchanged under Enhanced.
The weight at the argmax vertex \(v_j\) after Enhanced satisfies
That is, Enhanced reduces the argmax vertex’s weight to the uniform weight.
The number of vertices with weight \(\frac{1}{|\mathrm{supp}(W)|}\) increases after Enhanced:
For every vertex \(v \in \mathrm{supp}(w_M)\),
That is the weights of all support vertices in UniformBetter are uniform.
For any edge \(e = \{ v_a, v_b\} \) with \(v_a, v_b \in \mathrm{supp}(w_M)\),
In words: every supported edge has value equal to the square of the uniform vertex weight.
If \(|\mathrm{supp}(w_M)| = k\), then
For \(k {\gt} 0\),
That is the total edge weight for a clique with uniform weights simplifies to \(\frac{1}{2}(1 - \frac{1}{k})\).
The function
is nondecreasing for \(k \geq 1\).
If \(w\) is supported on a clique of size \(k \leq p-1\), then
In words: the total edge weight is bounded by the Turán bound for cliques of size less than \(p\).
Define
That is, the uniform vertex weight distribution assigns equal weight \(1/|V|\) to every vertex.
The total edge weight satisfies
THat is, the total edge weight under uniform vertex weights equals the number of edges times the square of the uniform weight.
Let \(p \geq 2\) and let \(G\) be a \(p\)-clique-free graph. Then