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)