Require Import Reals.
Require Import Fourier.
Require Import Classical.

Open Scope R_scope.

Definition Rfbound (f: R -> R) b := forall x, (Rabs (f x) <= b).

Ltac ffourier := (split_Rabs; auto; fourier; fail).

Theorem imo1972_hales:
 forall f g: R -> R,
 (forall x y: R,  f (x + y) + f (x - y) = 2 * f x * g y) ->
 ~ (forall x: R, f x = 0) ->
 Rfbound f 1 -> Rfbound g 1.
intros f g He Hp Hb.
assert (He1: forall l x y, Rabs (2 * (f x * g y ^ l)) <= 2).
  induction l; simpl;
    [intros x y; rewrite Rmult_1_r; assert (Hu := Hb x); ffourier | 
     idtac].
  intros x y; repeat rewrite <- Rmult_assoc; rewrite <- He;
    rewrite Rmult_plus_distr_r.
  assert (tmp1 := IHl (x + y) y);  assert (tmp2 := IHl (x - y) y).
    clear IHl; ffourier.
case (not_all_ex_not R (fun n => f n = 0) Hp); intros x Hx; clear Hp Hb.
intros y; clear He.
case (Rle_or_lt (Rabs (g y)) 1); intros H; auto.
case (Pow_x_infinity _ H (1 + 2/ Rabs (2 * f x))); intros x0 Hexp; clear H.
assert (Hexp1 := Hexp x0 (le_refl x0)); clear Hexp.
assert (Hexp2 := He1 x0 x y); clear He1.
let x := (type of Hexp2) in absurd x; auto; clear Hexp2; 
 apply Rgt_not_le; rewrite <- Rmult_assoc; rewrite Rabs_mult.
assert (H1: Rabs (2 * f x) > 0).
  red; apply Rabs_pos_lt; apply prod_neq_R0; intros HH; 
    try fourier; case Hx; auto.
pattern 2 at 2;
  replace 2 with (Rabs (2 * f x) * (2 / Rabs (2 * f x))).
  red; apply Rmult_lt_compat_l; ffourier.
field; auto with real.
Qed.