# Documentation

Archive.Imo.Imo1972Q5

# 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.

theorem imo1972_q5 (f : ) (g : ) (hf1 : ∀ (x y : ), f (x + y) + f (x - y) = 2 * f x * g y) (hf2 : ∀ (y : ), f y 1) (hf3 : x, f x 0) (y : ) :
g y 1

This proof begins by introducing the supremum of f, k ≤ 1 as well as k' = k / ‖g y‖. We then suppose that the conclusion does not hold (hneg) and show that k ≤ k' (by 2 * (‖f x‖ * ‖g y‖) ≤ 2 * k obtained from the main hypothesis hf1) and that k' < k (obtained from hneg directly), finally raising a contradiction with k' < k'.

(Authored by Stanislas Polu inspired by Ruben Van de Velde).

theorem imo1972_q5' (f : ) (g : ) (hf1 : ∀ (x y : ), f (x + y) + f (x - y) = 2 * f x * g y) (hf2 : BddAbove (Set.range fun x => f x)) (hf3 : x, f x 0) (y : ) :
g y 1

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.

This is a more concise version of the proof proposed by Ruben Van de Velde.