Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1973P6

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1973, Problem 6

Let $a_1, a_2,\cdots, a_n$ be $n$ positive numbers,
and let $q$ be a given real number such that $0 < q < 1$. Find $n$ numbers $b_1, b_2, \cdots, b_n$ for which

(a) $a_k < b_k$ for $k=1,2,\cdots, n$,

(b) $q < \dfrac{b_{k+1}}{b_k}<\dfrac{1}{q}$ for $k=1,2,\cdots,n-1$,

(c) $b_1+b_2+\cdots+b_n < \dfrac{1+q}{1-q}(a_1+a_2+\cdots+a_n)$.

-/

namespace Imo1973P6

variable (n : ℕ) (a : Fin n → ℝ) (q : ℝ)


theorem imo1973_p6 (npos : 0 < n) (hq : q ∈ Set.Ioo 0 1) (apos : ∀ i, 0 < a i)
    : ∃ b : Fin n → ℝ,
      (∀ k, a k < b k)
    ∧ (∀ k, ∀ _ : k < n-1, (b ⟨k+1, by lia⟩) / (b ⟨k, by lia⟩) ∈ Set.Ioo q (1 / q))
    ∧ (∑ k, b k < (1+q) / (1-q) * ∑ k, a k) := sorry



end Imo1973P6

File author(s): Constantin Seebach

This problem has a complete formalized solution.