Erdős Problem 501

References:

• erdosproblems.com/501
• [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. 6 (1961), 221-254.
• [ErHa71] Erdős, Paul and Hajnal, András, Unsolved problems in set theory. Axiomatic Set Theory, Proc. Sympos. Pure Math. XIII Part I (1971), 17-48.
• [ErHa60] Erdős, Paul and Hajnal, András. On some combinatorial problems involving complete graphs. Acta Math. Acad. Sci. Hungar. (1960), 395-424.
• [Gl62] Gladysz, S. Some topological properties of independent sets. Colloq. Math. (1962).
• [He72] Hechler, S. H. A dozen small uncountable cardinals. TOPO 72, Lecture Notes in Math. (1972), 207-218.
• [NPS87] Newelski, L., Pawlikowski, J., and Seredyński, F. Infinite independent sets in the closed case. Acta Math. Acad. Sci. Hungar. (1987).

theorem Erdos501.erdos_501 : True ↔ ∀ (A : ℝ → Set ℝ), (∀ (x : ℝ), Bornology.IsBounded (A x)) → (∀ (x : ℝ), MeasureTheory.volume.toOuterMeasure (A x) < 1) → ∃ (X : Set ℝ), X.Infinite ∧ X.Pairwise fun (x y : ℝ) => x ∉ A y

For every $x \in \mathbb{R}$ let $A_x \subset \mathbb{R}$ be a bounded set with outer measure $< 1$. Must there exist an infinite independent set, that is, some infinite $X \subseteq \mathbb{R}$ such that $x \notin A_y$ for all $x \neq y \in X$?

If the sets $A_x$ are closed and have measure $< 1$, then must there exist an independent set of size $3$?

Known results: Erdős–Hajnal [ErHa60] proved the existence of arbitrarily large finite independent sets. Hechler [He72] showed the answer is no assuming the continuum hypothesis.

theorem Erdos501.erdos_501.variants.erdosHajnal_finite : True ↔ ∀ (n : ℕ) (A : ℝ → Set ℝ), (∀ (x : ℝ), Bornology.IsBounded (A x)) → (∀ (x : ℝ), MeasureTheory.volume.toOuterMeasure (A x) < 1) → ∃ (X : Finset ℝ), n ≤ X.card ∧ (↑X).Pairwise fun (x y : ℝ) => x ∉ A y

Erdős–Hajnal (1960): arbitrarily large finite independent sets exist.

For every n : ℕ and every family A : ℝ → Set ℝ of bounded sets with Lebesgue outer measure < 1, there exists a finite independent set of size at least n.

This was proved by Erdős and Hajnal [ErHa60].

theorem Erdos501.erdos_501.variants.hechler_CH : True ↔ Cardinal.aleph 1 = Cardinal.continuum → ∃ (A : ℝ → Set ℝ), (∀ (x : ℝ), Bornology.IsBounded (A x)) ∧ (∀ (x : ℝ), MeasureTheory.volume.toOuterMeasure (A x) < 1) ∧ ¬∃ (X : Set ℝ), X.Infinite ∧ X.Pairwise fun (x y : ℝ) => x ∉ A y

Hechler (1972) [He72]: the answer to the main question is NO, assuming the continuum hypothesis.

Assuming CH (ℵ₁ = 𝔠), there exists a family A : ℝ → Set ℝ of bounded sets with Lebesgue outer measure < 1 for which no infinite independent set exists.

theorem Erdos501.erdos_501.variants.closed_size3 : True ↔ ∀ (A : ℝ → Set ℝ), (∀ (x : ℝ), IsClosed (A x)) → (∀ (x : ℝ), MeasureTheory.volume (A x) < 1) → ∃ (X : Set ℝ), 3 ≤ X.ncard ∧ X.Pairwise fun (x y : ℝ) => x ∉ A y

Closed sets case: existence of an independent set of size 3.

If the sets A x are closed with Lebesgue measure < 1, must there exist an independent set of size 3?

This is implied by the stronger theorem of Newelski–Pawlikowski–Seredyński [NPS87] below; Gladysz [Gl62] earlier proved the existence of an independent set of size 2.

theorem Erdos501.erdos_501.variants.newelski_pawlikowski_seredynski : True ↔ ∀ (A : ℝ → Set ℝ), (∀ (x : ℝ), IsClosed (A x)) → (∀ (x : ℝ), MeasureTheory.volume (A x) < 1) → ∃ (X : Set ℝ), X.Infinite ∧ X.Pairwise fun (x y : ℝ) => x ∉ A y

Newelski–Pawlikowski–Seredyński (1987) [NPS87]: infinite independent set in the closed case.

If all the sets A x are closed with Lebesgue measure < 1, then there is an infinite independent set. This gives a strong affirmative answer to the second question of Problem 501.

theorem Erdos501.erdos_501.variants.gladysz_size2 : True ↔ ∀ (A : ℝ → Set ℝ), (∀ (x : ℝ), IsClosed (A x)) → (∀ (x : ℝ), MeasureTheory.volume (A x) < 1) → ∃ (X : Set ℝ), 2 ≤ X.ncard ∧ X.Pairwise fun (x y : ℝ) => x ∉ A y

Gladysz (1962) [Gl62]: independent set of size 2 in the closed case.

If all the sets A x are closed with Lebesgue measure < 1, then there exist two distinct reals x y such that x ∉ A y and y ∉ A x.

This is a weaker result proved by Gladysz before the full Newelski–Pawlikowski– Seredyński theorem [NPS87].

theorem Erdos501.erdos_501.variants.singleton_independent (A : ℝ → Set ℝ) (x : ℝ) : {x}.Pairwise fun (x y : ℝ) => x ∉ A y

Trivial lower bound: a single-element set is always independent.

For any family A, any singleton {x} is vacuously independent: there are no two distinct elements.

theorem Erdos501.erdos_501.variants.pair_independent_iff (A : ℝ → Set ℝ) {x y : ℝ} (hxy : x ≠ y) : ({x, y}.Pairwise fun (x y : ℝ) => x ∉ A y) ↔ x ∉ A y ∧ y ∉ A x

Two-element sets: independent iff mutual non-membership.

A two-element set {x, y} (with x ≠ y) is independent for A if and only if x ∉ A y and y ∉ A x.

theorem Erdos501.erdos_501.tests.empty_family_is_valid : have A := fun (x : ℝ) => ∅; (∀ (x : ℝ), Bornology.IsBounded (A x)) ∧ (∀ (x : ℝ), MeasureTheory.volume.toOuterMeasure (A x) < 1) ∧ ∃ (X : Set ℝ), X.Infinite ∧ X.Pairwise fun (x y : ℝ) => x ∉ A y

The constant family A x = ∅ satisfies all hypotheses of the main problem: each A x is bounded (the empty set is bounded) and has Lebesgue outer measure 0 < 1. Moreover, all of ℝ is an independent set, showing the conclusion holds trivially.

This demonstrates that the hypotheses are non-vacuous: the family A x = ∅ is a valid input to the theorem, and ℝ (which is infinite) witnesses the conclusion.

theorem Erdos501.erdos_501.tests.singleton_zero_independent (A : ℝ → Set ℝ) : {0}.Pairwise fun (x y : ℝ) => x ∉ A y

A singleton {0} is an independent set for any family A : ℝ → Set ℝ, as witnessed by erdos_501.variants.singleton_independent.

theorem Erdos501.erdos_501.tests.pair_independent_empty : {0, 1}.Pairwise fun (x y : ℝ) => x ∉ (fun (x : ℝ) => ∅) y

Two reals form an independent set for the empty family A _ = ∅: neither 0 nor 1 belongs to ∅, so both conditions of pair_independent_iff hold.

theorem Erdos501.erdos_501.tests.singleton_outer_measure_lt_one (x : ℝ) : MeasureTheory.volume.toOuterMeasure {x} < 1

The hypothesis volume.toOuterMeasure (A x) < 1 is strictly satisfied when A x = {x} (a singleton), since Lebesgue measure of a singleton is 0.

theorem Erdos501.erdos_501.tests.unit_interval_measure : MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) = 1

The boundary case: the measure condition < 1 is sharp. An interval of length ≥ 1 has Lebesgue measure ≥ 1, so it would fail the hypothesis. Here [0, 1] has measure exactly 1.