Convex and general position of point sets

DefinitionRelation holding triplewise on a set#✓fully proved

Let \(r\) be a ternary relation on a type \(\alpha\) and let \(s \subseteq \alpha\). The relation \(r\) holds triplewise on \(s\) if \(r(x, y, z)\) holds for all pairwise distinct \(x, y, z \in s\).

protected def Triplewise (s : Set α) (r : α → α → α → Prop) : Prop :=
  ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃z⦄, z ∈ s → x ≠ y → y ≠ z → x ≠ z → r x y z

Used by 2

Used byIsosceles-free sets · Sets with no three collinear points

DefinitionSets with no three collinear points#✓fully proved

A set \(A\) of points in the plane is non-trilinear if no three distinct points of \(A\) lie on a common line.

def NonTrilinear (A : Set P) : Prop :=
  A.Triplewise (fun x y z ↦ ¬ Collinear ℝ {x, y, z})

Uses 1 · Used by 1

Statement usesRelation holding triplewise on a set

Used byPoints in general position

DefinitionSets with no \(n\) collinear points#✓fully proved

A set \(S\) of points in a Euclidean affine space has no \(n\) collinear points if no subset of \(S\) consisting of exactly \(n\) points is collinear.

def NonCollinearFor (n : ℕ) (S : Set P) : Prop :=
  ∀ (A : Set P), A ⊆ S → A.Finite → A.ncard = n → ¬ Collinear ℝ A

DefinitionSets containing a convex \(n\)-gon#✓fully proved

A set \(P \subseteq \mathbb{R}^2\) contains a convex \(n\)-gon if there is a set \(S \subseteq P\) of exactly \(n\) points that is convex independent: no point of \(S\) lies in the convex hull of the other points of \(S\).

def HasConvexNGon (n : ℕ) (P : Set ℝ²) : Prop :=
  ∃ S : Finset ℝ², S.card = n ∧ ↑S ⊆ P ∧
    ConvexIndependent ℝ (fun x : (↑S : Set ℝ²) => (x : ℝ²))

DefinitionCounterclockwise convex polygons#✓fully proved

Let \(P\) be an oriented two-dimensional Euclidean affine space. Points \(p_0, \dots, p_{n-1} \in P\) form a counterclockwise convex polygon if for all indices \(i < j < k\) the oriented angle \(\measuredangle p_i p_j p_k\) at \(p_j\) has sign \(-1\), that is, \(p_i, p_j, p_k\) are not collinear and lie in counterclockwise order with respect to the orientation of \(P\). Every list of at most two points qualifies.

def IsCcwConvexPolygon (p : Fin n → P) : Prop :=
  ∀ ⦃i j k⦄, i < j → j < k → (∡ (p i) (p j) (p k)).sign = -1

Used by 3

Used byConvex polygons · Affinely independent triples are convex polygons · Isosceles trapezoids

DefinitionConvex polygons#✓fully proved

Points \(p_0, \dots, p_{n-1}\) of an oriented two-dimensional Euclidean affine space form a convex polygon if one of the lists \(p_0, p_1, \dots, p_{n-1}\) and \(p_0, p_{n-1}, p_{n-2}, \dots, p_1\) is a counterclockwise convex polygon: for any three of its entries \(q, r, s\), in the order in which they occur in that list, the oriented angle \(\measuredangle q r s\) at \(r\) has sign \(-1\). Thus for \(n \ge 3\) the points are the vertices of a strictly convex polygon, listed counterclockwise or clockwise starting from \(p_0\); every list of at most two points qualifies.

def IsConvexPolygon {n : ℕ} (p : Fin n → P) : Prop :=
  IsCcwConvexPolygon p ∨ IsCcwConvexPolygon fun i => p (-i)

Uses 1 · Used by 1

Statement usesCounterclockwise convex polygons

Used byAffinely independent triples are convex polygons

TheoremAffinely independent triples are convex polygons#✓fully proved

If three points \(A, B, C\) of an oriented two-dimensional Euclidean affine space are affinely independent, then \(A, B, C\) form a convex polygon.

