Require Import Reals. Require Import Fourier. Open Scope R_scope. Definition Rfbound (f: R -> R) b := forall x, (Rabs (f x) <= b). (* Least upper bound for function *) Theorem Rflub_def: forall f: R -> R, forall b: R, Rfbound f b -> exists k, (Rfbound f k) /\ (forall b1, (Rfbound f b1) -> k <= b1). intros f b Hb. case (completeness (fun x => exists y, x = (Rabs (f y)))); auto. exists b; red. intros x [y Hy]; rewrite Hy; auto. exists (Rabs (f 0)); exists 0; auto. intros k [Hk1 Hk2]; exists k; split; auto. intros x; apply Hk1; exists x; auto. intros b1 Hb1; apply Hk2. intros x [y Hy]; rewrite Hy; auto. Qed. (* Tactic fields and fourier are first extended *) Ltac ffield := field; try apply Rmult_integral_contrapositive; try split; try intros tmp; fourier. Ltac ffourier := (split_Rabs; auto; fourier; fail). (* Ready for the main theorem *) Theorem imo1972: 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 Eq Nz Rf1 y. case (Rle_or_lt (Rabs (g y)) 1); intros H; auto. case (Rflub_def f _ Rf1); clear Rf1. intros k [Kb Kl]. assert (Kp: 0 < k); [idtac | clear Nz]. case (Rle_or_lt k 0); auto; intros H1. case Nz; intros x. assert (HH: forall x, Rabs x = 0 -> x = 0); [intros x1; ffourier | idtac]. apply HH; clear HH. apply Rle_antisym; [idtac | apply Rabs_pos]. assert (HH := Kb x); ffourier. replace (Rabs (g y)) with (k * (Rabs(g y) / k)); [idtac | ffield; auto with real]. replace 1 with (k / Rabs (g y) * (Rabs (g y) / k)); [idtac | ffield]. apply Rmult_le_compat_r; auto. unfold Rdiv; apply Rle_mult_inv_pos; auto with real; apply Rabs_pos. apply Kl; clear Kl Kp. intros x. replace (Rabs (f x)) with (((2 * Rabs (g y) * Rabs (f x))) * (1/(2 * Rabs (g y)))); [idtac | ffield]. replace (k / Rabs (g y)) with ((2 * k) * (1/(2 * Rabs (g y)))); [idtac | ffield]. apply Rmult_le_compat_r; auto with real. apply (Rle_mult_inv_pos 1 (2 * Rabs (g y))); fourier. pattern 2 at 1; rewrite <- (Rabs_pos_eq 2); auto with real. repeat rewrite <- Rabs_mult. replace (2 * g y * f x) with (2 * f x * g y); [idtac | ffield]. rewrite <- Eq; clear Eq. assert (Bxpy := Kb (x + y)); assert (Bxmy := Kb (x - y)); clear H Kb; ffourier. Qed.