Weighted Turán's Theorem

Let $G = (V, E)$ be a finite undirected simple graph, $x \colon V \to \mathbb{R_{\ge 0}}$ be a weight function. Prove that $$\sum_{(u, v) \in E} x(u)x(v) \leq \frac {\omega(G) - 1} {2 \omega(G)} \left( \sum_{v \in V} x(v) \right)^2,$$ where $\omega(G)$ is the maximum number of vertices in a clique of graph $G$.

import Mathlib.Combinatorics.SimpleGraph.Clique
import Mathlib.Data.NNReal.Defs

theorem solution {V : Type u} [Fintype V] [DecidableEq V]
    {G : SimpleGraph V} [DecidableRel G.Adj] (x : V → NNReal) : ∑ e ∈ G.edgeFinset, (e.map x).mul ≤
    (G.cliqueNum - 1 : ℕ) / (2 * G.cliqueNum) * (∑ v : V, x v) ^ 2 := sorry

Submit Solution

Login to submit a solution.

Recent Submissions