Books in graphs

DefinitionBook number#✓fully proved

Let \(G\) be a finite simple graph. The book number of \(G\) is the maximum, over ordered pairs \((u, v)\) of adjacent vertices, of the number of common neighbors of \(u\) and \(v\) (the number of triangles containing the edge \(uv\)); it is \(0\) if \(G\) has no edges.

noncomputable def bookNumber (G : SimpleGraph V) [DecidableRel G.Adj] : ℕ :=
  Finset.sup Finset.univ fun p : V × V =>
    if G.Adj p.1 p.2 then
      (Finset.univ.filter fun w => G.Adj p.1 w ∧ G.Adj p.2 w).card
    else 0

Used by 2

Used byBounding the book number · Common neighbors of an edge are bounded by the book number

TheoremCommon neighbors of an edge are bounded by the book number#✓fully proved

Let \(G\) be a finite simple graph. If \(u\) and \(v\) are adjacent vertices of \(G\), then the number of common neighbors of \(u\) and \(v\) is at most the book number of \(G\).

theorem le_bookNumber {u v : V} (h : G.Adj u v) :
    (Finset.univ.filter fun w => G.Adj u w ∧ G.Adj v w).card ≤ G.bookNumber

Uses 1

Statement usesBook number

TheoremBounding the book number#✓fully proved

Let \(G\) be a finite simple graph and \(b\) a natural number. If every pair of adjacent vertices \(u\), \(v\) of \(G\) has at most \(b\) common neighbors, then the book number of \(G\) is at most \(b\).

theorem bookNumber_le (b : ℕ)
    (h : ∀ u v : V, G.Adj u v →
      (Finset.univ.filter fun w => G.Adj u w ∧ G.Adj v w).card ≤ b) :
    G.bookNumber ≤ b

Uses 1

Statement usesBook number

DefinitionErdős Problem 905 on edges in many triangles#✓fully proved

The proposition asserts that for every natural number \(n\) and every simple graph \(G\) on \(n\) vertices with more than \(n^2/4\) edges, some edge of \(G\) lies in at least \(n/6\) triangles of \(G\).

def conjecture : Prop :=
  ∀ (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj],
    (n : ℝ) ^ 2 / 4 < (G.edgeFinset.card : ℝ) →
    ∃ e : G.edgeSet, (n : ℝ) / 6 ≤ ((G.trianglesContaining e).card : ℝ)

Uses 1 · Used by 1

Statement usesTriangles containing an edge

Used byEdwards–Khadzhiivanov–Nikiforov theorem on edges in many triangles

TheoremEdwards–Khadzhiivanov–Nikiforov theorem on edges in many triangles#●ready to prove

For every natural number \(n\), every simple graph \(G\) on \(n\) vertices with more than \(n^2/4\) edges has an edge that lies in at least \(n/6\) triangles of \(G\).

This was proved independently by Edwards and by Khadzhiivanov and Nikiforov, and answers Erdős Problem 905 affirmatively.

public theorem_wanted conjecture_holds : conjecture

Sources

• External Lean proof of Erdős Problem 905, https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/v4.29.1/ErdosProblems/Erdos905.lean.

Uses 1

Statement usesErdős Problem 905 on edges in many triangles

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.