theorem isConvexPolygon_three_of_affineIndependent {A B C : P}
    (hABC : AffineIndependent ℝ ![A, B, C]) : IsConvexPolygon ![A, B, C]

Uses 2

Statement usesConvex polygons

Proof usesCounterclockwise convex polygons

DefinitionOriented triangle area#✓fully proved

Let \(\omega\) be the area form of the given orientation of the Euclidean plane, so that \(\omega(u, v)\) is the signed area of the parallelogram spanned by the vectors \(u\) and \(v\). For points \(a\), \(b\), \(c\) of the plane, the oriented area of the triangle with vertices \(a\), \(b\), \(c\) is the real number \(\omega(a - c, b - c) / 2\).

It changes sign when two vertices are swapped, and it is positive when \(a\), \(b\), \(c\) are in counterclockwise order and negative when they are in clockwise order.

noncomputable def orientedTriangleArea (a b c : P) : ℝ :=
  positiveOrientation.areaForm (a -ᵥ c) (b -ᵥ c) / 2

Used by 1

Used byVarignon's theorem

DefinitionMaximum number of distinct distance counts#✓fully proved

For a finite set \(X \subseteq \mathbb{R}^2\) and a point \(x \in X\), let \(R_X(x)\) be the number of distinct distances \(\lvert y - x \rvert\) from \(x\) to the points \(y \in X\) other than \(x\). For \(n \in \mathbb{N}\), \(g(n)\) is the maximum, over all sets \(X \subseteq \mathbb{R}^2\) of exactly \(n\) points, of the number of distinct values among the numbers \(R_X(x)\) with \(x \in X\).

