IMO 2010 A4

Define the sequence $(x_n)_{n ≥ 0}$ recursively by $x_0 = 1$, $x_{2k} = (-1)^k x_k$, and $x_{2k + 1} = -x_k$ for all $k ∈ ℕ$. Prove that for any $n ∈ ℕ$, $$ \sum_{i < n} x_i ≥ 0. $$

The sequence (x_n)_{n ≥ 0}

@[reducible, inline]

abbrev IMOSL.IMO2010A4.x : ℕ → Bool

Equations

• IMOSL.IMO2010A4.x n = Nat.binaryRec false (fun (bit : Bool) (k : ℕ) => (bit || k.bodd).xor) n

theorem IMOSL.IMO2010A4.x_zero : x 0 = false

theorem IMOSL.IMO2010A4.x_mul2 (k : ℕ) : x (2 * k) = (k.bodd ^^ x k)

theorem IMOSL.IMO2010A4.x_mul2_add1 (k : ℕ) : x (2 * k + 1) = !x k

theorem IMOSL.IMO2010A4.x_mul4 (k : ℕ) : x (4 * k) = (k.bodd ^^ x k)

theorem IMOSL.IMO2010A4.x_mul4_add1 (k : ℕ) : x (4 * k + 1) = !x (4 * k)

theorem IMOSL.IMO2010A4.x_mul4_add2 (k : ℕ) : x (4 * k + 2) = x k

theorem IMOSL.IMO2010A4.x_mul4_add3 (k : ℕ) : x (4 * k + 3) = x k

The series ∑ x_i

@[reducible, inline]

abbrev IMOSL.IMO2010A4.S (n : ℕ) : ℤ

Equations

• IMOSL.IMO2010A4.S n = ∑ k ∈ Finset.range n, bif IMOSL.IMO2010A4.x k then -1 else 1

theorem IMOSL.IMO2010A4.S_zero : S 0 = 0

theorem IMOSL.IMO2010A4.S_succ (a : ℕ) : S a.succ = S a + bif x a then -1 else 1

theorem IMOSL.IMO2010A4.S_mul4_add2 (k : ℕ) : S (4 * k + 2) = S (4 * k)

theorem IMOSL.IMO2010A4.S_mul4 (k : ℕ) : S (4 * k) = 2 * S k

theorem IMOSL.IMO2010A4.S_parity (k : ℕ) : (S k).bodd = k.bodd

theorem IMOSL.IMO2010A4.S_four_mul_add_eq_zero_iff (q : ℕ) {r : ℕ} (h : r < 4) : S (4 * q + r) = 0 ↔ S q = 0 ∧ (r = 0 ∨ r = 2)

Summary

theorem IMOSL.IMO2010A4.final_solution (k : ℕ) : 0 ≤ S k

Final solution