ruzsaSzemerediNumber — Mathlib

English

The maximum number of edges in a locally linear graph on α.

Русский

Максимальное число ребер в локально линейном графе на α.

LaTeX

$$$ \max_{G\text{ locally linear on } \alpha} |E(G)| = ruzsaSzemerediNumber α $$$

Lean4

/-- The **Ruzsa-Szemerédi number** of a fintype is the maximum number of edges a locally linear
graph on that type can have.

In other words, `ruzsaSzemerediNumber α` is the maximum number of edges a graph on `α` can have such
that each edge belongs to exactly one triangle. -/
noncomputable def ruzsaSzemerediNumber : ℕ := by
  classical
    exact
    Nat.findGreatest (fun m ↦ ∃ (G : SimpleGraph α) (_ : DecidableRel G.Adj), #(G.cliqueFinset 3) = m ∧ G.LocallyLinear)
      ((card α).choose 3)

Похожие утверждения