noncomputable def maximalDistinctDistancesFrom (n : ℕ) : ℕ :=
  sSup {#(X.image (distinctDistancesFrom X)) | (X : Finset ℝ²) (_ : #X = n)}

Uses 1

Statement usesNumber of distinct distances from a point

DefinitionPoints in general position#✓fully proved

A set \(X \subseteq \mathbb{R}^2\), finite or infinite, is in general position if no three distinct points of \(X\) are collinear and no four distinct points of \(X\) lie on a common circle.

def InGeneralPosition (X : Set ℝ²) : Prop :=
  NonTrilinear X ∧ ∀ T ⊆ X, T.ncard = 4 → ¬Cospherical T

Uses 1

Statement usesSets with no three collinear points

DefinitionRight-angled triangles#✓fully proved

Points \(a, b, c\) of a Euclidean affine space are the vertices of a right-angled triangle if they are pairwise distinct and the unoriented angle at one of the three vertices equals \(\pi / 2\): \(\angle bac = \pi / 2\), \(\angle abc = \pi / 2\) or \(\angle bca = \pi / 2\).

The distinctness hypothesis rules out degenerate triples, whose angles can coincide with \(\pi / 2\).

def IsRightAngled (a b c : P) : Prop :=
  a ≠ b ∧ a ≠ c ∧ b ≠ c ∧
    (∠ b a c = π / 2 ∨ ∠ a b c = π / 2 ∨ ∠ b c a = π / 2)

DefinitionIsosceles trapezoids#✓fully proved

Points \(a, b, c, d \in \mathbb{R}^2\) are the vertices, in counterclockwise order, of an isosceles trapezoid if they are in strictly convex position and listed counterclockwise (for any three of them \(p, q, r\), in the order in which they occur in the list \(a, b, c, d\), the oriented angle \(\measuredangle p q r\) at \(q\) has sign \(-1\)), the line through \(a\) and \(b\) is parallel to the line through \(c\) and \(d\) (the two bases), and the diagonals have equal length: \(\operatorname{dist}(a, c) = \operatorname{dist}(b, d)\).

One pair of parallel sides together with equal diagonals is the classical characterization of an isosceles trapezoid; in particular it rules out non-rectangular parallelograms.

def IsIsoscelesTrapezoid (a b c d : ℝ²) : Prop :=
  IsCcwConvexPolygon ![a, b, c, d] ∧
  (affineSpan ℝ {a, b}).Parallel (affineSpan ℝ {c, d}) ∧
  dist a c = dist b d

Uses 1

Statement usesCounterclockwise convex polygons

DefinitionIsosceles-free sets#✓fully proved

A set \(A\) in a space with a distance function \(d\) is isosceles-free if there are no three distinct points \(x, y, z \in A\) such that two of the distances \(d(x, y)\), \(d(y, z)\), \(d(z, x)\) are equal.

def Set.IsIsoscelesFree {α : Type*} [Dist α] (A : Set α) : Prop :=
  A.Triplewise fun x y z ↦ ¬ _root_.IsIsosceles x y z

Uses 1

Statement usesRelation holding triplewise on a set

DefinitionGeneral position of affine points#✓fully proved

Let \(k\) be a division ring and \(P\) an affine space over \(k\). A family \((p_i)_{i \in \iota}\) of points of \(P\) is in general position through dimension \(d \in \mathbb{N}\) if for every finite set \(S \subseteq \iota\) of at most \(d + 1\) indices, the subfamily \((p_i)_{i \in S}\) is affinely independent over \(k\).

def IsGeneralPosition (k : Type u) [DivisionRing k] {V : Type v} {P : Type w} [AddCommGroup V]
    [Module k V] [AffineSpace V P] {ι : Type*} (d : ℕ) (p : ι → P) : Prop :=
  ∀ s : Finset ι, s.card ≤ d + 1 → AffineIndependent k (s.restrict p)

Used by 3

Used byConvex position threshold · Affinely independent families are in general position · General position in affine space is monotone in the dimension

TheoremAffinely independent families are in general position#✓fully proved

If a family \((p_i)_{i \in \iota}\) of points of an affine space over a division ring \(k\) is affinely independent over \(k\), then it is in general position through dimension \(d\) for every \(d \in \mathbb{N}\).

theorem AffineIndependent.isGeneralPosition {p : ι → P} (hp : AffineIndependent k p) (d : ℕ) :
    IsGeneralPosition k d p

Uses 1

Statement usesGeneral position of affine points

TheoremGeneral position in affine space is monotone in the dimension#✓fully proved

Let \(d \le e\) be natural numbers. If a family of points of an affine space over a division ring \(k\) is in general position through dimension \(e\), then it is in general position through dimension \(d\).

theorem IsGeneralPosition.mono {d e : ℕ} {p : ι → P} (hp : IsGeneralPosition k e p)
    (hde : d ≤ e) : IsGeneralPosition k d p

Uses 1

Statement usesGeneral position of affine points

DefinitionGeneral position of projective points#✓fully proved

Let \(k\) be a division ring and \(V\) a vector space over \(k\), with projective space \(\mathbb{P}(V)\). A family \((p_i)_{i \in \iota}\) of points of \(\mathbb{P}(V)\) is in general position through dimension \(d \in \mathbb{N}\) if for every finite set \(S \subseteq \iota\) of at most \(d + 1\) indices, the subfamily \((p_i)_{i \in S}\) is projectively independent.

def IsGeneralPosition {k : Type u} [DivisionRing k] {V : Type v} [AddCommGroup V] [Module k V]
    {ι : Type*} (d : ℕ) (p : ι → ℙ k V) : Prop :=
  ∀ s : Finset ι, s.card ≤ d + 1 → Independent (s.restrict p)

Used by 2

Used byProjectively independent families are in general position · General position in projective space is monotone in the dimension

TheoremProjectively independent families are in general position#✓fully proved

If a family \((p_i)_{i \in \iota}\) of points of the projective space \(\mathbb{P}(V)\) of a vector space \(V\) over a division ring \(k\) is projectively independent, then it is in general position through dimension \(d\) for every \(d \in \mathbb{N}\).

theorem Independent.isGeneralPosition {p : ι → ℙ k V} (hp : Independent p) (d : ℕ) :
    IsGeneralPosition d p

Uses 1

Statement usesGeneral position of projective points

TheoremGeneral position in projective space is monotone in the dimension#✓fully proved

Let \(d \le e\) be natural numbers. If a family of points of the projective space \(\mathbb{P}(V)\) of a vector space \(V\) over a division ring \(k\) is in general position through dimension \(e\), then it is in general position through dimension \(d\).

theorem IsGeneralPosition.mono {d e : ℕ} {p : ι → ℙ k V} (hp : IsGeneralPosition e p)
    (hde : d ≤ e) : IsGeneralPosition d p

Uses 1

Statement usesGeneral position of projective points

DefinitionConvex position threshold#✓fully proved

For natural numbers \(k\) and \(n\), \(f_k(n)\) is the least natural number \(m\) such that every set of \(m\) points of \(\mathbb{R}^k\) in general position (any at most \(k + 1\) of them affinely independent) contains \(n\) points in convex position (none of them in the convex hull of the others). If there is no such \(m\), then \(f_k(n) = 0\).

For \(k \ge 2\) such an \(m\) exists by the Erdős-Szekeres theorem.

noncomputable def convexPositionThreshold (k n : ℕ) : ℕ :=
  sInf {m | ∀ P : Finset (EuclideanSpace ℝ (Fin k)), P.card = m →
    IsGeneralPosition ℝ k ((↑) : P → EuclideanSpace ℝ (Fin k)) →
    ∃ S ⊆ P, S.card = n ∧ ConvexIndependent ℝ ((↑) : S → EuclideanSpace ℝ (Fin k))}

Uses 1 · Used by 1

Statement usesGeneral position of affine points

Used byErdős Problem 651: exponential growth of convex position thresholds

DefinitionErdős Problem 651: exponential growth of convex position thresholds#✓fully proved

For natural numbers \(k\) and \(n\) let \(f_k(n)\) be the least \(m\) such that every set of \(m\) points of \(\mathbb{R}^k\) in general position (any at most \(k + 1\) of them affinely independent) contains \(n\) points in convex position (none of them in the convex hull of the others), with \(f_k(n) = 0\) if there is no such \(m\). The claim is that for every \(k \ge 2\) there is a real \(c > 0\) with \((1 + c)^n < f_k(n)\) for all sufficiently large \(n\).

Erdős asked for a constant \(c_k > 0\) with \(f_k(n) > (1 + c_k)^n\); requiring this only for all large \(n\) makes the claim weaker and its refutation stronger.

def convexPositionThresholdExponential : Prop :=
  ∀ k : ℕ, 2 ≤ k → ∃ c > (0 : ℝ), ∀ᶠ n : ℕ in Filter.atTop,
    (1 + c) ^ n < (convexPositionThreshold k n : ℝ)

Uses 1 · Used by 1

Statement usesConvex position threshold

Used byErdős Problem 651 has a negative answer

TheoremErdős Problem 651 has a negative answer#●ready to prove

For natural numbers \(k\) and \(n\) let \(f_k(n)\) be the least \(m\) such that every set of \(m\) points of \(\mathbb{R}^k\) in general position (any at most \(k + 1\) of them affinely independent) contains \(n\) points in convex position (none of them in the convex hull of the others), with \(f_k(n) = 0\) if there is no such \(m\). It is not the case that for every \(k \ge 2\) there is a real \(c > 0\) with \((1 + c)^n < f_k(n)\) for all sufficiently large \(n\).

Pohoata and Zakharov proved \(f_d(n) = 2^{o(n)}\) for every \(d \ge 3\), so for \(k = 3\) and every \(c > 0\) the bound \(f_3(n) \le (1 + c)^n\) holds for all large \(n\); erdosproblems.com/651 lists the problem as disproved.

public theorem_wanted convexPositionThresholdExponential_refuted :
    ¬ convexPositionThresholdExponential

Sources

• T. F. Bloom, Erdős Problems, Problem #651, https://www.erdosproblems.com/651 (status DISPROVED (LEAN)); resolution: C. Pohoata and D. Zakharov, Convex polytopes from fewer points, arXiv:2208.04878 (2022), abstract: ES_d(n) = 2^{o(n)} for all d ≥ 3, ES_d(n) being the least number such that any ES_d(n) points in general position in ℝ^d contain n points in convex position; erdosproblems.com/651: the answer is no, even for k = 3, https://arxiv.org/abs/2208.04878.

Uses 1

Statement usesErdős Problem 651: exponential growth of convex position thresholds

21 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.