IMO 2019 Q4 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Find all pairs (k, n) of positive integers such that

  k! = (2 ^ n - 1)(2 ^ n - 2)(2 ^ n - 4)···(2 ^ n - 2 ^ (n - 1))

We show in this file that this property holds iff (k, n) = (1, 1) ∨ (k, n) = (3, 2).

Proof sketch: The idea of the proof is to count the factors of 2 on both sides. The LHS has less than k factors of 2, and the RHS has exactly n * (n - 1) / 2 factors of 2. So we know that n * (n - 1) / 2 < k. Now for n ≥ 6 we have RHS < 2 ^ (n ^ 2) < (n(n-1)/2)! < k!. We then treat the cases n < 6 individually.

source

theorem imo2019_q4.upper_bound {k n : ℕ} (hk : k > 0) (h : ↑(k.factorial) = (finset.range n).prod (λ (i : ℕ), 2 ^ n - 2 ^ i)) :

n < 6

source

theorem imo2019_q4 {k n : ℕ} (hk : k > 0) (hn : n > 0) :

↑(k.factorial) = (finset.range n).prod (λ (i : ℕ), 2 ^ n - 2 ^ i) ↔ (k, n) = (1, 1) ∨ (k, n) = (3, 2)