Point–line incidences

DefinitionLine sizes of a planar point set#✓fully proved

For a finite set \(P \subseteq \mathbb{R}^2\), this is the multiset of the numbers \(|\ell \cap P|\), where \(\ell\) ranges over the lines determined by \(P\), that is, the distinct lines through two distinct points of \(P\), each counted once.

noncomputable def lineSizes (P : Finset (ℝ × ℝ)) : Multiset ℕ :=
  ((P.offDiag.image fun pq => line[ℝ, pq.1, pq.2]).val.map fun ℓ =>
    (P.filter fun r => r ∈ ℓ).card)

Used by 1

Used byNumber of line-compatible sequences

DefinitionNumber of line-compatible sequences#✓fully proved

For a natural number \(n\), \(f(n)\) is the number of distinct multisets that arise as the line sizes of some \(n\)-point set \(P \subseteq \mathbb{R}^2\), that is, as the multiset of the numbers \(|\ell \cap P|\) over the distinct lines \(\ell\) through two distinct points of \(P\), each line counted once. These multisets are the line-compatible sequences for \(n\); there are finitely many, since each has at most \(n^2\) entries, all at most \(n\).

noncomputable def lineCompatibleCount (n : ℕ) : ℕ :=
  {X : Multiset ℕ | ∃ P : Finset (ℝ × ℝ), P.card = n ∧ lineSizes P = X}.ncard

Uses 1 · Used by 1

Statement usesLine sizes of a planar point set

Used bySubexponential count of line-compatible sequences (statement)

DefinitionSubexponential count of line-compatible sequences (statement)#✓fully proved

The proposition that there is a real constant \(C\) such that for every natural number \(n\), the number \(f(n)\) of line-compatible sequences for \(n\) is at most \(e^{C \sqrt{n}}\); that is, there are at most \(\exp(O(\sqrt{n}))\) line-compatible sequences. This is Erdős Problem 733.

def lineCompatibleCountSubexponential : Prop :=
  ∃ C : ℝ, ∀ n : ℕ, (lineCompatibleCount n : ℝ) ≤ Real.exp (C * Real.sqrt n)

Uses 1 · Used by 1

Statement usesNumber of line-compatible sequences

Used bySzemerédi–Trotter bound on line-compatible sequences

TheoremSzemerédi–Trotter bound on line-compatible sequences#●ready to prove

There is a real constant \(C\) such that for every natural number \(n\), the number of line-compatible sequences for \(n\), that is, of distinct multisets of the numbers \(|\ell \cap P|\) over the distinct lines \(\ell\) through two distinct points of an \(n\)-point set \(P \subseteq \mathbb{R}^2\), each line counted once, is at most \(e^{C \sqrt{n}}\). This answers Erdős Problem 733.

public theorem_wanted lineCompatibleCountSubexponential_holds : lineCompatibleCountSubexponential

Sources

• T. F. Bloom, Erdős Problems, Problem #733, https://www.erdosproblems.com/733 (status PROVED); resolution: E. Szemerédi and W. T. Trotter, Extremal problems in discrete geometry, Combinatorica 3 (1983), 381-392, erdosproblems.com/733: 'This is true, and was proved by Szemerédi and Trotter', https://doi.org/10.1007/BF02579194.

Uses 1

Statement usesSubexponential count of line-compatible sequences (statement)

DefinitionLine-incidence set of a finite planar point set#✓fully proved

For a finite set \(P \subseteq \mathbb{R}^2\), \(A(P)\) is the set of the numbers \(|\ell \cap P|\) over the lines \(\ell\) determined by \(P\), that is, the lines through at least two distinct points of \(P\).

noncomputable def lineIncidenceSet (P : Finset (ℝ × ℝ)) : Finset ℕ :=
  P.offDiag.image fun pq => (P.filter fun r => r ∈ line[ℝ, pq.1, pq.2]).card

Used by 1

Used byNumber of line-incidence sets

DefinitionNumber of line-incidence sets#✓fully proved

For a finite set \(P \subseteq \mathbb{R}^2\), let \(A(P)\) be the set of the numbers \(|\ell \cap P|\) over the lines \(\ell\) through at least two distinct points of \(P\). For a natural number \(n\), \(F(n)\) is the number of distinct sets \(A(P)\) over all \(n\)-point sets \(P \subseteq \mathbb{R}^2\). Every such \(A(P)\) is a subset of \(\{0, \dots, n\}\).

noncomputable def lineIncidenceSetCount (n : ℕ) : ℕ :=
  ((Finset.range (n + 1)).powerset.filter fun A =>
    ∃ P : Finset (ℝ × ℝ), P.card = n ∧ lineIncidenceSet P = A).card

Uses 1 · Used by 1

Statement usesLine-incidence set of a finite planar point set

Used byErdős Problem 607: subexponentially many line-incidence sets

DefinitionErdős Problem 607: subexponentially many line-incidence sets#✓fully proved

For a finite set \(P \subseteq \mathbb{R}^2\), let \(A(P)\) be the set of the numbers \(|\ell \cap P|\) over the lines \(\ell\) through at least two distinct points of \(P\), and let \(F(n)\) be the number of distinct sets \(A(P)\) over all \(n\)-point sets \(P \subseteq \mathbb{R}^2\). This is the statement that there is a real constant \(C\) such that \(F(n) \le e^{C\sqrt{n}}\) for every natural number \(n\), that is, \(F(n) \le \exp(O(\sqrt{n}))\).

def lineIncidenceSetCountSubexponential : Prop :=
  ∃ C : ℝ, ∀ n : ℕ, (lineIncidenceSetCount n : ℝ) ≤ Real.exp (C * Real.sqrt n)

Uses 1 · Used by 1

Statement usesNumber of line-incidence sets

Used bySzemerédi–Trotter bound for line-incidence sets (Erdős Problem 607)

TheoremSzemerédi–Trotter bound for line-incidence sets (Erdős Problem 607)#●ready to prove

For a finite set \(P \subseteq \mathbb{R}^2\), let \(A(P)\) be the set of the numbers \(|\ell \cap P|\) over the lines \(\ell\) through at least two distinct points of \(P\), and let \(F(n)\) be the number of distinct sets \(A(P)\) over all \(n\)-point sets \(P \subseteq \mathbb{R}^2\). There is a real constant \(C\) such that \(F(n) \le e^{C\sqrt{n}}\) for every natural number \(n\).

public theorem_wanted lineIncidenceSetCountSubexponential_holds :
    lineIncidenceSetCountSubexponential

Sources

• T. F. Bloom, Erdős Problems, Problem #607, https://www.erdosproblems.com/607 (status PROVED); resolution: E. Szemerédi and W. T. Trotter, Extremal problems in discrete geometry, Combinatorica 3 (1983), 381-392, erdosproblems.com/607: proved by Szemerédi and Trotter [SzTr83], https://doi.org/10.1007/BF02579194.

Uses 1

Statement usesErdős Problem 607: subexponentially many line-incidence sets

6 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.