Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1970P3

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1970, Problem 3

 The real numbers a₀, a₁, a₂, ... satisfy 1 = a₀ ≤ a₁ ≤ a₂ ≤ ... . b₁, b₂, b₃, ... are defined by bₙ = ∑_{k=1}^{n} (1 - a_{k-1}/a_k)/√a_k.

(a)  Prove that 0 ≤ bₙ < 2.

(b)  Given c satisfying 0 ≤ c < 2, prove that we can find an so that bₙ > c for all sufficiently large n.
-/

namespace Imo1970P3


open scoped Real

/-- A sequence of real numbers satisfying the given conditions -/
structure IncreasingSequenceFromOne where
  a : ℕ → ℝ
  a_zero : a 0 = 1
  a_mono : Monotone a

/-- The b_n sequence defined in terms of the a sequence -/
noncomputable def b_seq (seq : IncreasingSequenceFromOne) (n : ℕ) : ℝ :=
  ∑ k ∈ Finset.range n, (1 - seq.a k / seq.a (k + 1)) / √ (seq.a (k + 1))

def ValidBounds : Set ℝ :=
  { b | 0 ≤ b ∧ b < 2 }

theorem imo1970_p3 :
    (∀ seq : IncreasingSequenceFromOne, ∀ n : ℕ, b_seq seq n ∈ ValidBounds) ∧
    (∀ c ∈ ValidBounds, ∃ seq : IncreasingSequenceFromOne, ∃ N : ℕ,
      ∀ n ≥ N, b_seq seq n > c) := sorry

end Imo1970P3

File author(s): Tomas Ortega

This problem has a complete formalized solution.