Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2020P6

import Mathlib

/-!
# International Mathematical Olympiad 2020, Problem 6

Consider an integer n > 1, and a set S of n points in the plane
such that the distance between any two points in S is at least 1.
Prove that there is a line l separating S such that the distance
from any point of S to l is at least Ω(n ^ (-1/3)).

(A line l separates a set of points S if some segment jointing
two points in S croses l.)
-/

namespace Imo2020P6

open Finset Module
open scoped RealInnerProductSpace

variable {V P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
variable [NormedAddTorsor V P] (dim : Nat) [Fact (finrank ℝ V = dim + 1)]

variable [Fact (Module.finrank ℝ V = 2)]

theorem imo2020_p6 : ∃ c : ℝ, 0 < c ∧ ∀ {n : ℕ}, 1 < n → ∀ {S : Finset P}, #S = n →
    ((S : Set P).Pairwise fun x y ↦ 1 ≤ dist x y) →
    ∃ l : AffineSubspace ℝ P, finrank ℝ l.direction = 1 ∧
      (∃ p₁ ∈ S, ∃ p₂ ∈ S, l.SOppSide p₁ p₂) ∧
      ∀ p ∈ S, c * (n : ℝ) ^ (-1 / 3 : ℝ) ≤ Metric.infDist p l := sorry

end Imo2020P6

File author(s): Jovan Gerbscheid

This problem has a complete formalized solution.

The solution was imported from mathlib4.