Erdős Problem 184

References:

• erdosproblems.com/184
• [BM22] Bucić, M. and Montgomery, R., Towards the Erdős-Gallai Cycle Decomposition Conjecture. arXiv:2211.07689 (2022).
• [CFS14] Conlon, David and Fox, Jacob and Sudakov, Benny, Cycle packing. Random Structures Algorithms (2014), 608-626.
• [EGP66] Erdős, Paul and Goodman, A. W. and Pósa, Lajos, The representation of a graph by set intersections. Canadian J. Math. (1966), 106-112.
• [Er71] Erdős, P., Some unsolved problems in graph theory and combinatorial analysis. Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97-109.

def Erdos184.IsCycleOrEdge {U : Type u_1} [Fintype U] (H : SimpleGraph U) : Prop

A graph $H$ is a cycle or an edge if it is connected and 2-regular, or if it has exactly one edge.

Equations

• Erdos184.IsCycleOrEdge H = (H.Connected ∧ H.IsRegularOfDegree 2 ∨ H.edgeFinset.card = 1)

def Erdos184.IsDecomposition {V : Type u_1} (G : SimpleGraph V) (D : Finset G.Subgraph) : Prop

D is a decomposition of G into subgraphs.

Equations

• Erdos184.IsDecomposition G D = (((↑D).PairwiseDisjoint fun (H : G.Subgraph) => H.edgeSet) ∧ ⋃ H ∈ D, H.edgeSet = G.edgeSet)

theorem Erdos184.erdos_184 : ∃ (f : ℕ → ℝ), (f =O[Filter.atTop] fun (n : ℕ) => ↑n) ∧ ∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V), ∃ (D : Finset G.Subgraph), (∀ H ∈ D, IsCycleOrEdge H.coe) ∧ IsDecomposition G D ∧ ↑D.card ≤ f (Fintype.card V)

Any graph on $n$ vertices can be decomposed into $O(n)$ many edge-disjoint cycles and edges.

theorem Erdos184.erdos_184.variants.n_log_n : ∃ (f : ℕ → ℝ), (f =O[Filter.atTop] fun (n : ℕ) => ↑n * Real.log ↑n) ∧ ∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V), ∃ (D : Finset G.Subgraph), (∀ H ∈ D, IsCycleOrEdge H.coe) ∧ IsDecomposition G D ∧ ↑D.card ≤ f (Fintype.card V)

Erdős and Gallai [EGP66] proved that $O(n \log n)$ many cycles and edges suffices.

theorem Erdos184.erdos_184.variants.lower_bound : ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, have G := SimpleGraph.fromRel fun (i j : Fin n) => ↑i < 3 ∧ 3 ≤ ↑j; ∀ (D : Finset G.Subgraph), (∀ H ∈ D, IsCycleOrEdge H.coe) → IsDecomposition G D → (1 + c) * ↑n ≤ ↑D.card

The graph $K_{3,n-3}$ shows that at least $(1+c)n$ many cycles and edges are required, for some constant $c>0$.

theorem Erdos184.erdos_184.variants.covering : True ↔ ∀ {V : Type} [inst : Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V), ∃ (D : Finset G.Subgraph), (∀ H ∈ D, IsCycleOrEdge H.coe) ∧ ⋃ H ∈ D, H.edgeSet = G.edgeSet ∧ ↑D.card ≤ ↑(Fintype.card V) - 1

In [Er71] Erdős suggests that only $n-1$ many cycles and edges are required if we do not require them to be edge-disjoint.

theorem Erdos184.erdos_184.variants.bucic_montgomery : ∃ (f : ℕ → ℝ), (f =O[Filter.atTop] fun (n : ℕ) => ↑n * ↑(↑n).iteratedLog) ∧ ∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V), ∃ (D : Finset G.Subgraph), (∀ H ∈ D, IsCycleOrEdge H.coe) ∧ IsDecomposition G D ∧ ↑D.card ≤ f (Fintype.card V)

The best bound available is due to Bucić and Montgomery [BM22], who prove that $O(n\log^* n)$ many cycles and edges suffice, where $\log^*$ is the iterated logarithm function.

theorem Erdos184.erdos_184.variants.conlon_fox_sudakov (ε : ℝ) : ε > 0 → ∃ (f : ℕ → ℝ), (f =O[Filter.atTop] fun (n : ℕ) => ↑n) ∧ ∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V), ↑G.minDegree ≥ ε * ↑(Fintype.card V) → ∃ (D : Finset G.Subgraph), (∀ H ∈ D, IsCycleOrEdge H.coe) ∧ IsDecomposition G D ∧ ↑D.card ≤ f (Fintype.card V)

Conlon, Fox, and Sudakov [CFS14] proved that $O_\epsilon(n)$ cycles and edges suffice if $G$ has minimum degree at least $\epsilon n$, for any $\epsilon>0$.