mathlib documentation

mathlib-archive / imo.imo1972_q5

IMO 1972 Q5 #

Problem: f and g are real-valued functions defined on the real line. For all x and y, f(x + y) + f(x - y) = 2f(x)g(y). f is not identically zero and |f(x)| ≤ 1 for all x. Prove that |g(x)| ≤ 1 for all x.