Erdős Problem 74

Reference: erdosproblems.com/74

def Erdos74.SimpleGraph.edgeDistancesToBipartite {V : Type u} {G : SimpleGraph V} (A : G.Subgraph) : Set ℕ

For a given subgraph A, this is the set of all numbers k such that A can be made bipartite by deleting k edges.

Equations

• Erdos74.SimpleGraph.edgeDistancesToBipartite A = {x : ℕ | ∃ (E : Set (Sym2 V)) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x}

theorem Erdos74.SimpleGraph.edgeDistancesToBipartite_nonempty {V : Type u} {G : SimpleGraph V} (A : G.Subgraph) : (edgeDistancesToBipartite A).Nonempty

The set of edge distances to a bipartite graph is always non-empty because deleting all edges from a graph makes it bipartite.

noncomputable def Erdos74.SimpleGraph.minEdgeDistToBipartite {V : Type u} {G : SimpleGraph V} (A : G.Subgraph) : ℕ

The minimum number of edges that must be deleted from a subgraph A to make it bipartite.

Equations

• Erdos74.SimpleGraph.minEdgeDistToBipartite A = sInf (Erdos74.SimpleGraph.edgeDistancesToBipartite A)

def Erdos74.SimpleGraph.subgraphEdgeDistsToBipartite {V : Type u} (G : SimpleGraph V) (n : ℕ) : Set ℕ

For a graph G and a number n, this is the set of minEdgeDistToBipartite A for all induced subgraphs A of G on n vertices.

Equations

• Erdos74.SimpleGraph.subgraphEdgeDistsToBipartite G n = {x : ℕ | ∃ (A : G.Subgraph) (_ : A.verts.ncard = n) (_ : A.verts.Finite), Erdos74.SimpleGraph.minEdgeDistToBipartite A = x}

theorem Erdos74.SimpleGraph.subgraphEdgeDistsToBipartite_bddAbove {V : Type u} (G : SimpleGraph V) (n : ℕ) : BddAbove (subgraphEdgeDistsToBipartite G n)

The set of minimum edge distances to bipartite for subgraphs of size n is bounded above. A graph on n vertices has at most n choose 2 edges, and deleting all of them makes the graph bipartite, providing a straightforward upper bound.

noncomputable def Erdos74.SimpleGraph.maxSubgraphEdgeDistToBipartite {V : Type u} (G : SimpleGraph V) (n : ℕ) : ℕ

For a given graph $G$ and size $n$, this defines the smallest number $k$ such that any subgraph of $G$ on $n$ vertices can be made bipartite by deleting at most $k$ edges.

This value is optimal because it is the maximum of minEdgeDistToBipartite taken over all $n$-vertex subgraphs. This means there exists at least one $n$-vertex subgraph that requires exactly this many edge deletions. This is Definition 3.1 in [EHS82].

[EHS82] Erdős, P. and Hajnal, A. and Szemerédi, E., On almost bipartite large chromatic graphs Theory and practice of combinatorics (1982), 117-123.

Equations

• Erdos74.SimpleGraph.maxSubgraphEdgeDistToBipartite G n = sSup (Erdos74.SimpleGraph.subgraphEdgeDistsToBipartite G n)

theorem Erdos74.erdos_74 {V : Type u} : (∀ (f : ℕ → ℕ), Filter.Tendsto f Filter.atTop Filter.atTop → ∃ (G : SimpleGraph V), G.chromaticNumber = ⊤ ∧ ∀ (n : ℕ), SimpleGraph.maxSubgraphEdgeDistToBipartite G n ≤ f n) ↔ sorry

Let $f(n)\to \infty$ possibly very slowly. Is there a graph of infinite chromatic number such that every finite subgraph on $n$ vertices can be made bipartite by deleting at most $f(n)$ edges?

theorem Erdos74.erdos_74.variants.sqrt {V : Type u} : (∃ (G : SimpleGraph V), G.chromaticNumber = ⊤ ∧ ∀ (n : ℕ), ↑(SimpleGraph.maxSubgraphEdgeDistToBipartite G n) ≤ √↑n) ↔ sorry

Is there a graph of infinite chromatic number such that every finite subgraph on $n$ vertices can be made bipartite by deleting at most $\sqrt{n}$ edges?