IMO 2024 Q1

Determine all real numbers $\alpha$ such that, for every positive integer $n$, the integer [ \lfloor \alpha \rfloor + \lfloor 2\alpha \rfloor + \cdots + \lfloor n\alpha \rfloor ] is a multiple of~$n$.

We follow Solution 3 from the official solutions. First reducing modulo 2, any answer that is not a multiple of 2 is inductively shown to be contained in a decreasing sequence of intervals, with empty intersection.

def Imo2024Q1.Condition (α : ℝ) : Prop

The condition of the problem.

Equations

• Imo2024Q1.Condition α = ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋

def Imo2024Q1.solutionSet : Set ℝ

This is to be determined by the solver of the original problem.

Equations

• Imo2024Q1.solutionSet = {α : ℝ | ∃ (m : ℤ), α = 2 * ↑m}

theorem Imo2024Q1.condition_two_mul_int (m : ℤ) : Condition (2 * ↑m)

theorem Imo2024Q1.condition_sub_two_mul_int_iff {α : ℝ} (m : ℤ) : Condition (α - 2 * ↑m) ↔ Condition α

theorem Imo2024Q1.condition_toIcoMod_iff {α : ℝ} : Condition (toIcoMod ⋯ 0 α) ↔ Condition α

theorem Imo2024Q1.Condition.mem_Ico_one_of_mem_Ioo {α : ℝ} (hc : Condition α) (h : α ∈ Set.Ioo 0 2) : α ∈ Set.Ico 1 2

theorem Imo2024Q1.Condition.mem_Ico_n_of_mem_Ioo {α : ℝ} (hc : Condition α) (h : α ∈ Set.Ioo 0 2) {n : ℕ} (hn : 0 < n) : α ∈ Set.Ico ((2 * ↑n - 1) / ↑n) 2

theorem Imo2024Q1.not_condition_of_mem_Ioo {α : ℝ} (h : α ∈ Set.Ioo 0 2) : ¬Condition α

theorem Imo2024Q1.condition_iff_of_mem_Ico {α : ℝ} (h : α ∈ Set.Ico 0 2) : Condition α ↔ α = 0

theorem Imo2024Q1.result (α : ℝ) : Condition α ↔ α ∈ solutionSet