Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1979P3

module

public import Mathlib.Algebra.Field.ZMod
public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Probability.Distributions.Uniform
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.Positivity.Core
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 1979, Problem 3

$a_1, a_2, \dots, a_n$ is an arbitrary sequence of positive integers. A member of the
sequence is picked at random. Its value is $a$. Another member is picked at random,
independently of the first. Its value is $b$. Then a third, value $c$. Show that the
probability that $a + b + c$ is divisible by $3$ is at least $1 / 4$.
-/

namespace Usa1979P3

open Finset

/-- The residue of `a i` modulo `3`. -/
def res {n : ℕ} (a : Fin n → ℕ) (i : Fin n) : ZMod 3 := (a i : ZMod 3)

/-- The number of entries of `a` having residue `x` modulo `3`. -/
def cnt {n : ℕ} (a : Fin n → ℕ) (x : ZMod 3) : ℕ :=
  (univ.filter fun i ↦ res a i = x).card

/-- The "good" residue patterns: triples of residues that sum to `0`. -/
def patterns : Finset (Fin 3 → ZMod 3) := univ.filter fun u ↦ u 0 + u 1 + u 2 = 0

theorem usa1979_p3 (n : ℕ) [NeZero n] (a : Fin n → ℕ) (ha : ∀ i, 0 < a i) :
    1 / 4 ≤ (PMF.uniformOfFintype (Fin 3 → Fin n)).toOuterMeasure
      {t | 3 ∣ a (t 0) + a (t 1) + a (t 2)} := sorry

end Usa1979P3

File author(s): Kimi K3

This problem has a complete formalized solution.