Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1972P3

import Mathlib.Algebra.BigOperators.Associated
import Mathlib.Probability.Distributions.Uniform

/-!
# USA Mathematical Olympiad 1972, Problem 3

A random number selector can only select one of the nine integers 1, 2, ..., 9,
and it makes these selections with equal probability. Determine the probability
that after n selections, where n > 1, the product of the n numbers selected will
be divisible by 10.
-/

namespace Usa1972P3

abbrev Digit := Fin 9
abbrev DigitSeq (n : ℕ) := Fin n → Digit

noncomputable def unifDistN (n : ℕ) := PMF.uniformOfFintype (DigitSeq n)


def to_nat_digit : Digit → ℕ := fun d ↦ d + 1
def is_good_seq {n : ℕ} (s : DigitSeq n) := 10 ∣ ∏a, to_nat_digit (s a)
def good_seqs {n : ℕ} := {s : DigitSeq n | is_good_seq s}

noncomputable /- determine -/ abbrev solution (n : ℕ) : ENNReal := sorry

theorem usa1972_p3 (n : ℕ) (_hn : 1 < n) :
  (unifDistN n).toOuterMeasure good_seqs = solution n := sorry

end Usa1972P3

File author(s): Shalev Wengrowsky

This problem has a complete formalized solution.