Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2014P6

module

public import Mathlib.Algebra.EuclideanDomain.Basic
public import Mathlib.Algebra.EuclideanDomain.Field
public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.Analysis.InnerProductSpace.Basic
public import Mathlib.Analysis.Normed.Order.Lattice
public import Mathlib.Order.CompletePartialOrder

public section


/-!
# International Mathematical Olympiad 2014, Problem 6

A set of lines in the plane is in general position if no two are
parallel and no three pass through the same point. A set of lines in
general position cuts the plane into regions, some of which have finite
area; we call these its finite regions. Prove that for all sufficiently
large n, in any set of n lines in general position it is possible to
colour at least √n lines blue in such a way that none of its finite
regions has a completely blue boundary.
-/

namespace Imo2014P6

/-- A line in the plane `ℝ × ℝ`, given by the equation `a * x + b * y + c = 0`
with `(a, b) ≠ (0, 0)`. -/
structure Line where
  a : ℝ
  b : ℝ
  c : ℝ
  hab : a ≠ 0 ∨ b ≠ 0

noncomputable instance : DecidableEq Line := Classical.decEq _

namespace Line

/-- The affine function whose zero set is the line. -/
def val (ℓ : Line) (p : ℝ × ℝ) : ℝ := ℓ.a * p.1 + ℓ.b * p.2 + ℓ.c

/-- The line as a set of points. -/
def set (ℓ : Line) : Set (ℝ × ℝ) := {p | ℓ.val p = 0}

/-- The determinant of the two normals; nonzero iff the lines are not parallel. -/
def det (ℓ m : Line) : ℝ := ℓ.a * m.b - m.a * ℓ.b

/-- The intersection point of two non-parallel lines. -/
noncomputable def interPt (ℓ m : Line) : ℝ × ℝ :=
  ((ℓ.b * m.c - m.b * ℓ.c) / ℓ.det m, (m.a * ℓ.c - ℓ.a * m.c) / ℓ.det m)

end Line

/-- A set of lines is in *general position* if no two are parallel and no three
pass through the same point. -/
def GeneralPosition (L : Finset Line) : Prop :=
  (∀ ℓ ∈ L, ∀ m ∈ L, ℓ ≠ m → ℓ.det m ≠ 0) ∧
  (∀ ℓ ∈ L, ∀ m ∈ L, ∀ n ∈ L, ℓ ≠ m → ℓ ≠ n → m ≠ n → n.val (ℓ.interPt m) ≠ 0)

/-- The sign `±1` attached to a side of a line. -/
def sgn (b : Bool) : ℝ := if b then 1 else -1

/-- The *cell* of a sign vector `σ`: the set of points lying on the prescribed
side of every line of `L`. The nonempty cells are exactly the regions into which
the lines of `L` cut the plane, and the bounded nonempty cells are its finite
regions. -/
def Cell (L : Finset Line) (σ : Line → Bool) : Set (ℝ × ℝ) :=
  {p | ∀ ℓ ∈ L, sgn (σ ℓ) * ℓ.val p > 0}

theorem imo2014_p6 :
    ∃ N : ℕ, ∀ n ≥ N, ∀ L : Finset Line, L.card = n → GeneralPosition L →
      ∃ B : Finset Line, B ⊆ L ∧ Real.sqrt n ≤ B.card ∧
        ∀ σ : Line → Bool, (Cell L σ).Nonempty → Bornology.IsBounded (Cell L σ) →
          ¬ (frontier (Cell L σ) ⊆ ⋃ ℓ ∈ B, ℓ.set) := sorry

end Imo2014P6

File author(s): Kimi K3

This problem has a complete formalized solution.