Homogeneous sets of large logarithmic weight

DefinitionErdős Problem 191#✓fully proved

The statement that for every real \(C > 0\) there is an \(N\) such that for every \(n \ge N\) and every graph \(G\) on the natural numbers (its edges and non-edges 2-colour the pairs of \(\{2, \dots, n\}\)) there is a finite set \(X \subseteq \{2, \dots, n\}\) that is a clique or an independent set of \(G\) (a monochromatic set) with \(\sum_{x \in X} 1 / \log x \ge C\).

def homogeneousSetLargeLogWeight : Prop :=
  ∀ C : ℝ, 0 < C → ∀ᶠ n : ℕ in atTop, ∀ G : SimpleGraph ℕ, ∃ X : Finset ℕ,
    X ⊆ Finset.Icc 2 n ∧ (G.IsClique (X : Set ℕ) ∨ G.IsIndepSet (X : Set ℕ)) ∧
      C ≤ ∑ x ∈ X, 1 / Real.log x

Used by 1

Used byMonochromatic sets of large logarithmic weight exist

TheoremMonochromatic sets of large logarithmic weight exist#●ready to prove

For every real \(C > 0\) there is an \(N\) such that for every \(n \ge N\) and every graph \(G\) on the natural numbers there is a finite set \(X \subseteq \{2, \dots, n\}\) that is a clique or an independent set of \(G\) and satisfies \(\sum_{x \in X} 1 / \log x \ge C\).

Rödl proved this, and Conlon, Fox and Sudakov later showed that the best such \(X\) has weight at least \(2^{-8} \log \log \log n\) for large \(n\), which is sharp by Rödl's construction.

public theorem_wanted homogeneousSetLargeLogWeight_holds : homogeneousSetLargeLogWeight

Sources

• T. F. Bloom, Erdős Problems, Problem #191, https://www.erdosproblems.com/191 (status PROVED (LEAN)); resolution: V. Rödl, On homogeneous sets of positive integers, J. Combin. Theory Ser. A 102 (2003), 229-240, erdosproblems.com/191: proved by Rödl [Ro03]; Conlon, Fox and Sudakov (2013) gave the sharp bound 2^{-8} log log log n, https://doi.org/10.1016/S0097-3165(03)00026-8.

Uses 1

Statement usesErdős Problem 191

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.