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.