IMO 2019 N4

Fix some $C ∈ ℕ$. Find all functions $f : ℕ → ℕ$ such that $a + f(b) ∣ a^2 + b f(a)$ for any $a, b ∈ ℕ$ satisfying $a + b > C$.

Notes

The original functional equation is of type $ℕ^+ → ℕ^+$. However, the solution can be deduced from this $ℕ$-version as well. We do both versions in this file.

Extra lemmas

theorem IMOSL.IMO2019N4.dvd_iff_of_dvd_add {a b c : ℕ} (h : c ∣ a + b) : c ∣ a ↔ c ∣ b

theorem IMOSL.IMO2019N4.dvd_sq_iff_dvd_sq_of_dvd_add {a b c : ℕ} (h : c ∣ a + b) : c ∣ a ^ 2 ↔ c ∣ b ^ 2

theorem IMOSL.IMO2019N4.eq_zero_of_prime_add_dvd_sq {a p : ℕ} (h : Nat.Prime p) (h0 : a < p) (h1 : p + a ∣ p ^ 2) : a = 0

Start of the problem

def IMOSL.IMO2019N4.good (C : ℕ) (f : ℕ → ℕ) : Prop

Equations

• IMOSL.IMO2019N4.good C f = ∀ (a b : ℕ), C < a + b → a + f b ∣ a ^ 2 + b * f a

theorem IMOSL.IMO2019N4.linear_is_good (C k : ℕ) : good C fun (x : ℕ) => k * x

theorem IMOSL.IMO2019N4.good_is_linear {C : ℕ} {f : ℕ → ℕ} (h : good C f) : ∃ (k : ℕ), f = fun (x : ℕ) => k * x

theorem IMOSL.IMO2019N4.final_solution_Nat {C : ℕ} {f : ℕ → ℕ} : good C f ↔ ∃ (k : ℕ), f = fun (x : ℕ) => k * x

Final solution, Nat version

Extension from ℕ+ → ℕ+ to ℕ → ℕ

def IMOSL.IMO2019N4.goodPNat (C : ℕ+) (f : ℕ+ → ℕ+) : Prop

Equations

• IMOSL.IMO2019N4.goodPNat C f = ∀ (a b : ℕ+), C < a + b → a + f b ∣ a ^ 2 + b * f a

theorem IMOSL.IMO2019N4.linear_is_goodPNat (C k : ℕ+) : goodPNat C fun (x : ℕ+) => k * x

theorem IMOSL.IMO2019N4.goodPNat_is_linear {C : ℕ+} {f : ℕ+ → ℕ+} (h : goodPNat C f) : ∃ (k : ℕ+), f = fun (x : ℕ+) => k * x

theorem IMOSL.IMO2019N4.final_solution {C : ℕ+} {f : ℕ+ → ℕ+} : goodPNat C f ↔ ∃ (k : ℕ+), f = fun (x : ℕ+) => k * x

Final solution