Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1997P1

module

public import Mathlib.Algebra.CharP.Defs
public import Mathlib.Algebra.Order.Archimedean.Real.Basic
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Star
public import Mathlib.Data.Nat.Nth
public import Mathlib.Data.Nat.PrimeFin

public section


/-!
# USA Mathematical Olympiad 1997, Problem 1

Let p₁, p₂, p₃, ... be the prime numbers listed in increasing order, and let x₀
be a real number between 0 and 1. For positive integer k, define

    xₖ = 0,               if xₖ₋₁ = 0,
    xₖ = {pₖ / xₖ₋₁},     if xₖ₋₁ ≠ 0,

where {x} denotes the fractional part of x. (The fractional part of x is given
by x - ⌊x⌋, where ⌊x⌋ is the greatest integer less than or equal to x.)

Find, with proof, all x₀ satisfying 0 < x₀ < 1 for which the sequence
x₀, x₁, x₂, ... eventually becomes 0.
-/

namespace Usa1997P1

/-- The recursion from the problem, parametrized by the sequence `p : ℕ → ℕ`
of positive integers used as numerators, where `p k` is used at step `k + 1`.
The problem instantiates `p` to `Nat.nth Nat.Prime`, the increasing
enumeration of the primes, so that `p k` is the `(k + 1)`-th prime. -/
noncomputable def seq (p : ℕ → ℕ) (x₀ : ℝ) : ℕ → ℝ
  | 0 => x₀
  | k + 1 => if seq p x₀ k = 0 then 0 else Int.fract ((p k : ℝ) / seq p x₀ k)

/-- The answer to the problem: the sequence eventually becomes zero exactly
for the rational numbers in the open interval (0, 1). -/
/- determine -/ abbrev solution_set : Set ℝ := sorry

theorem usa1997_p1 (x₀ : ℝ) (hx₀ : x₀ ∈ Set.Ioo (0 : ℝ) 1) :
    (∃ k, seq (Nat.nth Nat.Prime) x₀ k = 0) ↔ x₀ ∈ solution_set := sorry

end Usa1997P1

File author(s): Kimi K3

This problem has a complete formalized solution.