Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1995P5

module

public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.Combinatorics.SimpleGraph.Clique
public import Mathlib.Combinatorics.SimpleGraph.DegreeSum

public section


/-!
# USA Mathematical Olympiad 1995, Problem 5

A graph with n points and k edges has no triangles. Show that it has a
point P such that there are at most k(1 - 4k/n²) edges between points
not joined to P (by an edge).
-/

namespace Usa1995P5

open Finset SimpleGraph

variable {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]

theorem usa1995_p5 {n : ℕ} [NeZero n] (G : SimpleGraph (Fin n))
    [DecidableRel G.Adj] (hG : G.CliqueFree 3) :
    ∃ P : Fin n,
      (#(G.edgeFinset.filter fun e => ∀ v ∈ e, ¬G.Adj P v) : ℝ)
        ≤ (#G.edgeFinset : ℝ) * (1 - 4 * #G.edgeFinset / n ^ 2) := sorry

end Usa1995P5

File author(s): Kimi K3

This problem has a complete formalized solution.