Degrees in 3-chromatic hypergraphs
DefinitionErdős Problem 833#✓fully proved
The statement that there is a real \(c > 0\) such that for every natural number \(r \ge 2\), every \(n\) and every hypergraph \(H\) on the vertex set \(\{0, \dots, n-1\}\) (a finite set of edges, each a set of exactly \(r\) vertices) that is \(3\)-colorable but not \(2\)-colorable, some vertex lies in at least \((1 + c)^r\) edges of \(H\).
def threeChromaticHighDegreeVertex : Prop :=
∃ c : ℝ, 0 < c ∧ ∀ r : ℕ, 2 ≤ r → ∀ (n : ℕ) (H : Finset (Finset (Fin n))),
(∀ e ∈ H, e.card = r) → HypergraphColorable H 3 → ¬ HypergraphColorable H 2 →
∃ v : Fin n, (1 + c) ^ r ≤ ((H.filter fun e => v ∈ e).card : ℝ)def HypergraphColorable {n : ℕ} (H : Finset (Finset (Fin n))) (k : ℕ) : Prop :=
∃ c : Fin n → Fin k, ∀ e ∈ H, ∃ u ∈ e, ∃ v ∈ e, c u ≠ c vWantedExt/Combinatorics/HypergraphColoringShared.lean:27
Uses 1 · Used by 1
TheoremErdős Problem 833 holds#●ready to prove
There is a real \(c > 0\) such that for every natural number \(r \ge 2\), every \(n\) and every hypergraph \(H\) on the vertex set \(\{0, \dots, n-1\}\) (a finite set of edges, each a set of exactly \(r\) vertices) that is \(3\)-colorable but not \(2\)-colorable, some vertex lies in at least \((1 + c)^r\) edges of \(H\).
Erdős and Lovász proved that every \(r\)-uniform hypergraph with chromatic number \(3\) has a vertex in at least \(2^{r-1} / (4r)\) edges (Theorem 2 with \(k = 2\)), which exceeds \((1 + c)^r\) for a small absolute \(c\) once \(r\) is large, while for every \(r\) some vertex lies in two edges (pairwise disjoint edges can be \(2\)-colored).
public theorem_wanted threeChromaticHighDegreeVertex_holds : threeChromaticHighDegreeVertexdef threeChromaticHighDegreeVertex : Prop :=
∃ c : ℝ, 0 < c ∧ ∀ r : ℕ, 2 ≤ r → ∀ (n : ℕ) (H : Finset (Finset (Fin n))),
(∀ e ∈ H, e.card = r) → HypergraphColorable H 3 → ¬ HypergraphColorable H 2 →
∃ v : Fin n, (1 + c) ^ r ≤ ((H.filter fun e => v ∈ e).card : ℝ)WantedExt/Combinatorics/ThreeChromaticHypergraphDegreeErdosProblem833Wanted.lean:42
Sources
- T. F. Bloom, Erdős Problems, Problem #833, https://www.erdosproblems.com/833 (status PROVED); resolution: P. Erdős and L. Lovász, Problems and results on 3-chromatic hypergraphs and some related questions, Infinite and finite sets (Colloq. Keszthely, 1973), Colloq. Math. Soc. János Bolyai 10 (1975), 609-627, Theorem 2: a (k + 1)-chromatic r-uniform hypergraph has an edge meeting at least k^{r-1}/4 other edges, so some vertex has degree at least k^{r-1}/(4r); for k = 2 this is 2^{r-1}/(4r), https://users.renyi.hu/~p_erdos/1975-34.pdf.
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.