(* IMO 1972/B2, (c) 2006 Pierre Corbineau *) Require Import Reals. Set Firstorder Depth 2. Open Scope R_scope. (* Problem B2 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 B2: forall f g : R -> R , (forall x y, f(x + y) + f (x - y) = 2 * f x * g y) -> (~ forall x, f x = 0) -> (forall x, Rabs (f x) <= 1) -> (forall x, Rabs (g x) <= 1). (* Solution Let k be the least upper bound for |f(x)|. Suppose |g(y)| > 1. Take any x with |f(x)| > 0, then 2k <= |f(x+y)| + |f(x-y)| <= |f(x+y) + f(x-y)| = 2|g(y)||f(x)|, so |f(x)| < k/|g(y)|. In other words, k/|g(y)| is an upper bound for |f(x)| which is less than k. Contradiction. *) proof. claim bigger_2_0: (2 > 0). have (2 > 0)%nat. hence (INR 2> INR 0) by lt_INR. end claim. let f,g be such that fge : (forall x y : R, f (x + y) + f (x - y) = 2 * f x * g y) and nzf:(~ (forall x : R, f x = 0)) and bf:(forall x : R, Rabs (f x) <= 1). define f_abs_image z as (exists x, Rabs (f x) = z). let y:R. per cases of (Rabs (g y) <= 1 \/ 1 < Rabs (g y)) by Rle_or_lt. suppose (Rabs (g y) <= 1). hence thesis. suppose (1 < Rabs (g y)). then hy:(Rabs (g y) > 1). claim (is_upper_bound f_abs_image 1). given z,x such that e:(Rabs (f x) = z). have (Rabs (f x) <= 1) by bf. hence thesis by e. end claim. then hb:(bound f_abs_image). have (f_abs_image (Rabs (f 0))) by tactic exists 0;reflexivity. then hnv:(exists x, f_abs_image x). consider k such that bkf:(is_upper_bound f_abs_image k) and ubkf:(forall l:R, is_upper_bound f_abs_image l -> k <= l) from (completeness f_abs_image hb hnv). claim ub:(forall x, Rabs (f x) <= k). let x:R. have (f_abs_image (Rabs (f x))) by tactic exists x;reflexivity. hence thesis by bkf. end claim. claim new_bound:(forall x, Rabs (f x) <= k / (Rabs (g y))). let x:R. have b1:(Rabs (f (x+y))<= k) by ub. have b2:(Rabs (f (x-y))<= k) by ub. have c1:(Rabs (f (x+y)) + Rabs (f (x-y)) <= k + k) by (Rplus_le_compat _ _ _ _ b1 b2). have c2:(Rabs (f (x+y) + f (x-y)) <= Rabs (f (x+y)) + Rabs (f (x-y))) by Rabs_triang. have c3:(Rabs (f (x+y) + f (x-y)) <= k + k) by Rle_trans,c2,c1 . have (Rabs (f (x + y) + f (x - y)) = Rabs (2 * f x * g y)) by fge. ~= (Rabs 2 * Rabs (f x) * Rabs (g y)) by Rabs_mult. ~= (2 * Rabs (f x) * Rabs (g y)) by Rabs_pos_eq,bigger_2_0. then c4:(2 * Rabs (f x) * Rabs (g y) <= k+k) by c3. have (k + k = 2*k) by tactic field. then c5:(2 * (Rabs (f x) * Rabs (g y)) <= 2*k) by Rmult_assoc,c4. then c6:(Rabs (f x) * Rabs (g y) <= k) by Rmult_le_reg_l,bigger_2_0. have hh: (0 <1). then nn:(0 < (Rabs (g y))) by Rlt_trans,hy. then cc: (0 < /(Rabs (g y))) by Rinv_0_lt_compat. then c7:(0 <= /(Rabs (g y))). then (Rabs (f x) * Rabs (g y) * / (Rabs (g y)) <= k * / Rabs (g y)) by Rmult_le_compat_r,c6. then c8:(Rabs (f x) * (Rabs (g y) * / (Rabs (g y))) <= k * / Rabs (g y)) by Rmult_assoc. have nngy:((Rabs (g y))<>0) by Rlt_not_eq,nn. then ( Rabs (g y) * / Rabs (g y) = 1) by Rinv_r. then c9:(Rabs (f x) <= k * / Rabs (g y)) by c8,Rmult_1_r. hence thesis. end claim. claim nub:(is_upper_bound f_abs_image (k / (Rabs (g y)))). given z:R,x:R such that e:(Rabs (f x)=z). have (Rabs (f x) <= (k / (Rabs (g y)))) by new_bound. hence thesis by e. end claim. have contra_1:(k <= k / (Rabs (g y))) by (ubkf _ nub). per cases of (k <= 0 \/ 0 < k) by Rlt_le_dec. suppose pk: (0 < k). have (1 0) by Req_dec. suppose (f x = 0). hence thesis. suppose (f x <> 0). then (Rabs (f x) <> 0) by Rabs_no_R0. hence thesis by e. end cases. end claim. hence thesis by nzf. end cases. end cases. end proof. Qed.