(* 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.