IMO 2010 N5 (P3) #

Find all functions $f : ℕ⁺ → ℕ⁺$ such that $(f(m) + n)(f(n) + m)$ is a square for any positive integers $m$ and $n$.

Answer #

$f(n) = n$ and $f(n) = n + k$ for some $k ∈ ℕ⁺$.

Solution #

We follow the official solution. The implementation is more comfortably done over $ℕ$ (the natural numbers), so we also solve an even more general functional equation as follows: given a natural number $c$, find all functions $f : ℕ → ℕ$ such that $(f(m) + n + c)(f(n) + m + c)$ is a square any $m, n ∈ ℕ$.

source

def IMOSL.IMO2010N5.good (c : ℕ) (f : ℕ → ℕ) :

Prop

A function f : ℕ → ℕ is called c-good if (f(m) + n + c)(f(n) + m + c) is a square for any m, n : ℕ.

Equations

IMOSL.IMO2010N5.good c f = ∀ (m n : ℕ), ∃ (k : ℕ), (f m + n + c) * (f n + m + c) = k ^ 2

Instances For

source

theorem IMOSL.IMO2010N5.add_right_is_good (c k : ℕ) :

good c fun (x : ℕ) => x + k

The function n ↦ n + k is c-good for any c, k : ℕ.

source

theorem IMOSL.IMO2010N5.step1_general {p a b : ℕ} (hp : Nat.Prime p) (h : ∃ (k : ℕ), a * b = k ^ 2) {n : ℕ} (ha : p ^ (2 * n + 1) ∣ a) (ha0 : ¬p ^ (2 * n + 2) ∣ a) :

p ∣ b

Step 1: if ab is a square and ν_p(a) = 2n + 1 for some n : ℕ, then p ∣ b.

source

theorem IMOSL.IMO2010N5.step1_modeq {p a b : ℕ} (hp : Nat.Prime p) (h : ∃ (k : ℕ), a * b = k ^ 2) {n : ℕ} (ha : a ≡ p ^ (2 * n + 1) [MOD p ^ (2 * n + 2)]) :

p ∣ b

A version of Step 1 with a ≡ p^{2n + 1} (mod p^{2n + 2}).

source

theorem IMOSL.IMO2010N5.step1_pow_one {p a b : ℕ} (hp : Nat.Prime p) (h : ∃ (k : ℕ), a * b = k ^ 2) (ha : a ≡ p [MOD p ^ 2]) :

p ∣ b

A version of Step 1 with a ≡ p (mod p^2).

source

theorem IMOSL.IMO2010N5.exists_add_modeq {b : ℕ} (hb : 0 < b) (a c : ℕ) :

∃ (n : ℕ), a + n ≡ c [MOD b]

For any b > 0 and for any a, c : ℕ, there exists n : ℕ such that a + n ≡ c (mod b).

source

theorem IMOSL.IMO2010N5.map_modeq_prime_imp_modeq {c : ℕ} {f : ℕ → ℕ} {p k l : ℕ} (hf : good c f) (hp : Nat.Prime p) (h : f k ≡ f l [MOD p]) :

k ≡ l [MOD p]

If f is c-good and f(k) ≡ f(l) (mod p), then k ≡ l (mod p).

source

theorem IMOSL.IMO2010N5.not_modeq_prime_imp₁ {k l : ℕ} (h : k ≤ l) (h0 : ∀ (p : ℕ), Nat.Prime p → ¬k ≡ l [MOD p]) :

l = k + 1

If k ≤ l and k ≢ l (mod p) for every prime p, then l = k + 1.

source

theorem IMOSL.IMO2010N5.not_modeq_prime_imp₂ {k l : ℕ} (h : ∀ (p : ℕ), Nat.Prime p → ¬k ≡ l [MOD p]) :

l = k + 1 ∨ k = l + 1

If k ≢ l (mod p) for every prime p, then either l = k + 1 or k = l + 1.

source

theorem IMOSL.IMO2010N5.step3 {f : ℕ → ℕ} (hf : ∀ {p k l : ℕ}, Nat.Prime p → f k ≡ f l [MOD p] → k ≡ l [MOD p]) :

∃ (k : ℕ), f = fun (x : ℕ) => x + k

Let f : ℕ → ℕ be a function such that f(k) ≡ f(l) (mod p) implies k ≡ l (mod p) for any k, l : ℕ and for any prime p. Then f = n ↦ n + k for some k : ℕ.

source