Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1983P1

module

public import Mathlib.Probability.Distributions.Uniform
public import Mathlib.Tactic.NormNum

public section


/-!
# USA Mathematical Olympiad 1983, Problem 1

If six points are chosen sequentially at random on the circumference of a
circle, what is the probability that the triangle formed by the first three
is disjoint from that formed by the second three?
-/

namespace Usa1983P1

/-- The cyclic order in which the six chosen points appear around the circle:
`σ i` is the position of the `i`-th chosen point among the six positions
`0, …, 5` listed in clockwise order. Only the cyclic order of the six points
matters for this problem, and all `6!` orders are equally likely, so we take
the uniform distribution on `Equiv.Perm (Fin 6)` as the sample space. -/
abbrev Ordering := Equiv.Perm (Fin 6)

/-- The event that the triangle formed by the first three points is disjoint
from the triangle formed by the last three points. With six points on a
circle, the two triangles are disjoint iff the two vertex sets do not
interleave around the circle, which for `3 + 3` points means that the first
three points occupy three (cyclically) consecutive positions. -/
def Favorable (σ : Ordering) : Prop :=
  ∃ k : Fin 6, ({σ 0, σ 1, σ 2} : Finset (Fin 6)) = {k, k + 1, k + 2}

instance : DecidablePred Favorable :=
  fun σ ↦ inferInstanceAs
    (Decidable (∃ k : Fin 6, ({σ 0, σ 1, σ 2} : Finset (Fin 6)) = {k, k + 1, k + 2}))

noncomputable /- determine -/ abbrev solution : ENNReal := sorry

theorem usa1983_p1 :
    (PMF.uniformOfFintype Ordering).toOuterMeasure {σ | Favorable σ} = solution := sorry

end Usa1983P1

File author(s): Kimi K3

This problem has a complete formalized solution.