/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilErdős Problem 74
Reference: erdosproblems.com/74
open Filter SimpleGraphopen scoped Topology Realnamespace Erdos74open Erdos74universe uvariable {V : Type u}
For a given subgraph A, this is the set of all numbers k such that A can be made
bipartite by deleting k edges.
def SimpleGraph.edgeDistancesToBipartite {G : SimpleGraph V} (A : G.Subgraph) : Set ℕ :=
{ (E.ncard) | (E : Set (Sym2 V)) (_ : E ⊆ A.edgeSet) (_ : IsBipartite (A.deleteEdges E).coe)}set_option backward.isDefEq.respectTransparency false inThe set of edge distances to a bipartite graph is always non-empty because deleting all edges from a graph makes it bipartite.
@[category test, AMS 5]
theorem SimpleGraph.edgeDistancesToBipartite_nonempty {G : SimpleGraph V} (A : G.Subgraph) :
SimpleGraph.edgeDistancesToBipartite A |>.Nonempty := V:Type uG:SimpleGraph VA:G.Subgraph⊢ (edgeDistancesToBipartite A).Nonempty
V:Type uG:SimpleGraph VA:G.Subgraph⊢ {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x}.Nonempty
V:Type uG:SimpleGraph VA:G.Subgraph⊢ (A.deleteEdges A.edgeSet).coe.IsBipartite
V:Type uG:SimpleGraph VA:G.Subgraph⊢ ∀ {a b : ↑(A.deleteEdges A.edgeSet).verts}, (A.deleteEdges A.edgeSet).coe.Adj a b → (completeGraph (Fin 2)).Adj 0 0
All goals completed! 🐙
The minimum number of edges that must be deleted from a subgraph A to make it bipartite.
noncomputable def SimpleGraph.minEdgeDistToBipartite {G : SimpleGraph V} (A : G.Subgraph) : ℕ :=
sInf <| SimpleGraph.edgeDistancesToBipartite A
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.
def SimpleGraph.subgraphEdgeDistsToBipartite (G : SimpleGraph V) (n : ℕ) : Set ℕ :=
{ (SimpleGraph.minEdgeDistToBipartite A) |
(A : Subgraph G) (_ : A.verts.ncard = n) (_ : A.verts.Finite) }set_option backward.isDefEq.respectTransparency false in
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.
V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = mthis:A.edgeSet.ncard ≤ n.choose 2⊢ sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} ≤ n.choose 2
V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = mthis:A.edgeSet.ncard ≤ n.choose 2⊢ sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} ≤ A.edgeSet.ncard
V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = mthis:A.edgeSet.ncard ≤ n.choose 2⊢ A.edgeSet.ncard ∈ {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x}
V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = mthis:A.edgeSet.ncard ≤ n.choose 2⊢ ∃ E ⊆ A.edgeSet, (A.deleteEdges E).coe.IsBipartite ∧ E.ncard = A.edgeSet.ncard
V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = mthis:A.edgeSet.ncard ≤ n.choose 2⊢ A.edgeSet ⊆ A.edgeSet ∧ (A.deleteEdges A.edgeSet).coe.IsBipartite ∧ A.edgeSet.ncard = A.edgeSet.ncard
refine ⟨V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = mthis:A.edgeSet.ncard ≤ n.choose 2⊢ A.edgeSet ⊆ A.edgeSet All goals completed! 🐙, ?_, rfl⟩
V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = mthis:A.edgeSet.ncard ≤ n.choose 2⊢ ∀ {a b : ↑A.verts}, (A.deleteEdges A.edgeSet).coe.Adj a b → (completeGraph (Fin 2)).Adj 0 0
All goals completed! 🐙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.
noncomputable def SimpleGraph.maxSubgraphEdgeDistToBipartite
(G : SimpleGraph V) (n : ℕ) : ℕ := sSup <| SimpleGraph.subgraphEdgeDistsToBipartite G nLet $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?
@[category research open, AMS 5]
theorem erdos_74 : answer(sorry) ↔ ∀ f : ℕ → ℕ, Tendsto f atTop atTop →
(∃ (V : Type u) (G : SimpleGraph V), G.chromaticNumber = ⊤ ∧
∀ n, G.maxSubgraphEdgeDistToBipartite n ≤ f n) := ⊢ True ↔
∀ (f : ℕ → ℕ),
Tendsto f atTop atTop → ∃ V G, χ(G) = ⊤ ∧ ∀ (n : ℕ), SimpleGraph.maxSubgraphEdgeDistToBipartite G n ≤ f n
All goals completed! 🐙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?
@[category research open, AMS 5]
theorem erdos_74.variants.sqrt : answer(sorry) ↔
∃ (V : Type u) (G : SimpleGraph V), G.chromaticNumber = ⊤ ∧
∀ n, G.maxSubgraphEdgeDistToBipartite n ≤ (n : ℝ).sqrt := ⊢ True ↔ ∃ V G, χ(G) = ⊤ ∧ ∀ (n : ℕ), ↑(SimpleGraph.maxSubgraphEdgeDistToBipartite G n) ≤ √↑n
All goals completed! 🐙-- TODO(firsching): add the remaining statements/comments
end Erdos74