Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1970P2

module

public import Mathlib.Tactic

public section


/-!
# International Mathematical Olympiad 1970, Problem 2

Let a, b and n be integers greater than 1, and let a and b be the bases of two
number systems. A_{n-1} and A_n are numbers in the system with base a, and
B_{n-1} and B_n are numbers in the system with base b; these are related as
follows:

  A_n     = x_n x_{n-1} ⋯ x_0,   A_{n-1} = x_{n-1} x_{n-2} ⋯ x_0,
  B_n     = x_n x_{n-1} ⋯ x_0,   B_{n-1} = x_{n-1} x_{n-2} ⋯ x_0,

(written as digit strings in the respective systems) with x_n ≠ 0 and
x_{n-1} ≠ 0.

Prove that A_{n-1}/A_n < B_{n-1}/B_n if and only if a > b.
-/

namespace Imo1970P2

/-- The real number whose base-`c` digit string is `x m, x (m-1), ..., x 0`,
i.e. `∑ i ≤ m, x i * c ^ i`. -/
def value (x : ℕ → ℕ) (c : ℕ) (m : ℕ) : ℝ :=
  ∑ i ∈ Finset.range (m + 1), (x i : ℝ) * (c : ℝ) ^ i

theorem imo1970_p2 (a b n : ℕ) (ha : 1 < a) (hb : 1 < b) (hn : 1 < n) (x : ℕ → ℕ)
    (hdig : ∀ i ≤ n, x i < min a b) (hxn : x n ≠ 0) (hxn1 : x (n - 1) ≠ 0) :
    value x a (n - 1) / value x a n < value x b (n - 1) / value x b n ↔ b < a := sorry

end Imo1970P2

File author(s): Kimi K3

This problem has a complete formalized solution.