Require Import Reals Ranalysis5 Psatz ClassicalEpsilon. Require Import Rcomplements RInt. Open Scope R_scope. Lemma Rlt_1_2 : 1 < 2. Proof. psatzl R. Qed. Ltac lt0 := match goal with | |- _ => assumption | |- 0 < exp _ => apply exp_pos | |- 0 < pos _ => apply cond_pos | |- _ > 0 => unfold Rgt; lt0 | |- 0 < 1 => apply Rlt_0_1 | |- 0 < 2 => apply Rlt_0_2 | |- 0 < PI => apply PI_RGT_0 | |- _ <> 0 => apply Rgt_not_eq; lt0 | |- 0 < Rabs _ + _ => apply (Rplus_le_lt_0_compat _ _ (Rabs_pos _)); lt0 | |- 0 < _ * _ => apply Rmult_lt_0_compat; lt0 | |- 0 < _ + _ => apply Rplus_lt_0_compat; lt0 | |- 0 < Rmin _ _ => apply Rmin_glb_lt; lt0 | |- 0 < / _ => apply Rinv_0_lt_compat; lt0 | |- 0 < sqrt _ => apply sqrt_lt_R0; lt0 | |- 0 < _ / _ => unfold Rdiv; apply Rmult_lt_0_compat; lt0 | |- 0 < _ ^ _ => apply pow_lt; lt0 | |- 0 < _ ^ 2 + _ => apply Rplus_le_lt_0_compat;[apply pow2_ge_0 | lt0] | |- _ <= _ => apply Rlt_le; lt0 | |- _ => psatzl R end. Lemma open_interval : forall b, open_set (fun x => x < b). intros b; unfold open_set, neighbourhood. intros x xp. assert (dp : 0 < (b - x)/2) by psatzl R. exists (mkposreal _ dp). unfold disc; simpl; intros y py; apply Rabs_lt_between in py; psatzl R. Qed. Definition R_to_nat (v : R) := Z.abs_nat (Zmax (up v - 1) 0). Lemma R_to_nat_INR : forall n, R_to_nat (INR n) = n. intros n; unfold R_to_nat. rewrite INR_IZR_INZ. assert (0 <= up (IZR (Z.of_nat n)) - 1)%Z. destruct n as [ | n]. assert (t := up_tech 0 0); simpl in t |- *; rewrite <- t; try psatzl R. lia. rewrite <- INR_IZR_INZ. assert (1 <= INR (S n)). rewrite S_INR; assert (t := pos_INR n); psatzl R. apply le_IZR; destruct (archimed (INR (S n))); simpl (IZR 0). rewrite minus_IZR; simpl (IZR 1); psatzl R. assert (step : Z.max (up (IZR (Z.of_nat n)) - 1) 0 = (up (IZR (Z.of_nat n)) - 1)%Z); [ | rewrite step; clear step]. rewrite Zmax_left;[reflexivity | lia]. pattern n at 2; rewrite <- Zabs2Nat.id; apply f_equal. assert (up (IZR (Z.of_nat n)) = (Z.of_nat n + 1)%Z);[ | lia]. symmetry; apply tech_up; rewrite plus_IZR; simpl (IZR 1); psatzl R. Qed. Lemma R_to_nat_le : forall x y, x <= y -> (R_to_nat x <= R_to_nat y)%nat. intros x y xy; unfold R_to_nat. assert (up x <= up y)%Z. destruct (Rlt_dec y (IZR (up x))). assert (t := archimed x). assert (IZR (up x) <= y + 1) by psatzl R. rewrite (tech_up y (up x)); try psatzl R; lia. destruct (archimed y). apply le_IZR; apply Rlt_le, Rle_lt_trans with y; psatzl R. apply Zabs_nat_le. lia. Qed. Definition ext a b (f : R -> R) x := match Rle_dec x a with left _ => f a | right _ => match Rle_dec b x with left _ => f b | _ => f x end end. Lemma ext_eq : forall a b f x, a <= x <= b -> ext a b f x = f x. intros a b f x intx; unfold ext; destruct (Rle_dec x a). replace x with a; psatzl R. destruct (Rle_dec b x);[replace x with b | ];psatzl R. Qed. Lemma extend_continuity : forall a b f, a < b -> (forall x, a <= x <= b -> continuity_pt f x) -> continuity (ext a b f). unfold ext;intros a b f ab ct x eps ep . destruct (Rle_dec x a). destruct (Req_EM_T x a) as [xa | xna]. rewrite xa; assert (inta : a <= a <= b) by psatzl R. destruct (ct a inta eps ep) as [alp [ap Pa]]. exists alp;split;[exact ap | intros y Dy]. destruct (Rle_dec y a). simpl; rewrite R_dist_eq; assumption. destruct (Rle_dec b y). simpl; apply Pa; simpl. split;[split;[exact I | psatzl R ] | unfold R_dist; rewrite Rabs_pos_eq; try psatzl R]. simpl in Dy; unfold R_dist in Dy; rewrite Rabs_pos_eq in Dy; psatzl R. apply Pa; assumption. exists ((a - x)/2);split;[psatzl R | ]. simpl; unfold R_dist; intros y Dy. destruct (Rle_dec y a);[rewrite Rminus_eq0, Rabs_R0; assumption |]. rewrite Rabs_pos_eq in Dy; psatzl R. destruct (Rle_dec b x). destruct (Req_EM_T b x) as [bx | xnb]. rewrite <- bx; assert (intb : a <= b <= b) by psatzl R. destruct (ct b intb eps ep) as [alp [ap Pa]]. exists alp;split;[exact ap | intros y Dy]. destruct (Rle_dec b y). destruct (Rle_dec y a);[psatzl R | ]. simpl; rewrite R_dist_eq; assumption. destruct (Rle_dec y a). apply Pa. simpl; unfold R_dist; rewrite <- Rabs_Ropp, Rabs_pos_eq; [ | psatzl R]. split;[split;[exact I | psatzl R] |]. simpl in Dy; unfold R_dist in Dy; rewrite <-Rabs_Ropp, Rabs_pos_eq in Dy; psatzl R. apply Pa; assumption. exists ((x - b)/2);split;[psatzl R | ]. simpl; unfold R_dist; intros y Dy. destruct Dy as [_ Dy]; apply Rabs_lt_between in Dy. destruct (Rle_dec y a);[ psatzl R | ]. destruct (Rle_dec b y);[ | psatzl R]. rewrite Rminus_eq0, Rabs_R0; assumption. assert (intx : a <= x <= b) by psatzl R. destruct (ct _ intx eps ep) as [alpha [ap Pa]]. exists (Rmin (Rmin (b - x) (x - a)) alpha). split. repeat apply Rmin_glb_lt; try psatzl R. assert (Rmin (Rmin (b - x) (x - a)) alpha <= alpha). apply Rmin_r. assert (Rmin (Rmin (b - x) (x - a)) alpha <= x - a). apply Rle_trans with (Rmin (b - x) (x - a)). apply Rmin_l. apply Rmin_r. assert (Rmin (Rmin (b - x) (x - a)) alpha <= b - x). apply Rle_trans with (Rmin (b - x) (x - a)); apply Rmin_l. intros y [cy inty]; simpl in inty; unfold R_dist in inty; apply Rabs_lt_between in inty. destruct (Rle_dec y a);[psatzl R | ]. destruct (Rle_dec b y);[psatzl R | ]. apply Pa; split;[assumption | simpl; unfold R_dist]. apply Rabs_def1; psatzl R. Qed. Lemma CV_shift : (* standard *) forall f k l, Un_cv (fun n => f (n + k)%nat) l -> Un_cv f l. intros f' k l cvfk eps ep; destruct (cvfk eps ep) as [N Pn]. exists (N + k)%nat; intros n nN; assert (tmp: (n = (n - k) + k)%nat) by omega. rewrite tmp; apply Pn; omega. Qed. Lemma CV_shift' : (* standard *) forall f k l, Un_cv f l -> Un_cv (fun n => f (n + k)%nat) l. intros f' k l cvf eps ep; destruct (cvf eps ep) as [N Pn]. exists N; intros n nN; apply Pn; omega. Qed. Lemma Dini : forall a b, a < b -> forall f_ f, (forall x, a <= x <= b -> Un_cv (fun n => f_ n x) (f x)) -> (forall n x, a <= x <= b -> continuity_pt (f_ n) x) -> (forall x, a <= x <= b -> continuity_pt f x) -> (forall x, a <= x <= b -> Un_growing (fun n => f_ n x)) -> forall c d, (forall x, Boule c d x -> a <= x <= b) -> CVU f_ f c d. intros a b ab f_ f cv ct ctf gr c d cp eps ep. set (E := fun n x => Rabs (ext a b (f_ n) x - ext a b f x) < eps). set (Ef := mkfamily (* (fun x => 0 <= x) *) (fun _ => True) (fun x y => (* 0 <= x /\ *) E (R_to_nat x) y) (* (fun x h => let (y, h') := h in let (h2, _) := h' in h2) *) (fun x h => I)). assert (cos : covering_open_set (fun x => a <= x <= b) Ef). split. intros x intx; destruct (cv x intx eps ep) as [N Pn]. exists (INR N). simpl. rewrite R_to_nat_INR. unfold E; rewrite !ext_eq; auto. (* split; [apply pos_INR | ]. *) solve[apply Pn; apply le_n]. intros nR. simpl in Ef. apply open_set_P6 with (fun y => Rabs (ext a b (f_ (R_to_nat nR)) y - ext a b f y) < eps). apply (continuity_P2 (fun y => Rabs (ext a b (f_ (R_to_nat nR)) y - ext a b f y)) (fun x => x < eps)). solve[reg; apply extend_continuity; auto]. apply open_interval. unfold Ef; simpl. split; intros y h; exact h. destruct (compact_P3 a b Ef cos) as [sE [P1 [l Pl]]]. exists (R_to_nat (MaxRlist l)). intros n y nmax b_y. assert (inty : a <= y <= b) by (apply cp; assumption). assert (cvy : Un_cv (fun n => f_ n y) (f y)) by (apply cv; assumption). assert (fy_ineq : f_ n y <= f y). apply (growing_ineq (fun n => f_ n y) (f y)); [apply gr; assumption| apply cvy]. destruct (P1 y inty) as [ny [Pny Pny']]. rewrite Rabs_pos_eq;[ | psatzl R]. simpl in Pl; unfold intersection_domain in Pl. assert (Pl' : True /\ sE ny). split; [auto |]; assumption. rewrite Pl in Pl'. assert (nymax : ny <= MaxRlist l). apply MaxRlist_P1; assumption. replace (f y - f_ n y) with (f y - f_ (R_to_nat ny) y + (f_ (R_to_nat ny) y - f_ n y)) by ring. rewrite <- (Rplus_0_r eps); apply Rplus_lt_le_compat. rewrite <- (ext_eq a b f), <- (ext_eq a b (f_ _)); auto. unfold Ef, E in Pny; simpl in Pny. assert (ext a b (f_ (R_to_nat ny)) y <= ext a b f y). rewrite !ext_eq; try psatzl R. apply (growing_ineq (fun n => f_ n y)); solve[auto]. rewrite <- Rabs_Ropp, Rabs_pos_eq in Pny; psatzl R. assert (f_ (R_to_nat ny) y <= f_ n y);[ | psatzl R]. apply (tech9 (fun n => f_ n y));[apply gr; assumption | ]. apply le_trans with (2 := nmax). apply R_to_nat_le; assumption. Qed. Lemma sqrt_pow2 : forall x, 0 <= x -> sqrt (x ^ 2) = x. intros; simpl; rewrite Rmult_1_r, sqrt_square; auto. Qed. Lemma Ropp_Rmax : forall x y, - Rmax x y = Rmin (-x) (-y). intros x y; apply Rmax_case_strong. intros w; rewrite Rmin_left;[ reflexivity | psatzl R]. intros w; rewrite Rmin_right; [reflexivity | psatzl R]. Qed. Lemma Rmax_assoc : forall a b c, Rmax a (Rmax b c) = Rmax (Rmax a b) c. intros a b c; unfold Rmax; destruct (Rle_dec b c); destruct (Rle_dec a b); destruct (Rle_dec a c); destruct (Rle_dec b c); psatzl R. Qed. Lemma Rminmax : forall a b, Rmin a b <= Rmax a b. (* TODO : General theorem *) intros a b; destruct (Rle_dec a b). rewrite Rmin_left, Rmax_right; assumption. rewrite Rmin_right, Rmax_left; psatzl R. Qed. Lemma Rmin_assoc : forall x y z, Rmin x (Rmin y z) = Rmin (Rmin x y) z. intros x y z; unfold Rmin. destruct (Rle_dec y z); destruct (Rle_dec x y); destruct (Rle_dec x z); destruct (Rle_dec y z); try psatzl R. Qed. Lemma R_dist_mult_l : forall a b c, R_dist (a * b) (a * c) = Rabs a * R_dist b c. unfold R_dist. intros a b c; rewrite <- Rmult_minus_distr_l, Rabs_mult; reflexivity. Qed. Lemma primitive_ext : forall f a b (ab : a <= b) (h h' : forall x, a <= x -> x <= b -> Riemann_integrable f a x) x, primitive ab h x = primitive ab h' x. intros f a b ab h h' x; unfold primitive. destruct (Rle_dec a x); destruct (Rle_dec x b). apply RiemannInt_P5. apply f_equal, RiemannInt_P5. reflexivity. reflexivity. Qed. Lemma RiemannInt_const_bound : forall f a b l u (h : Riemann_integrable f a b), a <= b -> (forall x, a < x < b -> l <= f x <= u) -> l * (b - a) <= RiemannInt h <= u * (b - a). intros f a b l u ri ab intf. rewrite <- !(fun l => RiemannInt_P15 (RiemannInt_P14 a b l)). split; apply RiemannInt_P19; try assumption; intros x intx; unfold fct_cte; destruct (intf x intx); assumption. Qed. Definition up_infinite_integrable (f : R -> R) (a : R) := {h : forall b, a < b -> Riemann_integrable f a b & {l : R | forall eps, eps > 0 -> exists K, forall b, K < b -> forall h', R_dist (RiemannInt (h b h')) l < eps}}. Definition down_infinite_integrable (f : R -> R) (a : R) := {h : forall b, b < a -> Riemann_integrable f b a & {l : R | forall eps, eps > 0 -> exists K, forall b, b < K -> forall h', R_dist (RiemannInt (h b h')) l < eps}}. Definition infinite_integrable (f : R -> R) := {h : forall a b, a < b -> Riemann_integrable f a b & {l : R | forall eps, eps > 0 -> exists K, forall a b, a < -K -> K < b -> forall h', R_dist (RiemannInt (h a b h')) l < eps}}. Definition upInt (f : R -> R) (a : R) (h : up_infinite_integrable f a) : R := match h with existT h (exist l _) => l end. Arguments upInt [f a] h. Definition downInt (f : R -> R) (a : R) (h : down_infinite_integrable f a) :R := match h with existT h (exist l _) => l end. Definition infInt (f : R -> R) (h : infinite_integrable f) : R := match h with existT h (exist l _) => l end. Lemma infinite_integrable_down_up : forall f a, down_infinite_integrable f a -> up_infinite_integrable f a -> infinite_integrable f. intros f a [dib [dil Pd]] [uib [uil Pu]]. assert (h' : forall c d, c < d -> Riemann_integrable f c d). intros c d cltd; destruct (Rlt_dec a d) as [altd | dlea]. destruct (Rlt_dec c a) as [clta | alec]. apply RiemannInt_P24 with a. apply dib; assumption. apply uib; assumption. destruct (Req_EM_T a c) as [aqc | anc]. rewrite <- aqc; apply uib; psatzl R. apply RiemannInt_P24 with a. apply RiemannInt_P1, uib; psatzl R. apply uib; assumption. apply RiemannInt_P24 with a. apply dib; psatzl R. case (Req_EM_T a d) as [aqd | and]. rewrite aqd; apply RiemannInt_P7. apply RiemannInt_P1, dib; psatzl R. exists h'; exists (dil + uil). intros eps ep. assert (ep' : eps/2 > 0) by psatzl R. destruct (Pu _ ep') as [Ku Pku]. destruct (Pd _ ep') as [Kd Pkd]. exists (Rmax (Rabs a) (Rmax (Rabs Ku) (Rabs Kd))); intros c d. intros cdown dup. assert (c < a). rewrite Ropp_Rmax in cdown. apply Rlt_le_trans with (1 := cdown). apply Rle_trans with (1 := Rmin_l _ _). assert (-a <= Rabs a);[ | psatzl R]. rewrite <- Rabs_Ropp; apply RRle_abs. assert (a < d). apply Rle_lt_trans with (2 := dup). apply Rle_trans with (2 := Rmax_l _ _). apply RRle_abs. intros h'0. replace (RiemannInt (h' c d h'0)) with (RiemannInt (dib _ H) + RiemannInt (uib _ H0)) . apply Rle_lt_trans with (1 := R_dist_plus _ _ _ _). assert (c < Kd). rewrite Ropp_Rmax in cdown. apply Rlt_le_trans with (1 := cdown). apply Rle_trans with (1 := Rmin_r _ _). rewrite Ropp_Rmax. apply Rle_trans with (1 := Rmin_r _ _). assert (-Kd <= Rabs Kd);[ | psatzl R]. rewrite <- Rabs_Ropp; apply RRle_abs. assert (Ku < d). apply Rle_lt_trans with (2 := dup). apply Rle_trans with (2 := Rmax_r _ _). apply Rle_trans with (2 := Rmax_l _ _). apply RRle_abs. assert (t := Pkd _ H1 H). assert (t' := Pku _ H2 H0). psatzl R. apply RiemannInt_P26. Qed. Lemma up_infinite_integrable_break_aux : forall f a b, up_infinite_integrable f a -> Riemann_integrable f a b -> forall c, b < c -> Riemann_integrable f b c. intros f a b [ha [la fa]] fab c bc. assert (fba := RiemannInt_P1 fab). destruct (Rlt_dec a c) as [altc | clea]. solve[apply RiemannInt_P24 with a; auto]. apply RiemannInt_P22 with a; auto; psatzl R. Qed. Lemma up_infinite_integrable_break : forall f a b, up_infinite_integrable f a -> Riemann_integrable f a b -> up_infinite_integrable f b. intros f a b ha fab. assert (fba := RiemannInt_P1 fab). assert (u := up_infinite_integrable_break_aux f a b ha fab); exists u. destruct ha as [ha [la fa]]; exists (RiemannInt fba + la). intros eps ep; destruct (fa eps ep) as [Ka Pka]. exists (Rmax Ka a); intros c Kc bc. assert (altc : a < c) by apply Rle_lt_trans with (2 := Kc), Rmax_r. replace (RiemannInt (u c bc)) with (RiemannInt fba + RiemannInt (ha _ altc)). apply Rle_lt_trans with (1 := R_dist_plus _ _ _ _). rewrite R_dist_eq, Rplus_0_l. apply Pka, (Rle_lt_trans _ _ _ (Rmax_l _ _) Kc). apply RiemannInt_P26. Defined. Lemma upInt_eq : forall f a (h1 h2 : up_infinite_integrable f a), upInt h1 = upInt h2. intros f a [h1 [v1 Pv1]] [h2 [v2 Pv2]]; simpl. rewrite <- R_dist_refl. assert (R_dist v1 v2 <= 0);[ | assert (t := R_dist_pos v1 v2);psatzl R]. apply prop_eps; intros eps ep; assert (ep2 : 0 < eps/2) by psatzl R. destruct (Pv2 _ ep2) as [K2 Pk2]; destruct (Pv1 _ ep2) as [K1 Pk1]. assert (d1 : K1 < Rmax a (Rmax K1 K2) + 1). rewrite Rmax_comm, <-Rmax_assoc. apply Rle_lt_trans with (1 := Rmax_l _ (Rmax K2 a)); psatzl R. assert (d2 : K2 < Rmax a (Rmax K1 K2) + 1). rewrite Rmax_assoc. apply Rle_lt_trans with (1 := Rmax_r (Rmax a K1) _); psatzl R. assert (da : a < Rmax a (Rmax K1 K2) + 1). apply Rle_lt_trans with (1 := Rmax_l _ (Rmax K1 K2)); psatzl R. apply Rle_lt_trans with (1:= R_dist_tri _ _ (RiemannInt (h1 _ da))). replace eps with (eps/2 + eps/2) by field. apply Rplus_lt_compat. solve[rewrite R_dist_sym; apply Pk1; auto]. solve[rewrite (RiemannInt_P5 (h1 _ da) (h2 _ da)); apply Pk2; auto]. Qed. Lemma upInt_break : forall f a b (ha : up_infinite_integrable f a) (hba : Riemann_integrable f b a) (hb : up_infinite_integrable f b), RiemannInt hba + upInt ha = upInt hb. intros f a b ha hba hb; rewrite (upInt_eq _ _ hb (up_infinite_integrable_break f a b ha (RiemannInt_P1 hba))). destruct ha as [ha [la fa]]; simpl. rewrite (RiemannInt_P5 (RiemannInt_P1 (RiemannInt_P1 hba)) hba); reflexivity. Qed. Lemma Riemann_integrable_eq : forall f g a b, (forall x, Rmin a b <= x <= Rmax a b -> f x = g x) -> Riemann_integrable f a b -> Riemann_integrable g a b. intros f g a b fg rif eps; destruct (rif eps) as [phi [psi [P1 P2]]]. exists phi; exists psi;split;[ | assumption ]. intros t intt; rewrite <- fg;[ | assumption]. apply P1; assumption. Qed. Lemma up_infinite_integrable_ext : forall f g a, (forall x, a <= x -> f x = g x) -> up_infinite_integrable f a -> up_infinite_integrable g a. intros f g a fg [hf [lf pf]]. assert (hg: forall b, a < b -> Riemann_integrable g a b). intros b ab; apply Riemann_integrable_eq with f. intros x intx; apply fg. rewrite <- (Rmin_left a b); psatzl R. apply hf; assumption. exists hg; exists lf; intros eps ep; destruct (pf _ ep) as [K Pk]. exists K; intros b Kb ab. rewrite <- (RiemannInt_P18 (hf b ab) (hg b ab)). apply Pk; assumption. psatzl R. intros x intx; apply fg; psatzl R. Qed. Lemma up_infinite_integrable_lin : forall f g a c, up_infinite_integrable f a -> up_infinite_integrable g a -> up_infinite_integrable (fun x => f x + c * g x) a. intros f g a c [hf [lf Pf]] [hg [lg Pg]]. assert (h' : forall b, a < b -> Riemann_integrable (fun x => f x + c * g x) a b). intros b ab; apply RiemannInt_P10; solve[auto]. exists h'; exists (lf + c * lg). destruct (Req_EM_T c 0) as [c0 | cn0]. intros eps ep; destruct (Pf eps ep) as [K Pk]; exists K; intros b Kb ab. replace (RiemannInt (h' b ab)) with (RiemannInt (hf _ ab) + c * RiemannInt (hg _ ab)) by apply sym_equal, RiemannInt_P13. solve[rewrite c0, !Rmult_0_l, !Rplus_0_r; apply Pk; auto]. assert (0 < Rabs c) by (apply Rabs_pos_lt; assumption). intros eps ep; assert (ep1 : eps/(1 + Rabs c) > 0). apply Rmult_lt_0_compat;[assumption | ]. solve[apply Rinv_0_lt_compat, Rplus_lt_0_compat;psatzl R]. destruct (Pf _ ep1) as [Kf Pkf]; destruct (Pg _ ep1) as [Kg Pkg]. exists (Rmax Kf Kg); intros b Kb ab. assert (dc :RiemannInt (h' _ ab) = RiemannInt (hf _ ab) + c * RiemannInt (hg _ ab)) by apply RiemannInt_P13. rewrite dc; apply Rle_lt_trans with (1 := R_dist_plus _ _ _ _). replace eps with (eps/(1 + Rabs c) + Rabs c * (eps/(1 + Rabs c))) by (field; psatzl R). apply Rplus_lt_compat;[solve[apply Pkf, Rle_lt_trans with (2 := Kb), Rmax_l]|]. rewrite R_dist_mult_l; apply Rmult_lt_compat_l;[ assumption | ]. apply Pkg, Rle_lt_trans with (2 := Kb), Rmax_r. Qed. Lemma derivable_pt_lim_eq : forall f g x a b l, a < x < b -> (forall z, a < z < b -> f z = g z) -> derivable_pt_lim f x l -> derivable_pt_lim g x l. intros f g x a b l axb fg df e ep. destruct (df e ep) as [d pd]. assert (d'h : 0 < Rmin d (Rmin (b - x) (x - a))). apply Rmin_pos;[apply cond_pos | apply Rmin_pos; psatzl R]. exists (mkposreal _ d'h); simpl; intros h hn0 cmp. rewrite <- !fg;[ |assumption | ]. apply pd;[assumption |]. apply Rlt_le_trans with (1 := cmp), Rmin_l. assert (-h < x - a). apply Rle_lt_trans with (1 := Rle_abs _). rewrite Rabs_Ropp; apply Rlt_le_trans with (1 := cmp). rewrite Rmin_assoc; apply Rmin_r. assert (h < b - x). apply Rle_lt_trans with (1 := Rle_abs _). apply Rlt_le_trans with (1 := cmp). rewrite Rmin_comm, <- Rmin_assoc; apply Rmin_l. psatzl R. Qed. Lemma antiderivative_Riemann : forall f g a b (h : a <= b) (C0 : forall x, a <= x <= b -> continuity_pt f x), antiderivative f g a b -> forall h' : Riemann_integrable f a b, RiemannInt h' = g b - g a. intros f g a b h C0 atdfg h'. destruct (antiderivative_Ucte f g _ a b atdfg (RiemannInt_P29 h C0)) as [c Pc]. rewrite !Pc;[ | psatzl R | psatzl R]; unfold primitive. destruct (Rle_dec a b) as [ab' | anb];[ | elimtype False; psatzl R]. destruct (Rle_dec b b) as [bb' | bnb];[ | psatzl R]. destruct (Rle_dec a a) as [aa' | ana];[ | elimtype False; psatzl R]. rewrite RiemannInt_P9, (RiemannInt_P5 _ (FTC_P1 h C0 ab' bb')); ring. Qed. Lemma up_infinite_integrable_power_aux1 : forall a b c, 0 < a -> 1 < b -> a < c -> Riemann_integrable (fun x => Rpower x (-b)) a c. intros a b c a0 b1; revert c. assert(ct : forall c x : R, a <= x <= c -> continuity_pt (fun x0 : R => Rpower x0 (- b)) x). intros c x axc; apply derivable_continuous_pt. assert (derivable_pt_lim (fun x => Rpower x (-b)) x (-b * Rpower x (-b - 1))). apply derivable_pt_lim_power; psatzl R. eapply exist; eassumption. intros c ac; apply continuity_implies_RiemannInt;[psatzl R | apply ct]. Qed. Lemma up_infinite_integrable_aux2 : forall a b (a0 : 0 < a) (b1 : 1 < b), forall eps : R, eps > 0 -> exists K : R, forall c : R, K < c -> a < c -> forall h' : Riemann_integrable (fun y => Rpower y (-b)) a c, R_dist (RiemannInt h') (Rpower a (- b + 1) / (b - 1)) < eps. intros a b a0 b1 eps ep. exists (exp (-ln((b - 1) * eps) /(b - 1))). intros c ec ac h'. assert (ac' : a <= c) by psatzl R. rewrite (antiderivative_Riemann (fun x => Rpower x (-b)) (fun x => -Rpower x (-b + 1)/(b - 1)) a c ac'). unfold R_dist. match goal with |- Rabs ?a < eps => replace a with (-Rpower c (-b + 1)/(b-1)) by (field; psatzl R) end. rewrite Ropp_div, Rabs_Ropp, Rabs_pos_eq. rewrite <- (exp_ln eps);[ | assumption]. rewrite <- (exp_ln (b - 1));[ | psatzl R]. unfold Rdiv, Rpower; rewrite <- exp_Ropp, <- exp_plus. apply exp_increasing. apply (Rplus_lt_reg_r (ln (b - 1))). rewrite Rplus_comm, Rplus_assoc, Rplus_opp_l, Rplus_0_r. apply Ropp_lt_cancel; replace (- ((-b + 1) * ln c)) with ((b - 1) * ln c) by ring. apply (Rmult_lt_reg_l (/(b - 1))). apply Rinv_0_lt_compat; psatzl R. rewrite <- Rmult_assoc, Rinv_l, Rmult_1_l, Rmult_comm;[ | psatzl R]. rewrite <- ln_mult;[ | psatzl R | assumption]. rewrite <- (ln_exp (-ln((b - 1) * eps) * / (b - 1))). apply ln_increasing;[apply exp_pos | exact ec]. unfold Rpower; apply Rlt_le, Rmult_lt_0_compat;[apply exp_pos | ]. apply Rinv_0_lt_compat; psatzl R. intros x int; apply derivable_continuous_pt. assert (derivable_pt_lim (fun x => Rpower x (-b)) x (-b * Rpower x (-b - 1))). apply derivable_pt_lim_power; psatzl R. eapply exist; eassumption. split;[ | assumption]. intros x [ax xc]. assert (pr : derivable_pt_lim (fun y => -Rpower y (-b+1)/(b-1)) x (Rpower x (-b))). replace (Rpower x (-b)) with (-((-b + 1) * Rpower x (-b))/(b-1) + (-Rpower x (-b + 1)) * 0) by (field; psatzl R). apply (derivable_pt_lim_mult (fun y => -Rpower y (-b + 1))(fun y => /(b-1))); [ | apply derivable_pt_lim_const]. unfold Rpower; apply derivable_pt_lim_opp. assert (t : (-b + 1) * exp (-b * ln x) = ((-b + 1)/x) * exp ((-b + 1) * ln x)). unfold Rdiv; rewrite Rmult_assoc; apply f_equal. pattern x at 2; rewrite <- exp_ln, <- exp_Ropp; [ | psatzl R]. rewrite <- exp_plus. replace (-ln x + (-b+1) * ln x) with (-b * ln x) by ring; reflexivity. rewrite t, Rmult_comm; apply (derivable_pt_lim_comp _ exp). apply derivable_pt_lim_scal, derivable_pt_lim_ln; psatzl R. solve[apply derivable_pt_lim_exp]. exists (exist _ (Rpower x (- b)) pr); reflexivity. Qed. Lemma up_infinite_integrable_Rpower : forall a b, 0 < a -> 1 < b -> up_infinite_integrable (fun x => Rpower x (-b)) a. intros a b a0 b1. exists (fun c => up_infinite_integrable_power_aux1 a b c a0 b1). exists (Rpower a (-b + 1)/(b - 1)). intros eps ep; destruct (up_infinite_integrable_aux2 a b a0 b1 eps ep) as [K Pk]. exists K; intros c Kc ac; apply Pk; assumption. Defined. Lemma Rpower_upInt : forall a b (a0 : 0 < a) (b1 : 1 < b), upInt (up_infinite_integrable_Rpower a b a0 b1) = (Rpower a (-b + 1)/(b - 1)). intros a b a0 b1; reflexivity. Qed. Lemma Rpower_upInt2 : forall a (a0 : 0 < a), upInt (up_infinite_integrable_Rpower a 2 a0 Rlt_1_2) = /a. intros a a0; rewrite Rpower_upInt; replace (2 - 1) with 1 by ring. replace (-2 + 1) with (-1) by ring; rewrite Rpower_Ropp. solve[unfold Rdiv; rewrite Rinv_1, Rmult_1_r, Rpower_1; auto]. Qed. Lemma upInt_ge_0 : forall f a, forall u : up_infinite_integrable f a, (forall x, a <= x -> 0 <= f x) -> 0 <= upInt u. intros f a [u [l Pl]] fp; simpl. assert (-l <= 0);[ | psatzl R]; apply prop_eps. intros eps ep; destruct (Pl _ ep) as [K Pk]. assert (da : a < Rmax K a + 1). apply Rle_lt_trans with (1 := Rmax_r K _); psatzl R. assert (dK : K < Rmax K a + 1). apply Rle_lt_trans with (1 := Rmax_l _ a); psatzl R. apply Rle_lt_trans with (2 := Pk _ dK da). apply Rle_trans with (RiemannInt (u (Rmax K a + 1) da) - l). replace (-l) with (RiemannInt (RiemannInt_P14 a (Rmax K a + 1) 0) - l). apply Rplus_le_compat_r, RiemannInt_P19. apply Rlt_le; assumption. intros x intx; unfold fct_cte; apply fp;psatzl R. rewrite RiemannInt_P15, Rmult_0_l, Rminus_0_l; reflexivity. unfold R_dist; apply Rle_abs. Qed. Lemma up_integrable_vanish : forall f a, up_infinite_integrable f a -> forall eps, eps > 0 -> exists K, forall b, K <= b -> exists h : up_infinite_integrable f b, Rabs (upInt h) < eps. intros f a [ha [la fa]] eps ep. assert (h' := fun b h => upInt_break f a b (existT _ ha (exist _ la fa)) (RiemannInt_P1 h) (up_infinite_integrable_break f a b (existT _ ha (exist _ la fa)) h)). simpl in h'. destruct (fa _ ep) as [K Pk]; exists (Rmax a K + 1). intros b Kb. assert (da : a < b). apply Rlt_le_trans with (2 := Kb). apply Rle_lt_trans with (1 := Rmax_l _ K). psatzl R. assert (K < b). apply Rlt_le_trans with (2 := Kb). apply Rle_lt_trans with (1 := Rmax_r a _). psatzl R. exists (up_infinite_integrable_break f a b (existT _ ha (exist _ la fa)) (ha _ da)). simpl. rewrite (RiemannInt_P8 _ (ha b da)), <- Rabs_Ropp, Ropp_plus_distr, Ropp_involutive. apply Pk; assumption. Qed. Lemma up_integrable_vanish_Riemann : forall f a, up_infinite_integrable f a -> forall eps, eps > 0 -> exists K, forall b c, K <= b <= c -> forall h: Riemann_integrable f b c, Rabs (RiemannInt h) < eps. intros f a fa eps ep. assert (ep2 : 0 < eps/2) by psatzl R. destruct (up_integrable_vanish f a fa _ ep2) as [K Pk]. exists K. intros b c int bc; assert (db : K <= b) by tauto; assert (dc : K <= c) by psatzl R. destruct (Pk _ db) as [hb Pb]; destruct (Pk _ dc) as [hc Pc]. replace (RiemannInt bc) with (upInt hb - upInt hc). replace eps with (eps/2 + eps/2) by field. apply Rle_lt_trans with (1 := Rabs_triang _ _). apply Rplus_lt_compat;[|rewrite Rabs_Ropp];assumption. rewrite <- (upInt_break _ _ _ hb (RiemannInt_P1 bc) hc). rewrite (RiemannInt_P8 bc (RiemannInt_P1 bc)); ring. Qed. (* Lemma plus_INR_diff : forall a b N, a + INR N <= b -> (N <= Zabs_nat (up (b - a)))%nat. intros a b N diff. rewrite <- (Zabs2Nat.id N); apply Zabs_nat_le;split;[apply Zle_0_nat|]. apply le_IZR; rewrite <- INR_IZR_INZ; assert (t := archimed (b - a)); psatzl R. Qed. *) Ltac Rmax_isol f := rewrite ?Rmax_assoc, <- ?(Rmax_comm f), <- ?Rmax_assoc; match goal with |- _ < Rmax _ ?b + _ => apply Rle_lt_trans with (1:=Rmax_l _ b); psatzl R end. Lemma upInt_ext : forall f g a (hf : up_infinite_integrable f a) (hg : up_infinite_integrable g a), (forall x, a <= x -> f x = g x) -> upInt hf = upInt hg. intros f g a hf hg ext. rewrite <- (R_dist_refl (upInt hf) (upInt hg)). apply Rle_antisym;[ | assert (t := R_dist_pos (upInt hf) (upInt hg)); psatzl R]. apply prop_eps; intros eps ep; assert (ep2 : 0 < eps/2) by psatzl R. destruct (up_integrable_vanish f a hf _ ep2) as [Kf Pf]. destruct (up_integrable_vanish g a hg _ ep2) as [Kg Pg]. set (u := Rmax a (Rmax Kf Kg) + 1). assert (ua : a < u) by (unfold u; Rmax_isol a). assert (uKf : Kf < u) by (unfold u; Rmax_isol Kf). assert (uKg : Kg < u) by (unfold u; Rmax_isol Kg). destruct (Pf u (Rlt_le _ _ uKf)) as [hfk Pf2]. destruct (Pg u (Rlt_le _ _ uKg)) as [hgk Pg2]. assert (tf := hf); destruct tf as [tf _]. assert (tg := hg); destruct tg as [tg _]. assert (hfau : Riemann_integrable f a u) by (apply tf; assumption). assert (hgau : Riemann_integrable g a u) by (apply tg; assumption). rewrite <- (upInt_break _ _ _ hfk hfau hf), <- (upInt_break _ _ _ hgk hgau hg). apply Rle_lt_trans with (1:= R_dist_plus _ _ _ _). rewrite (RiemannInt_P18 hfau hgau), R_dist_eq, Rplus_0_l;[ |psatzl R |]. unfold R_dist, Rminus; apply Rle_lt_trans with (1 := Rabs_triang _ _). replace eps with (eps/2 + eps/2) by psatzl R. rewrite Rabs_Ropp; apply Rplus_lt_compat; assumption. intros; apply ext; psatzl R. Qed. Lemma upInt_bound : forall a f g, (forall x, a <= x -> 0 <= f x <= g x) -> (forall x, a <= x -> Riemann_integrable f a x) -> up_infinite_integrable g a -> up_infinite_integrable f a. intros a f g fg ri upg. assert (h : forall n, a <= a + INR n). intros n; pattern a at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l, pos_INR. assert (grow : Un_growing (fun n => RiemannInt (ri _ (h n)))). intros n. assert (rinsn : Riemann_integrable f (a + INR n) (a + INR (S n))). apply RiemannInt_P23 with a;[exact (ri _ (h (S n))) | ]. assert (t:=pos_INR n); rewrite S_INR; psatzl R. rewrite <- (RiemannInt_P26 (ri _ (h n)) rinsn). assert (0 <= RiemannInt rinsn);[ | psatzl R]. replace 0 with (RiemannInt (RiemannInt_P14 (a + INR n) (a + INR (S n)) 0)). apply RiemannInt_P19. rewrite S_INR; psatzl R. intros x intx ; unfold fct_cte; apply fg; assert (t := h n); psatzl R. rewrite RiemannInt_P15, Rmult_0_l; reflexivity. assert {l | Un_cv (fun n => RiemannInt (ri _ (h n))) l} as [l Pl]. apply growing_cv;[assumption | ]. exists (upInt upg); intros v [n qv]; rewrite qv. assert (tmp := upg); destruct tmp as [hg _]. assert (hg' : Riemann_integrable g a (a + INR n)). destruct n as [ | n]. rewrite Rplus_0_r; apply RiemannInt_P7. rewrite S_INR; apply hg; assert (t := pos_INR n); psatzl R. assert (gan := up_infinite_integrable_break g a (a + INR n) upg hg'). rewrite <- (upInt_break g _ _ gan hg'). replace (RiemannInt (ri _ (h n))) with (RiemannInt (ri _ (h n)) + 0) by ring. apply Rplus_le_compat. apply RiemannInt_P19. auto. intros x intx; apply fg; psatzl R. apply upInt_ge_0. intros x ax; assert (t:= h n); assert (t' : a <= x) by psatzl R. assert (t'' := fg _ t'); psatzl R. assert (ri' : forall x, a < x -> Riemann_integrable f a x). intros x ax; apply ri; psatzl R. exists ri'; exists l; intros eps ep. assert (ep2 : 0 < eps/2) by psatzl R. destruct (up_integrable_vanish_Riemann g a upg _ ep2) as [Kv Pv]. destruct (Pl _ ep2) as [N Pn]. assert (exists N1, Kv <= a + INR N1 /\ (N <= N1)%nat) as [N1 [KN1 NN1]]. exists (N + Z.abs_nat (up (Rmax 0 (Kv - a))))%nat. split. destruct (archimed (Rmax 0 (Kv - a))) as [t _]. rewrite plus_INR, (INR_IZR_INZ (Z.abs_nat _)), Zabs2Nat.id_abs, Z.abs_eq. apply Rlt_le, Rle_lt_trans with (a + INR N + Rmax 0 (Kv - a));[ | psatzl R]. assert (t' := Rmax_r 0 (Kv - a)); assert (t'' := h N); psatzl R. assert (0 < up (Rmax 0 (Kv - a)))%Z;[|omega]. assert (IZR (up (Rmax 0 (Kv - a))) > IZR 0). simpl (IZR 0); assert (t' := Rmax_l 0 (Kv - a));psatzl R. apply lt_IZR; assumption. omega. exists (a + INR N1). intros b Kb h'. replace eps with (eps/2 + eps/2) by field. assert (aNb : Riemann_integrable f (a + INR N1) b). apply RiemannInt_P23 with a. apply ri'; assumption. split; assert (t' := pos_INR N1); psatzl R. replace (RiemannInt (ri' b h')) with (RiemannInt (ri _ (h N1)) + RiemannInt aNb) by apply RiemannInt_P26. unfold R_dist; rewrite Rplus_comm; unfold Rminus; rewrite Rplus_assoc. apply Rle_lt_trans with (1:= Rabs_triang _ _). apply Rplus_lt_compat;[ | apply Pn, NN1]. assert (ganb:Riemann_integrable g (a + INR N1) b). apply RiemannInt_P23 with a. destruct upg as [hg _]; apply hg; assumption. split; assert (t := Rmax_l a Kv); assert (t' := pos_INR N1); psatzl R. rewrite Rabs_pos_eq. apply Rle_lt_trans with (RiemannInt ganb). apply RiemannInt_P19. psatzl R. intros x intx; apply fg. assert (t := h N1); psatzl R. apply Rle_lt_trans with (1 := Rle_abs _), Pv. psatzl R. replace 0 with (RiemannInt (RiemannInt_P14 (a + INR N1) b 0)); [ | rewrite RiemannInt_P15, Rmult_0_l; reflexivity]. apply RiemannInt_P19;[psatzl R | ]. intros x intx; apply fg; assert (t := h N1); psatzl R. Qed. Lemma derivable_pt_lim_ext : forall f g x d, (forall y, f y = g y) -> derivable_pt_lim f x d -> derivable_pt_lim g x d. intros f g x d ext Pd eps ep; destruct (Pd _ ep) as [delta P']. exists delta; intros h hn0 hdelta; rewrite <- !ext; auto. Qed. Lemma RiemannInt_variable_change : forall f g g' a b (ab : a <= b) (h : Riemann_integrable (fun x => g' x * f (g x)) a b) (h' : Riemann_integrable f (g a) (g b)), (forall x, a <= x <= b -> derivable_pt_lim g x (g' x)) -> (forall x, a <= x <= b -> g a <= g x <= g b) -> (forall x, g a <= x <= g b -> continuity_pt f x) -> (forall x, a <= x <= b -> continuity_pt g' x) -> RiemannInt h = RiemannInt h'. intros f g g' a b ab h h' dr incr cf cg'. assert (gab : g a <= g b) by (assert (t := incr a); psatzl R). assert (pr : forall x, g a <= x -> x <= g b -> Riemann_integrable f (g a) x). intros x ax xb; apply RiemannInt_P22 with (g b); [ | psatzl R]. apply continuity_implies_RiemannInt; assumption || psatzl R. assert (t' : forall x, a <= x <= b -> continuity_pt (fun y => g' y * f (g y)) x). intros x intx; reg. apply derivable_continuous_pt. exists (g' x); apply dr; assumption. apply cf, incr; psatzl R. apply cg'; assumption. rewrite (RiemannInt_P20 gab pr). apply (antiderivative_Riemann (fun x => g' x * f (g x)) (fun x => primitive gab pr (g x)) a b ab t'). split;[ | assumption]. intros x intx. change (fun y => primitive gab pr (g y)) with (comp (primitive gab pr) g). assert (p0 : derivable_pt_lim (primitive gab pr) (g x) (f (g x))). apply (derivable_pt_lim_ext (primitive gab (FTC_P1 gab cf))). solve[apply primitive_ext]. apply RiemannInt_P28, incr; psatzl R. assert (p' : derivable_pt (primitive gab pr) (g x)). exists (f (g x)); apply p0. exists (derivable_pt_comp g _ x (exist _ _ (dr x intx)) p'). rewrite derive_pt_comp. rewrite (derive_pt_eq_0 _ _ _ p' p0); simpl; ring. Qed. (* (* TODO : the function primitive should not impose any order on the bounds. *) *) Lemma derivable_pt_lim_div_scal : forall f x l a, derivable_pt_lim f x l -> derivable_pt_lim (fun y => f y / a) x (l / a). intros f x l a df; apply (derivable_pt_lim_eq (fun y => /a * f y) _ _ (x - 1) (x + 1)). psatzl R. intros z _; rewrite Rmult_comm; reflexivity. unfold Rdiv; rewrite Rmult_comm; apply derivable_pt_lim_scal; assumption. Qed. Lemma derivable_pt_lim_scal_right : forall f x l a, derivable_pt_lim f x l -> derivable_pt_lim (fun y => f y * a) x (l * a). intros f x l a df; apply (derivable_pt_lim_eq (fun y => a * f y) _ _ (x - 1) (x + 1)). psatzl R. intros z _; rewrite Rmult_comm; reflexivity. unfold Rdiv; rewrite Rmult_comm; apply derivable_pt_lim_scal; assumption. Qed. Lemma Riemann_integrable_scal : forall f a b k, Riemann_integrable f a b -> Riemann_integrable (fun x => k * f x) a b. intros f a b k ri. apply Riemann_integrable_eq with (f := fun x => 0 + k * f x). intros; ring. apply (RiemannInt_P10 _ (RiemannInt_P14 _ _ 0) ri). Qed. Arguments Riemann_integrable_scal [f a b] k _ eps. Lemma RiemannInt_scal : (* TODO : find usages for this theorem *) forall f a b k (h : Riemann_integrable f a b) (h' : Riemann_integrable (fun x => k * f x) a b), RiemannInt h' = k * RiemannInt h. intros; destruct (Rle_dec a b). rewrite (RiemannInt_P18 h' (RiemannInt_P10 k (RiemannInt_P14 _ _ 0) h)); [ | assumption | unfold fct_cte; intros; ring ]. rewrite (RiemannInt_P13 (RiemannInt_P14 a b 0) h). rewrite RiemannInt_P15, Rmult_0_l, Rplus_0_l; reflexivity. rewrite (RiemannInt_P8 h' (RiemannInt_P1 h')), (RiemannInt_P8 h (RiemannInt_P1 h)), Ropp_mult_distr_r_reverse. apply f_equal. rewrite (RiemannInt_P18 (RiemannInt_P1 h') (RiemannInt_P10 k (RiemannInt_P14 _ _ 0) (RiemannInt_P1 h))); [ | psatzl R | unfold fct_cte; intros; ring ]. rewrite (RiemannInt_P13 (RiemannInt_P14 b a 0) (RiemannInt_P1 h)). rewrite RiemannInt_P15, Rmult_0_l, Rplus_0_l; reflexivity. Qed. Lemma Riemann_integrable_Ropp : forall f a b, Riemann_integrable f a b -> Riemann_integrable (fun x => - f x) a b. intros ff a b h. apply Riemann_integrable_eq with (f := fun x => (-1) * ff x). intros; ring. apply Riemann_integrable_scal; assumption. Qed. Arguments Riemann_integrable_Ropp [f a b] _ eps. Lemma RiemannInt_Ropp : forall f a b (h : Riemann_integrable f a b), -RiemannInt h = RiemannInt (Riemann_integrable_Ropp h). intros ff a b h. destruct (Rle_dec a b). rewrite (RiemannInt_P18 (Riemann_integrable_Ropp h) (Riemann_integrable_scal (-1) h)); [rewrite (RiemannInt_scal _ _ _ _ h) | assumption | intros ]; ring. rewrite (RiemannInt_P8 h (RiemannInt_P1 h)). rewrite (RiemannInt_P8 (Riemann_integrable_Ropp h) (RiemannInt_P1 (Riemann_integrable_Ropp h))). apply f_equal. rewrite (RiemannInt_P18 (RiemannInt_P1 (Riemann_integrable_Ropp h)) (RiemannInt_P1 (Riemann_integrable_scal (-1) h))); [rewrite (RiemannInt_scal _ _ _ _ (RiemannInt_P1 h)) | psatzl R | intros ]; ring. Qed. Lemma RiemannInt_variable_change1 : forall f g g' a b (ab : a <= b) (h : Riemann_integrable (fun x => g' x * f (g x)) a b) (h' : Riemann_integrable f (g a) (g b)), (forall x, a <= x <= b -> derivable_pt_lim g x (g' x)) -> (forall x, a <= x <= b -> Rmin (g a) (g b) <= g x <= Rmax (g a) (g b)) -> (forall x, Rmin (g a) (g b) <= x <= Rmax (g a) (g b) -> continuity_pt f x) -> (forall x, a <= x <= b -> continuity_pt g' x) -> RiemannInt h = RiemannInt h'. intros f g g' a b ab h h' dr incr cf cg'. assert (pr : forall x, Rmin (g a) (g b) <= x -> x <= Rmax (g a) (g b) -> Riemann_integrable f (Rmin (g a) (g b)) x). intros x ax xb; apply RiemannInt_P22 with (Rmax (g a) (g b)); [ | psatzl R]. apply continuity_implies_RiemannInt; try assumption. apply Rminmax. assert (t' : forall x, a <= x <= b -> continuity_pt (fun y => g' y * f (g y)) x). intros x intx; reg. apply derivable_continuous_pt. exists (g' x); apply dr; assumption. apply cf, incr; psatzl R. apply cg'; assumption. destruct (Rle_dec (g a) (g b)) as [gab | gnab]. revert pr cf incr; rewrite Rmin_left, Rmax_right; try assumption. intros pr cf incr; rewrite (RiemannInt_P20 gab pr). apply (antiderivative_Riemann (fun x => g' x * f (g x)) (fun x => primitive gab pr (g x)) a b ab t'). split;[ | assumption]. intros x intx. change (fun y => primitive gab pr (g y)) with (comp (primitive gab pr) g). assert (p0 : derivable_pt_lim (primitive gab pr) (g x) (f (g x))). apply (derivable_pt_lim_ext (primitive gab (FTC_P1 gab cf))). solve[apply primitive_ext]. apply RiemannInt_P28, incr; psatzl R. assert (p' : derivable_pt (primitive gab pr) (g x)). exists (f (g x)); apply p0. exists (derivable_pt_comp g _ x (exist _ _ (dr x intx)) p'). rewrite derive_pt_comp. rewrite (derive_pt_eq_0 _ _ _ p' p0); simpl; ring. assert (gba : g b <= g a) by psatzl R. revert pr cf incr; rewrite Rmin_right, Rmax_left; try assumption. intros pr cf incr; rewrite (RiemannInt_P8 h' (RiemannInt_P1 h')). rewrite (RiemannInt_P20 gba pr), Ropp_minus_distr, Rplus_comm. apply (antiderivative_Riemann (fun x => g' x * f (g x)) (fun x => primitive gba pr (g x)) a b ab t'). split;[ | assumption]. intros x intx. change (fun y => primitive gba pr (g y)) with (comp (primitive gba pr) g). assert (p0 : derivable_pt_lim (primitive gba pr) (g x) (f (g x))). apply (derivable_pt_lim_ext (primitive gba (FTC_P1 gba cf))). solve[apply primitive_ext]. apply RiemannInt_P28, incr; psatzl R. assert (p' : derivable_pt (primitive gba pr) (g x)). exists (f (g x)); apply p0. exists (derivable_pt_comp g _ x (exist _ _ (dr x intx)) p'). rewrite derive_pt_comp. rewrite (derive_pt_eq_0 _ _ _ p' p0); simpl; ring. Qed. Lemma RiemannInt_variable_change' : forall f f2 g g' a b (ab : a <= b) (h : Riemann_integrable f2 a b) (h': Riemann_integrable f (g a) (g b)), (forall x, a <= x <= b -> derivable_pt_lim g x (g' x)) -> (forall x, a <= x <= b -> g a <= g x <= g b) -> (forall x, g a <= x <= g b -> continuity_pt f x) -> (forall x, a <= x <= b -> continuity_pt g' x) -> (forall x, a <= x <= b -> f2 x = g' x * f (g x)) -> RiemannInt h = RiemannInt h'. intros f f2 g g' a b ab ri2 ri' der int ct derct eq. assert (hc : Riemann_integrable (fun x => g' x * f (g x)) a b). apply Riemann_integrable_eq with (2 := ri2). intros x; rewrite Rmin_left, Rmax_right; try psatzl R; solve[apply eq]. rewrite <- (RiemannInt_variable_change _ _ _ _ _ ab hc ri' der int ct derct). apply RiemannInt_P18;[assumption | intros; apply eq; psatzl R]. Qed. Lemma RiemannInt_variable_change1' : forall f f2 g g' a b (ab : a <= b) (h : Riemann_integrable f2 a b) (h' : Riemann_integrable f (g a) (g b)), (forall x, a <= x <= b -> derivable_pt_lim g x (g' x)) -> (forall x, a <= x <= b -> Rmin (g a) (g b) <= g x <= Rmax (g a) (g b)) -> (forall x, Rmin (g a) (g b) <= x <= Rmax (g a) (g b) -> continuity_pt f x) -> (forall x, a <= x <= b -> continuity_pt g' x) -> (forall x, a <= x <= b -> f2 x = g' x * f (g x)) -> RiemannInt h = RiemannInt h'. intros f f2 g g' a b ab ri2 ri' der int ct derct eq. assert (eq' : forall x, Rmin a b <= x <= Rmax a b -> f2 x = g' x * f (g x)). rewrite Rmin_left, Rmax_right; assumption. assert (hc : Riemann_integrable (fun x => g' x * f (g x)) a b). apply Riemann_integrable_eq with (1 := eq') (2 := ri2). rewrite <- (RiemannInt_variable_change1 _ _ _ _ _ ab hc ri' der int ct derct). apply RiemannInt_P18;[assumption | ]. intros; apply eq; psatzl R. Qed. (* Starting the work on algebraic geometric means. *) Fixpoint ag (a b : R) (n : nat) := match n with 0%nat => (a, b) | S p => let (a_p, b_p) := ag a b p in ((a_p + b_p)/2, sqrt(a_p * b_p)) end. Definition f_ (n : nat) (x : R) := ag 1 x n. Lemma q1_1_aux : forall a b, 0 <= b <= a -> b <= sqrt (a * b) <= (a + b)/2 /\ (a + b)/2 <= a. intros a b [b0 ba]. assert (tmp : 0 <= Rsqr (sqrt a - sqrt b)) by apply Rle_0_sqr. revert tmp; rewrite Rsqr_minus, !Rsqr_sqrt;[ | psatzl R | psatzl R]. rewrite Rmult_assoc, <- sqrt_mult_alt;[ | psatzl R]. intros tmp; split;[split;[ | psatzl R ] | psatzl R]. rewrite sqrt_mult_alt;[ | psatzl R]. pattern b at 1; rewrite <- (Rsqr_sqrt b);[ | psatzl R]; unfold Rsqr. apply Rmult_le_compat_r;[apply sqrt_pos | apply sqrt_le_1_alt; assumption]. Qed. Lemma q1_1_aux2 : forall a b, 0 <= b <= a -> a <> b -> sqrt (a * b) <> (a + b)/2. intros a b [b0 ba] anb. assert (sqrt b < sqrt a) by (apply sqrt_lt_1_alt; psatzl R). assert (sqrt a - sqrt b <> 0) by psatzl R. assert (tmp : 0 < Rsqr (sqrt a - sqrt b)) by (apply Rlt_0_sqr; assumption). revert tmp; rewrite Rsqr_minus, Rmult_assoc, <- sqrt_mult_alt;[ | psatzl R]. rewrite !Rsqr_sqrt;psatzl R. Qed. (* Error in the subject. *) Lemma diff_ag : forall a b, 0 <= b <= a -> (a + b)/2 - sqrt (a * b) <= (a - b)/2. intros a b [b0 ba]. pattern a at 1 3; rewrite <- (Rsqr_sqrt a);[ | psatzl R]. pattern b at 1 3; rewrite <- (Rsqr_sqrt b);[ | psatzl R]. rewrite sqrt_mult_alt;[ | psatzl R]. apply Rmult_le_reg_l with 2;[psatzl R | ]. unfold Rdiv; rewrite Rmult_minus_distr_l, !(Rmult_comm 2), !Rmult_assoc. rewrite !Rinv_l, !Rmult_1_r; try psatzl R. rewrite <- Rmult_assoc, <- (Rmult_comm 2), <- Rmult_assoc. rewrite <- Rsqr_minus. rewrite <- Rsqr_plus_minus; unfold Rsqr. apply Rmult_le_compat_r. assert (sqrt b <= sqrt a) by (apply sqrt_le_1_alt; psatzl R); psatzl R. assert (0 <= sqrt b) by apply sqrt_pos; psatzl R. Qed. Lemma ag_positive : forall n a b, 0 < a -> 0 < b -> 0 < fst (ag a b n) /\ 0 < snd (ag a b n). induction n. intros a b; simpl; tauto. intros a b a0 b0; simpl. generalize (IHn a b a0 b0); destruct (ag a b n) as [v1 v2]; simpl. intros [v1_0 v2_0]; split;[psatzl R | ]. apply sqrt_lt_R0, Rmult_lt_0_compat; assumption. Qed. Lemma ag_comm : forall a b n, (1 <= n)%nat -> ag a b n = ag b a n. intros a b n n1; induction n1. simpl; rewrite Rmult_comm, Rplus_comm; reflexivity. simpl; rewrite IHn1; reflexivity. Qed. Lemma q1_1_1 : forall a b n, 0<= a -> 0 <= b -> a <> b -> (1 <= n)%nat -> 0 <= snd (ag a b n) <= snd (ag a b (n + 1)) /\ snd (ag a b (n + 1)) < fst (ag a b (n + 1)) <= fst (ag a b n) /\ fst (ag a b (n + 1)) - snd (ag a b (n + 1)) <= (fst (ag a b n) - snd (ag a b n))/2. intros a b n a0 b0 anb H; induction H. change (snd (ag a b (1 + 1))) with (sqrt (fst (ag a b 1) * snd (ag a b 1))). change (fst (ag a b (1 + 1))) with ((fst (ag a b 1) + snd (ag a b 1))/2). revert a0 b0 anb; pattern a, b. (* wlog : a <= b *) match goal with |- ?F a b => assert (wlog : forall c d, d <= c -> F c d); [clear a b; intros a b ab a0 b0 anb | case (Rle_dec b a); [intros ba; apply (wlog a b ba) | intros ab' a0 b0 anb; assert (ab : a <= b) by psatzl R; rewrite !(ag_comm a); try (apply le_n); apply (wlog b a ab b0 a0 (not_eq_sym anb))]] end. destruct (q1_1_aux a b (conj b0 ab)) as [[H1 H2] H3]. assert (H4 := q1_1_aux2 a b (conj b0 ab) anb). destruct (q1_1_aux ((a + b)/2) (sqrt (a * b))) as [[H5 H6] H7]; [split;[apply sqrt_pos | tauto ] | ]. assert (H8 := q1_1_aux2 ((a + b)/2) (sqrt (a * b)) (conj (sqrt_pos _) H2) (not_eq_sym H4)). simpl; intuition; psatzl R. rewrite plus_comm in IHle; simpl in IHle. rewrite plus_comm; simpl; destruct (ag a b m) as [a' b']; simpl in IHle |- *. assert (tmp' : 0 <= b' <= a') by psatzl R. assert (tmp := q1_1_aux a' b' tmp'). assert (tmp'' : 0 <= sqrt (a' * b') <= (a' + b')/2) by psatzl R. assert (tmp2 := q1_1_aux _ _ tmp''). assert (tmp3 := q1_1_aux2 _ _ tmp'). assert (tmp4 := q1_1_aux2 _ _ tmp''). psatzl R. Qed. Lemma q1_1_1' : forall a n, 0 <= a -> ag a a n = (a, a). intros a n a0; induction n;[reflexivity | ]. simpl; rewrite IHn; simpl. assert (H' : (a + a)/2 = a) by psatzl R; rewrite H'; apply f_equal. apply sqrt_Rsqr; assumption. Qed. Lemma ag_unfold : forall a b n, ag a b (S n) = ((fst (ag a b n) + snd (ag a b n))/2, sqrt (fst (ag a b n) * (snd (ag a b n)))). intros a b n; simpl; destruct (ag a b n); simpl; reflexivity. Qed. Lemma q1_1_1_cor : forall a b n, 0 < a -> 0 < b -> b < a -> snd (ag a b n) <= fst (ag a b n). intros a b n a0 b0 ba. destruct n as [ | n]. solve[apply Rlt_le, ba]. rewrite ag_unfold. assert (t := ag_positive n a b a0 b0). destruct (ag a b n) as [a' b']; simpl in t |- *. destruct (Rle_dec b' a') as [b'a' | a'b']. destruct (q1_1_aux a' b' (conj (Rlt_le _ _ (proj2 t)) b'a')); psatzl R. assert (t' : a' <= b') by psatzl R. destruct (q1_1_aux b' a' (conj (Rlt_le _ _ (proj1 t)) t')). rewrite Rplus_comm, Rmult_comm; psatzl R. Qed. Lemma an_decreasing : forall a b, 0 <= a -> 0 <= b -> Un_decreasing (fun n => fst (ag a b (n + 1))). intros a b a0 b0. destruct (Req_EM_T a b) as [ab | anb]. rewrite ab; intros n; rewrite !q1_1_1'; psatzl R. intros n; replace (S n) with (n + 1)%nat by ring. assert (t : (1 <= n + 1)%nat) by omega. assert (tmp := q1_1_1 a b (n + 1) a0 b0 anb t). tauto. Qed. Lemma cv_an : forall a b, 0 <= a -> 0 <= b -> {l : R | Un_cv (fun n => fst (ag a b n)) l}. intros a b a0 b0. destruct (Req_EM_T a b) as [ab | anb]. exists b; exists 0%nat; intros; rewrite ab, q1_1_1', ?R_dist_eq; assumption. assert {l | Un_cv (fun n => fst (ag a b (n + 1))) l}. apply decreasing_cv. intros n; replace (S n) with (n + 1)%nat by ring. assert (tmp := q1_1_1 a b (n + 1) a0 b0 anb); assert (tmp' : (1 <= n + 1)%nat) by omega. tauto. exists (- snd (ag a b 1)). apply Un_bound_imp; unfold opp_seq; intros n; apply Ropp_le_contravar. assert (H:snd (ag a b 1) <= snd (ag a b (n + 1)) <= fst (ag a b (n + 1))); [ | psatzl R]. induction n. assert (tmp := q1_1_1 a b 1 a0 b0 anb (le_n _)); simpl in tmp |- *; psatzl R. assert (t : (1 <= n + 1)%nat) by omega. assert (tmp := q1_1_1 a b (n + 1) a0 b0 anb t). replace (S n + 1)%nat with (n + 1 + 1)%nat by ring. psatzl R. destruct H as [l Pl]; exists l; apply CV_shift with 1%nat; assumption. Qed. Lemma bn_growing : forall a b, 0 <= a -> 0 <= b -> Un_growing (fun n => snd (ag a b (n + 1))). intros a b a0 b0 n; replace (S n) with (n + 1)%nat by ring. case (Req_EM_T a b) as [ab | anb]. rewrite ab, !q1_1_1'; psatzl R. assert (tmp := q1_1_1 a b (n + 1) a0 b0 anb). assert (tmp' : (1 <= n + 1)%nat) by omega. tauto. Qed. Lemma cv_bn : forall a b, 0 <= a -> 0 <= b -> {l : R | Un_cv (fun n => snd (ag a b n)) l}. intros a b a0 b0. destruct (Req_EM_T a b) as [ab | anb]. exists a; intros e ep; exists 0%nat; intros n _; rewrite <- ab, q1_1_1'; [ | assumption]. unfold R_dist, Rminus; rewrite Rplus_opp_r, Rabs_R0; assumption. assert {l | Un_cv (fun n => snd (ag a b (n + 1))) l}. apply growing_cv;[apply bn_growing; assumption | ]. exists (fst (ag a b 1)). apply Un_bound_imp; intros n. assert (H:snd (ag a b (n + 1)) <= fst (ag a b (n + 1)) <= fst (ag a b 1)); [ | psatzl R]. induction n. assert (tmp := q1_1_1 a b 1 a0 b0 anb (le_n _)); simpl in tmp |- *; psatzl R. assert (t : (1 <= n + 1)%nat) by omega. assert (tmp := q1_1_1 a b (n + 1) a0 b0 anb t). replace (S n + 1)%nat with (n + 1 + 1)%nat by ring. psatzl R. destruct H as [l Pl]; exists l; apply CV_shift with 1%nat; assumption. Qed. Lemma cv_div2 : forall a, Un_cv (fun n => a/2^n) 0. intros a; unfold Rdiv; replace 0 with (a * 0) by ring. apply CV_mult. intros eps ep; exists 0%nat; rewrite R_dist_eq; intros n _; assumption. exact (cv_infty_cv_R0 pow_2_n pow_2_n_neq_R0 pow_2_n_infty). Qed. Lemma ag_diff_maj : forall a b n, (1 <= n)%nat -> 0 <= a -> 0 <= b -> 0 <= fst (ag a b n) - snd (ag a b n) <= Rabs (a - b)/(2 ^ n). intros a b n n1 a0 b0; simpl; case (Req_dec a b) as [ab | anb]. unfold Rminus, Rdiv. rewrite ab, q1_1_1', !Rplus_opp_r, Rabs_R0, Rmult_0_l; simpl; auto; psatzl R. split. assert (tmp:= q1_1_1 _ _ n a0 b0 anb n1); psatzl R. induction n1. destruct (Rle_dec b a) as [bla | alb]. simpl; rewrite Rmult_1_r, Rabs_pos_eq;[ | psatzl R]. apply diff_ag; psatzl R. simpl; rewrite Rplus_comm, Rmult_comm, Rabs_left;[ | psatzl R]. rewrite Ropp_minus_distr, (Rplus_comm (- _)), Rmult_1_r; apply diff_ag; psatzl R. assert (tmp : 0 <= snd (ag a b m) <= fst (ag a b m)). assert (t := q1_1_1 a b m a0 b0 anb n1); simpl in t. generalize (diff_ag (fst (ag a b m)) (snd (ag a b m))); psatzl R. simpl; destruct (ag a b m) as [a' b']; simpl in IHn1, tmp |- *. apply Rle_trans with (1 := diff_ag a' b' tmp). apply Rmult_le_reg_r with 2; unfold Rdiv; [psatzl R | ]. rewrite Rmult_assoc, Rinv_l, Rmult_1_r;[|psatzl R]. apply Rle_trans with (1 := IHn1), Req_le; field; apply pow_nonzero; psatzl R. Qed. Lemma q1_1_2 : forall a b, 0 <= a -> 0 <= b -> {l : R | Un_cv (fun n => fst (ag a b n)) l /\ Un_cv (fun n => snd (ag a b n)) l}. intros a b a0 b0. destruct (Req_EM_T a b) as [ab | anb]. exists a;split; exists 0%nat; intros n _; rewrite ab, q1_1_1'; try psatzl R; simpl; rewrite R_dist_eq; assumption. destruct (cv_an a b a0 b0) as [l1 cv1]; destruct (cv_bn a b a0 b0) as [l2 cv2]. exists l1; split;[assumption | assert (tmp: l1 = l2);[ | rewrite tmp; assumption]]. apply Rminus_diag_uniq, (UL_sequence (fun n => fst (ag a b n) - snd (ag a b n))). apply CV_minus; assumption. intros eps ep; destruct (cv_div2 (Rabs (a - b)) eps ep) as [N Pn]. exists (N + 1)%nat; intros n nN; assert ((n >= N)%nat /\ (1 <= n)%nat) as [nN' n1] by omega. apply Rle_lt_trans with (2 := Pn n nN'). unfold R_dist; rewrite !Rminus_0_r, Rabs_pos_eq, Rabs_pos_eq; [ | apply Rmult_le_pos; [apply Rabs_pos | apply Rlt_le, Rinv_0_lt_compat, pow_lt; psatzl R] | assert (tmp := q1_1_1 a b n a0 b0 anb n1); psatzl R]. apply ag_diff_maj; assumption. Qed. Definition M (a b : R) : R := match (Rle_dec 0 a) with left a0 => match Rle_dec 0 b with left b0 => let (v, _) := q1_1_2 a b a0 b0 in v | right _ => b end | right _ => b end. Lemma M_def : forall a b, 0 <= a -> 0 <= b -> Un_cv (fun n => fst (ag a b n)) (M a b). intros a b a0 b0; unfold M. destruct (Rle_dec 0 a) as [a0' | ?];[ | psatzl R]. destruct (Rle_dec 0 b) as [b0' | ?];[ | psatzl R]. destruct (q1_1_2 a b a0' b0') as [v [P1 P2]]; assumption. Qed. Lemma M_def' : forall a b, 0 <= a -> 0 <= b -> Un_cv (fun n => snd (ag a b n)) (M a b). intros a b a0 b0; unfold M. destruct (Rle_dec 0 a) as [a0' | ?];[ | psatzl R]. destruct (Rle_dec 0 b) as [b0' | ?];[ | psatzl R]. destruct (q1_1_2 a b a0' b0') as [v [P1 P2]]; assumption. Qed. Definition ff x := M 1 x. Lemma ag_shift : forall a b n p, ag (fst (ag a b n)) (snd (ag a b n)) p = ag a b (n + p). intros a b n; induction p. rewrite plus_0_r; simpl; rewrite <- surjective_pairing; reflexivity. rewrite <- plus_n_Sm; simpl; rewrite IHp; reflexivity. Qed. Lemma q1_2_1 : forall a b n, 0 <= a -> 0 <= b -> M (fst (ag a b n)) (snd (ag a b n)) = M a b. intros a b n a0 b0. destruct (Req_EM_T a b) as [ab | anb]. rewrite ab, q1_1_1'; solve[trivial]. assert (0 <= fst (ag a b n) /\ 0 <= snd (ag a b n)) as [t1 t2]. destruct n as [ | n]. simpl; tauto. replace (S n) with (n + 1)%nat by ring. assert (t' : (1 <= n + 1)%nat) by omega. assert (tm := q1_1_1 a b (n + 1) a0 b0 anb t'); psatzl R. apply UL_sequence with (fun i => fst (ag (fst (ag a b n)) (snd (ag a b n)) i)). apply (M_def _ _ t1 t2). apply (Un_cv_ext (fun i => fst (ag a b (i + n)))). intros; rewrite ag_shift, plus_comm; reflexivity. assert (t3 := M_def _ _ a0 b0). apply (CV_shift' (fun i => fst (ag a b i))); assumption. Qed. Lemma q1_2_2 : forall a b, 0 <= a -> 0 <= b -> M a b = M b a. intros a b a0 b0. apply (UL_sequence _ _ _ (M_def a b a0 b0)). apply (CV_shift _ 1), (Un_cv_ext (fun i => fst (ag b a (i + 1)))). intros n; apply f_equal, ag_comm; omega. apply (CV_shift' _ 1 _ (M_def b a b0 a0)). Qed. Lemma ag_scal : forall a b c n, 0 <= a -> 0 <= b -> 0 <= c -> fst (ag (c * a) (c * b) n) = c * fst (ag a b n) /\ snd (ag (c * a) (c * b) n) = c * snd (ag a b n). intros a b c n a0 b0 c0; induction n. split; reflexivity. simpl; destruct (ag (c * a) (c * b) n) as [a' b']. destruct (ag a b n) as [a'' b'']; simpl in IHn |- *. destruct IHn as [IHn1 IHn2]. rewrite IHn1, IHn2;split;[psatzl R | ]. replace (c * a'' * (c * b'')) with (Rsqr c * (a'' * b'')) by (unfold Rsqr; ring). rewrite sqrt_mult_alt;[rewrite sqrt_Rsqr; auto | apply Rle_0_sqr]. Qed. Lemma q1_2_3 : forall a b c, 0 <= a -> 0 <= b -> 0 <= c -> M (c * a) (c * b) = c * M a b. intros a b c a0 b0 c0. assert (t1 : 0 <= c * a) by (apply Rmult_le_pos; assumption). assert (t2 : 0 <= c * b) by (apply Rmult_le_pos; assumption). assert (tt := M_def _ _ t1 t2). apply (UL_sequence (fun n => fst (ag (c * a) (c * b) n))). assumption. apply (Un_cv_ext (fun n => c * fst (ag a b n))). intros n; apply sym_equal, ag_scal; solve[auto]. apply (CV_mult (fun n => c) (fun n => fst (ag a b n))). intros eps ep; exists 0%nat; intros n _; rewrite R_dist_eq; assumption. apply M_def; assumption. Qed. Lemma q1_2_4 : forall a b, 0 < a -> 0 <= b -> M a b = a * ff (b / a). intros a b a0 b0; unfold ff. assert (0 < / a) by (apply Rinv_0_lt_compat; assumption). replace 1 with (a / a) by (field; apply Rgt_not_eq; assumption). unfold Rdiv; rewrite <- !(Rmult_comm (/a)), q1_2_3; try psatzl R. rewrite <- Rmult_assoc, Rinv_r; psatzl R. Qed. Definition ball_in_01 (x : R) : 0 < x < 1 -> {r | 0 < r /\ 0 < x - r /\ x + r < 1}. intros int; exists (Rmin x (1 -x)/2). assert (0 < /2) by (apply Rinv_0_lt_compat; psatzl R). split. apply Rmult_lt_0_compat;[ | assumption]. apply Rgt_lt; rewrite Rmin_Rgt; psatzl R. assert (Rmin x (1 - x)/2 <= x/2). apply Rmult_le_compat_r;[psatzl R | apply Rmin_l]. assert (Rmin x (1 - x)/2 <= (1 - x)/2). apply Rmult_le_compat_r;[psatzl R | apply Rmin_r]. split;psatzl R. Qed. Lemma continuity_pt_eq : (*duplicate from pi.v *) forall f g a x, 0 < a -> (forall y, R_dist y x < a -> f y = g y) -> continuity_pt f x -> continuity_pt g x. intros f g a x a0 q cf eps ep. destruct (cf eps ep) as [a' [a'p Pa']]. exists (Rmin a a'); split. unfold Rmin; destruct (Rle_dec a a'). assumption. assumption. intros y cy; rewrite <- !q. apply Pa'. split;[| apply Rlt_le_trans with (Rmin a a');[ | apply Rmin_r]];tauto. rewrite R_dist_eq; assumption. apply Rlt_le_trans with (Rmin a a');[ | apply Rmin_l]; tauto. Qed. Definition u_ (n : nat) (x : R) := fst (ag 1 x n). Lemma q1_3_1 : forall x n, 0 < x -> continuity_pt (u_ n) x. intros x n int; unfold u_; assert (continuity_pt (fun y => fst (ag 1 y n)) x /\ continuity_pt (fun y => snd (ag 1 y n)) x);[ | tauto]. induction n. simpl. split. intros eps ep; (* destruct (ball_in_01 x int) as [alpha Pa]. *) set (alpha := x/2);assert (alpha = x/2) by reflexivity. exists alpha; split;[psatzl R | ]. intros y _; unfold R_met; simpl; try rewrite R_dist_eq; assumption. intros eps ep; set (alpha := x/2); assert (alpha = x/2) by reflexivity. exists (Rmin alpha eps); split. rewrite Rmin_Rgt; psatzl R. unfold R_met; simpl; intros y [_ yx]; apply Rlt_le_trans with (1 := yx). solve[apply Rmin_r]. split. apply (continuity_pt_eq (fun y => (/2) * (fst (ag 1 y n) + snd (ag 1 y n))) _ 1 _ Rlt_0_1). intros y _; simpl; destruct (ag 1 y n); simpl; field. apply (continuity_pt_scal (fun y => fst (ag 1 y n) + snd (ag 1 y n)) (/2) x). apply continuity_pt_plus; tauto. apply (continuity_pt_eq (fun y => sqrt (fst (ag 1 y n) * snd (ag 1 y n))) _ 1 _ Rlt_0_1). intros y _; simpl; destruct (ag 1 y n); simpl; reflexivity. apply (continuity_pt_comp _ sqrt). apply continuity_pt_mult; tauto. apply continuity_pt_sqrt. destruct (Req_EM_T x 1) as [x1 | xn1]. rewrite x1, q1_1_1', Rmult_1_l; apply Rlt_le, Rlt_0_1. destruct n as [ | n]. simpl; rewrite Rmult_1_l; psatzl R. assert (t : (1 <= S n)%nat) by omega. assert (tmp:= q1_1_1 1 x (S n) (Rlt_le _ _ Rlt_0_1) (Rlt_le _ _ int) (sym_not_equal xn1) t). apply Rmult_le_pos; psatzl R. Qed. Lemma q1_3_2 : forall n x, (1 <= n)%nat -> 0 <= x -> 0 <= u_ n x - ff x <= Rabs(1 - x)/2^n. intros n x n1 x0; unfold u_. assert (t' := Rlt_le _ _ Rlt_0_1). assert (tmp := ag_diff_maj 1 x n n1 t' x0). assert (t1 := CV_shift' _ 1 (ff x) (M_def' 1 x t' x0)). assert (t := growing_ineq _ (ff x) (bn_growing 1 x t' x0) t1 (n - 1)). assert (snd (ag 1 x n) <= ff x). apply Rle_trans with (2 := t). replace (n - 1 + 1)%nat with n by omega; apply Rle_refl. split;[ | psatzl R]. assert (t2 := CV_shift' _ 1 (ff x) (M_def 1 x t' x0)). assert (t3 := decreasing_ineq _ (ff x) (an_decreasing 1 x t' x0) t2 (n - 1)). assert (ff x <= fst (ag 1 x n));[ | psatzl R]. apply Rle_trans with (1 := t3). replace (n - 1 + 1)%nat with n by omega; apply Rle_refl. Qed. Lemma cvu_u_ff : forall x (x0 : 0 < x), CVU u_ ff x (pos_div_2 (mkposreal x x0)). intros x x0. intros eps ep; destruct (cv_div2 (Rmax (Rabs (1 - 3/2 * x)) (Rabs (1 - x / 2))) eps ep) as [N Pn]. exists (N + 1)%nat; intros n y Nn dyx. assert (n1 : (1 <= n)%nat) by omega. unfold Boule in dyx; apply Rabs_lt_between in dyx; unfold pos_div_2, pos in dyx. assert (y0 : 0 <= y) by psatzl R. destruct (q1_3_2 n y n1 y0) as [difpos difbound]. rewrite <- Rabs_Ropp, Rabs_pos_eq, Ropp_minus_distr';[ | psatzl R]. apply Rle_lt_trans with (1 := proj2 (q1_3_2 n y n1 y0)). assert (Nn' : (n >= N)%nat) by lia. assert (Pn' := Pn n Nn'); unfold R_dist in Pn'. apply Rabs_lt_between in Pn'; rewrite Rminus_0_r in Pn'. destruct Pn' as [_ Pn2]. apply Rlt_trans with (2 := Pn2), Rmult_lt_compat_r;[lt0 | ]. unfold Rmax; case (Rle_dec (Rabs (1 - 3/2 * x)) (Rabs (1 - x /2))); unfold Rabs; destruct (Rcase_abs (1 - 3/2 * x)); destruct (Rcase_abs (1 - x/2)); destruct (Rcase_abs (1 - y));try psatzl R. Qed. Lemma q1_3_3 : forall x, 0 < x -> continuity_pt ff x. intros x x0; assert (d2 : 0 < x/2) by psatzl R. set (delta := mkposreal _ d2). assert (ctu : forall n y, Boule x delta y -> continuity_pt (u_ n) y). intros n y dyx; apply q1_3_1; unfold Boule, delta, pos in dyx. apply Rabs_lt_between in dyx; psatzl R. apply (CVU_continuity u_ ff x delta (cvu_u_ff x x0) ctu), Boule_center. Qed. Lemma q2_body_bound : forall a b x, (a * b) ^ 2 <= (x ^ 2 + a ^ 2) * (x ^ 2 + b ^ 2). intros a b x; replace ((a * b) ^ 2) with (a ^ 2 * b ^ 2) by ring. apply Rmult_le_compat; try apply pow2_ge_0; assert (t := pow2_ge_0 x); psatzl R. Qed. Lemma q2_body_pos : forall a b x, 0 < a -> 0 < b -> 0 < (x ^ 2 + a ^ 2) * (x ^ 2 + b ^ 2). intros; apply Rlt_le_trans with (2 := q2_body_bound _ _ _). apply pow_lt, Rmult_lt_0_compat; assumption. Qed. Lemma q2_1_1 : forall a b, 0 < a -> 0 < b -> up_infinite_integrable (fun t => /sqrt ((t^2 + a^2) * (t^2 + b^2))) 0. intros a b a0 b0. assert (pv : forall x, 0 <= x -> 0 < (x ^ 2 + a ^ 2) * (x ^ 2 + b ^ 2)). intros x x1; apply q2_body_pos; auto. apply up_infinite_integrable_break with 1. apply (upInt_bound _ _ (fun t => /Rpower t 2)). intros x x1. split. apply Rlt_le, Rinv_0_lt_compat, sqrt_lt_R0, pv; psatzl R. apply Rle_Rinv. apply exp_pos. apply sqrt_lt_R0, pv; psatzl R. change 2 with (INR 2); rewrite Rpower_pow;[|psatzl R]. apply Rle_trans with (sqrt (x^2 * x^2)). rewrite sqrt_square;[apply Rle_refl | apply pow2_ge_0 ]. assert (t : forall x y, x ^ 2 <= x ^ 2 + y ^ 2). intros u v; assert (t' := pow2_ge_0 v); psatzl R. apply sqrt_le_1_alt, Rmult_le_compat; try apply pow2_ge_0; apply t. intros x x1; apply continuity_implies_RiemannInt;[assumption | ]. intros y inty; reg. apply Rlt_le, pv; psatzl R. apply Rgt_not_eq, sqrt_lt_R0, pv; psatzl R. apply up_infinite_integrable_ext with (fun t => Rpower t (-2)). intros x x1; rewrite Rpower_Ropp; reflexivity. apply up_infinite_integrable_Rpower; psatzl R. apply RiemannInt_P1, continuity_implies_RiemannInt;[psatzl R | ]. intros x intx; reg. apply Rlt_le, pv; psatzl R. apply Rgt_not_eq, sqrt_lt_R0, pv; psatzl R. Qed. Lemma q2_1_2_aux : forall a b, 0 < a -> 0 < b -> Riemann_integrable (fun t => /sqrt(a^2 * (cos t)^2 + b^2 * (sin t)^2)) 0 (PI/2). intros a b a0 b0; apply continuity_implies_RiemannInt. assert (t := PI_RGT_0); psatzl R. intros t tint; apply continuity_pt_inv. apply (continuity_pt_comp _ sqrt);[ | apply continuity_pt_sqrt]. reg. apply Rplus_le_le_0_compat; apply Rmult_le_pos; apply pow2_ge_0. apply Rgt_not_eq, sqrt_lt_R0. destruct (Req_EM_T t 0) as [t0 | tn0]. apply Rlt_le_trans with (a ^ 2 * cos t ^ 2 + 0). rewrite Rplus_0_r; rewrite t0, cos_0; simpl (1 ^ 2); rewrite !Rmult_1_r. apply pow_lt; assumption. apply Rplus_le_compat_l; apply Rmult_le_pos; apply pow2_ge_0. apply Rlt_le_trans with (0 + b ^ 2 * sin t ^ 2). rewrite Rplus_0_l; apply Rmult_lt_0_compat. apply pow_lt; assumption. apply pow_lt; apply sin_gt_0; psatzl R. apply Rplus_le_compat_r. solve[rewrite <- Rpow_mult_distr; apply pow2_ge_0]. Qed. Definition gg x := match Rlt_dec 0 x with left h => RiemannInt (q2_1_2_aux 1 x Rlt_0_1 h) | right _ => 0 end. Lemma Rpower_mult_distr : (* standard *) forall x y z, 0 < x -> 0 < y -> Rpower x z * Rpower y z = Rpower (x * y) z. intros x y z x0 y0; unfold Rpower. rewrite <- exp_plus, ln_mult, Rmult_plus_distr_l; auto. Qed. Lemma q2_1_2 : forall a b (a0 : 0 < a) (b0 :0 < b), upInt ((q2_1_1 _ _ a0 b0) : _ (fun t => /sqrt ((t ^ 2 + a ^ 2) * (t ^ 2 + b ^ 2))) 0) = RiemannInt ((q2_1_2_aux _ _ a0 b0) : _ (fun x => /sqrt (a ^ 2 * cos x ^ 2 + b ^ 2 * sin x ^ 2)) 0 (PI / 2)). intros a b a0 b0; assert (pi2_0 : 0 < PI/2) by (set (t := PI_RGT_0); psatzl R). destruct (q2_1_1 a b a0 b0) as [h [l P]]; simpl. rewrite <- R_dist_refl. assert (R_dist l (RiemannInt (q2_1_2_aux a b a0 b0)) <= 0); [ | assert (t := R_dist_pos l (RiemannInt (q2_1_2_aux a b a0 b0))); apply Rle_antisym; [assumption | apply Rge_le; assumption]]. apply prop_eps; intros eps ep; assert (ep2 : 0 < eps/2) by psatzl R. destruct (P _ ep2) as [K Pk]; clear P. assert (exists delta :R, 0 < delta /\ forall x, PI/2 - delta < x < PI/2 -> exists h : Riemann_integrable (fun y => /sqrt (a ^ 2 * cos y ^ 2 + b ^ 2 * sin y ^ 2)) 0 x, R_dist (RiemannInt h) (RiemannInt (q2_1_2_aux a b a0 b0)) < eps/2) as [delta [delta0 Pdelta]]. assert (f2_ct : forall x, 0 <= x <= PI/2 -> continuity_pt (fun y => /sqrt (a ^ 2 * cos y ^ 2 + b ^ 2 * sin y ^ 2)) x). intros x [x0 xpi2]; reg. apply Rplus_le_le_0_compat; apply Rmult_le_pos; apply pow2_ge_0. apply Rgt_not_eq, sqrt_lt_R0. destruct x0 as [xgt0 | xq0]. apply Rplus_le_lt_0_compat. apply Rmult_le_pos; apply pow2_ge_0. assert (t : x < PI) by psatzl R; set (t' := sin_gt_0 _ xgt0 t); apply Rmult_lt_0_compat; apply pow_lt; assumption. rewrite <- xq0, sin_0, pow_ne_zero, Rmult_0_r, Rplus_0_r, cos_0;[|omega]. rewrite pow1, Rmult_1_r; apply pow_lt; assumption. assert (pr_ct : forall x, 0 <= x <= PI/2 -> continuity_pt (primitive (Rlt_le _ _ pi2_0) (FTC_P1 (Rlt_le _ _ pi2_0) f2_ct)) x). intros x intx; apply derivable_continuous_pt. exists ((fun y => /sqrt (a ^ 2 * cos y ^ 2 + b ^ 2 * sin y ^ 2)) x). unfold derivable_pt_abs. apply (@RiemannInt_P28 (fun y => /sqrt (a ^ 2 * cos y ^ 2 + b ^ 2 * sin y ^ 2))). assumption. destruct (pr_ct (PI/2) (conj (Rlt_le _ _ pi2_0) (Rle_refl (PI/2))) _ ep2) as [delta [delta0 Pdelta]]; unfold R_met, dist, Base in Pdelta. assert (ftc_a1 := Rlt_le _ _ pi2_0). set (delta' := Rmin delta (PI/4)). assert (delta' <= delta) by apply Rmin_l. assert (delta'0 : 0 < delta') by (apply Rmin_pos; psatzl R). assert (delta'_pi2 : delta' < PI/2). apply Rle_lt_trans with (1 := Rmin_r delta _); psatzl R. assert (pi2md0 : 0 < PI/2 - delta') by psatzl R. exists delta';split;[assumption | intros x [pimdelta xpi2]]. assert (pi2mdeltapi2 : PI/2 -delta' <= PI/2) by psatzl R. assert (f2_ct_x : forall z, 0 <= z <= x -> continuity_pt (fun y => /sqrt (a ^ 2 * cos y ^ 2 + b ^ 2 * sin y ^ 2)) z). intros; apply f2_ct; psatzl R. assert (x0 : 0 <= x) by psatzl R. exists (FTC_P1 ftc_a1 f2_ct x0 (Rlt_le _ _ xpi2)). assert (Pdelta_cond : D_x no_cond (PI / 2) x /\ R_dist x (PI / 2) < delta). unfold D_x, no_cond. split;[split;[exact I | apply Rgt_not_eq; assumption] | ]. unfold R_dist; rewrite Rabs_left; psatzl R. generalize (Pdelta _ Pdelta_cond); unfold primitive. destruct (Rle_dec 0 x) as [x0' | abs];[ |psatzl R; tauto]. (* TO REPORT: BUG *) destruct (Rle_dec x (PI/2)) as [xpi2' | abs];[ | psatzl R; psatzl R]. destruct (Rle_dec 0 (PI / 2)) as [pi2_0' | abs];[ | psatzl R; psatzl R]. destruct (Rle_dec (PI / 2) (PI / 2)) as [pi2' | abs];[ | psatzl R; psatzl R]. rewrite (RiemannInt_P5 (FTC_P1 (Rlt_le _ _ pi2_0) f2_ct pi2_0' pi2') (q2_1_2_aux a b a0 b0)); clear pi2_0' pi2'; simpl. match goal with |- R_dist ?a _ < _ -> R_dist ?b _ < _ => replace a with b by apply RiemannInt_P5; tauto end. set (u := Rmax (PI/2 - delta/2) (atan (Rmax 1 (K/b + 1)))). assert (u0 : 0 < u). apply Rlt_le_trans with (2 := Rmax_r (PI / 2 - delta/2) _). rewrite <- atan_0; apply atan_increasing. apply Rlt_le_trans with (2 := Rmax_l _ _);psatzl R. assert (u0' : 0 < tan u). rewrite <- tan_0; apply tan_increasing. psatzl R. assumption. apply Rmax_lub_lt;[psatzl R | ]. destruct (atan_bound (Rmax 1 (K/b + 1))); unfold u; psatzl R. assert (-PI/2 < u < PI/2) as [u_mpi2 u_pi2]. destruct (atan_bound (Rmax 1 (K/b + 1))). split. apply Rlt_le_trans with (2 := Rmax_r _ _); psatzl R. apply Rmax_lub_lt;psatzl R. assert (uK : K < b * tan u). replace K with (b * (K/b)) by (field; apply Rgt_not_eq; assumption). apply Rmult_lt_compat_l;[assumption | ]. destruct (Rmax_r (PI/2 - delta/2)(atan (Rmax 1 (K/b + 1)))) as [strict | q]. apply Rlt_trans with (tan (atan (Rmax 1 (K/b + 1)))). rewrite atan_right_inv. apply Rlt_le_trans with (2 := Rmax_r _ _); psatzl R. apply tan_increasing; try assumption. destruct (atan_bound (Rmax 1 (K/b + 1))); psatzl R. unfold u; rewrite <- q; unfold u; rewrite atan_right_inv. apply Rlt_le_trans with (2 := Rmax_r _ _); psatzl R. assert (ricomp : Riemann_integrable (fun x => b * (1 + tan x ^ 2) * /sqrt (((b * tan x)^2 + a ^ 2) * ((b * tan x) ^ 2 + b ^ 2))) 0 u). apply continuity_implies_RiemannInt;[psatzl R | ]. intros x [x0 xu]. assert (tanx0 : 0 <= tan x). destruct x0 as [xgt0 | xq0]. rewrite <- tan_0; apply Rlt_le, tan_increasing. psatzl R. assumption. apply Rle_lt_trans with (2:=u_pi2); assumption. rewrite <- xq0, tan_0; apply Rle_refl. reg. apply Rmult_le_pos; apply Rplus_le_le_0_compat; apply pow2_ge_0. apply derivable_continuous_pt, derivable_pt_tan; psatzl R. apply Rgt_not_eq. apply sqrt_lt_R0; apply Rmult_lt_0_compat; apply Rplus_le_lt_0_compat; (try apply pow2_ge_0); apply pow_lt; assumption. assert (f_ct : forall x : R, b * tan 0 <= x <= b * tan u -> continuity_pt (fun t : R => / sqrt ((t ^ 2 + a ^ 2) * (t ^ 2 + b ^ 2))) x). intros x intx; reg. apply Rmult_le_pos; apply Rplus_le_le_0_compat; apply pow2_ge_0. apply Rgt_not_eq, sqrt_lt_R0, Rmult_lt_0_compat; apply Rplus_le_lt_0_compat; try (apply pow2_ge_0); apply pow_lt; assumption. assert (f_ri :Riemann_integrable (fun t : R => / sqrt ((t ^ 2 + a ^ 2) * (t ^ 2 + b ^ 2))) (b * tan 0) (b * tan u)). apply continuity_implies_RiemannInt. apply Rmult_le_compat; try rewrite tan_0; try psatzl R. assumption. assert (f_der : forall x, 0 <= x <= u -> derivable_pt_lim (fun x0 : R => b * tan x0) x (b * (1 + tan x ^ 2))). intros x intx. assert (intx' : -PI/2 < x < PI/2) by psatzl R. apply derivable_pt_lim_scal. rewrite <- (derive_pt_eq _ _ _ (derivable_pt_tan x intx')). apply derive_pt_tan. assert (intg : forall x : R, 0 <= x <= u -> b * tan 0 <= b * tan x <= b * tan u). intros x [x0 xu]. assert (0 <= tan x). destruct x0 as [xgt0 | xq0]. apply Rlt_le, tan_gt_0; psatzl R. rewrite <- xq0, tan_0; apply Rle_refl. split. rewrite tan_0, Rmult_0_r; apply Rmult_le_pos; [apply Rlt_le |];assumption. apply Rmult_le_compat; try psatzl R. destruct xu as [xltu | xqu]. apply Rlt_le, tan_increasing; try psatzl R. rewrite xqu; apply Rle_refl. assert (d_ct : forall x : R, 0 <= x <= u -> continuity_pt (fun x0 : R => b * (1 + tan x0 ^ 2)) x). intros; reg; apply derivable_continuous_pt, derivable_pt_tan; psatzl R. assert (vc := RiemannInt_variable_change (fun t => /(sqrt ((t ^ 2 + a ^ 2) * (t ^ 2 + b ^ 2)))) (fun x => b * tan x) (fun x => b * (1 + tan x ^ 2)) 0 u (Rlt_le _ _ u0) ricomp f_ri f_der intg f_ct d_ct). assert (intdelta2 : PI/2 - delta < u Rpower x (-/2)). assert (0 < 1 + tan x ^ 2) by (set (t := pow2_ge_0 (tan x));psatzl R). assert (0 < b * (1 + tan x ^ 2)) by (apply Rmult_lt_0_compat; assumption). rewrite Rpower_Ropp. replace (Rpower (b * (1 + tan x ^ 2)) 2) with ((b * (1 + tan x ^ 2)) ^ 2) by (replace 2 with (INR 2) by auto; apply sym_equal, Rpower_pow; assumption). assert (cxn0 : cos x <> 0) by (apply Rgt_not_eq, cos_gt_0; psatzl R). assert (trigo1 : 1 + tan x ^ 2 = 1/cos x ^ 2). unfold tan; pattern 1 at 2; rewrite <- (sin2_cos2 x); unfold Rsqr. field; assumption. rewrite trigo1; unfold tan. replace (/ (b * (1 / cos x ^ 2)) ^ 2) with ((cos x ^2) ^ 2/b^2) by (field;psatzl R). field_simplify;[ | split;[ | apply Rgt_not_eq]; assumption]. replace (sin x ^ 4) with ((sin x ^ 2) ^ 2) by ring. replace (sin x ^ 2) with (1 - cos x ^ 2). field; apply Rgt_not_eq; psatzl R. rewrite <- (sin2_cos2 x); unfold Rsqr; ring. Qed. Definition I_t (a b : R) := match Rlt_dec 0 a with left a0 => match Rlt_dec 0 b with left b0 => upInt (q2_1_1 _ _ a0 b0) | right _ => 0 (* To do: choose a continuation that makes I_t C1_fun, if possible *) end | right _ => 0 end. Definition I2_t (a b : R) := match Rlt_dec 0 a with left a0 => match Rlt_dec 0 b with left b0 => RiemannInt (q2_1_2_aux _ _ a0 b0) | right _ => 0 end | right _ => 0 end. Lemma q2_1_2_t : forall a b, I_t a b = I2_t a b. intros a b; unfold I_t, I2_t; destruct (Rlt_dec 0 a); destruct (Rlt_dec 0 b); apply q2_1_2 || reflexivity. Qed. Lemma ag_derivable_pt : forall n a b, 0 < a -> 0 < b -> derivable_pt (fun x => (fst (ag x b n))) a * derivable_pt (fun x => (snd (ag x b n))) a * derivable_pt (fun x => (fst (ag a x n))) b * derivable_pt (fun x => (snd (ag a x n))) b. induction n. simpl; intros a b a0 b0; repeat apply pair; reg. simpl; intros a b a0 b0; destruct (IHn _ _ a0 b0) as [[[[l1 IHn1] [l2 IHn2]] [l3 IHn3]] [l4 IHn4]]. split;[split;[split |]|]. assert (derivable_pt (fun x => (fst (ag x b n) + snd (ag x b n))/2) a) as [la Pla]. exists ((l1 + l2)/2). unfold derivable_pt_abs. apply derivable_pt_lim_div_scal; apply derivable_pt_lim_plus; assumption. exists la. apply derivable_pt_lim_eq with (a := 0) (b := a + 1) (3 := Pla). psatzl R. intros z _; destruct (ag z b n); reflexivity. assert (derivable_pt (fun x => sqrt (fst (ag x b n) * snd (ag x b n))) a) as [lb Plb]. exists (/ (2 * sqrt (fst (ag a b n) * snd (ag a b n))) * (l1 * snd (ag a b n) + fst (ag a b n) * l2)). apply (derivable_pt_lim_comp (fun y => fst (ag y b n) * snd (ag y b n)) sqrt). apply derivable_pt_lim_mult; assumption. apply derivable_pt_lim_sqrt. destruct (ag_positive n a b);try assumption. apply Rmult_lt_0_compat; assumption. exists lb. apply derivable_pt_lim_eq with (f := fun x => (sqrt (fst (ag x b n) * snd (ag x b n)))) (a := 0) (b := a + 1) (3 := Plb). psatzl R. intros z _; destruct (ag z b n); reflexivity. assert (derivable_pt (fun x => (fst (ag a x n) + snd (ag a x n))/2) b) as [la Pla]. exists ((l3 + l4)/2). unfold derivable_pt_abs. apply derivable_pt_lim_div_scal; apply derivable_pt_lim_plus; assumption. exists la. apply derivable_pt_lim_eq with (a := 0) (b := b + 1) (3 := Pla). psatzl R. intros z _; destruct (ag a z n); reflexivity. assert (derivable_pt (fun x => sqrt (fst (ag a x n) * snd (ag a x n))) b) as [lb Plb]. exists (/ (2 * sqrt (fst (ag a b n) * snd (ag a b n))) * (l3 * snd (ag a b n) + fst (ag a b n) * l4)). apply (derivable_pt_lim_comp (fun y => fst (ag a y n) * snd (ag a y n)) sqrt). apply derivable_pt_lim_mult; assumption. apply derivable_pt_lim_sqrt. destruct (ag_positive n a b);try assumption. apply Rmult_lt_0_compat; assumption. exists lb. apply derivable_pt_lim_eq with (a := 0) (b := b + 1) (3 := Plb). psatzl R. intros z _; destruct (ag a z n); reflexivity. Qed. Lemma q2_1_3_scal : forall a b (a0 : 0 < a) (b0 :0 < b) (ba0 : 0 < b/a), upInt (q2_1_1 _ _ a0 b0) = 1 / a * upInt (q2_1_1 _ _ Rlt_0_1 ba0). set (PI_RGT_0:=PI_RGT_0). intros a b a0 b0 ba0. assert (H : forall x, Rmin 0 (PI/2) <= x <= Rmax 0 (PI/2) -> (fun x => /sqrt (a ^ 2 * cos x ^ 2 + b ^ 2 * sin x ^ 2)) x = (fun x => 0 + /a * /sqrt (1 ^ 2 * cos x ^ 2 + (b / a) ^ 2 * sin x ^ 2)) x). intros x intx; rewrite Rplus_0_l, pow1, Rmult_1_l. assert (0 < cos x ^ 2 + (b / a) ^ 2 * sin x ^ 2). destruct (Req_EM_T x 0) as [x0 | xn0]. rewrite x0, sin_0, pow_ne_zero, Rmult_0_r, Rplus_0_r, cos_0, pow1; [psatzl R | omega]. rewrite Rmin_left, Rmax_right in intx; try (psatzl R). rewrite <- Rpow_mult_distr. apply Rplus_le_lt_0_compat;[apply pow2_ge_0 | apply pow_lt]. apply Rmult_lt_0_compat;[ | apply sin_gt_0; psatzl R]. assumption. rewrite <- Rinv_mult_distr;[ | apply Rgt_not_eq | apply Rgt_not_eq, sqrt_lt_R0]; try assumption. pattern a at 2; rewrite <- sqrt_Rsqr;[ | psatzl R]. replace (Rsqr a) with (a ^ 2) by (unfold Rsqr; ring). rewrite <- sqrt_mult;[ | apply Rlt_le, pow_lt | apply Rlt_le];try assumption. unfold Rdiv; rewrite Rmult_plus_distr_l, Rpow_mult_distr, <- Rinv_pow; [ | apply Rgt_not_eq; assumption]. rewrite (Rmult_comm (b ^ 2) (/ a ^ 2)), <- !Rmult_assoc, Rinv_r, Rmult_1_l; [reflexivity | apply Rgt_not_eq, pow_lt; assumption]. assert (H' := H). apply Riemann_integrable_eq in H;[ | apply q2_1_2_aux; assumption]. rewrite !q2_1_2. rewrite (RiemannInt_P18 (q2_1_2_aux a b a0 b0) H); [ | psatzl R | intros; apply H'; rewrite Rmin_left, Rmax_right;psatzl R]. change (1/a) with (1 * / a); rewrite Rmult_1_l. match goal with |- _ = ?A => rewrite <- (Rplus_0_l A) end. pattern 0 at 3; replace 0 with (RiemannInt (RiemannInt_P14 0 (PI / 2) 0)) by (rewrite RiemannInt_P15; apply Rmult_0_l). apply RiemannInt_P13. Qed. Lemma q2_1_3_comm : forall a b (a0 : 0 < a) (b0 : 0 < b), upInt (q2_1_1 _ _ a0 b0) = upInt (q2_1_1 _ _ b0 a0). intros; apply upInt_ext; intros; rewrite Rmult_comm; reflexivity. Qed. Lemma q2_2_1_derive : forall t a, 0 < t -> derivable_pt_lim (fun x => (x - a / x)/ 2) t ((1 + a/(t ^ 2))/2). intros t a t0. apply derivable_pt_lim_eq with (f:= fun x => /2 * (x + (-a) * / x)) (a := t/2) (b := t + 1);[psatzl R | intros; field; apply Rgt_not_eq; psatzl R |]. replace ((1 + a / t ^ 2)/2) with (/2 * (1 + (-a) * ((-1)*Rpower t (-INR 2)))); [ | rewrite Rpower_Ropp, Rpower_pow; try (field; apply Rgt_not_eq); tauto ]. apply derivable_pt_lim_scal. apply derivable_pt_lim_plus. apply derivable_pt_lim_id. apply derivable_pt_lim_scal. apply derivable_pt_lim_eq with (f := fun x => Rpower x (-1)) (a := t/2) (b := t+1). psatzl R. intros z intz; rewrite Rpower_Ropp, Rpower_1;[reflexivity | psatzl R]. replace (-INR 2) with (-1 - 1) by (simpl; psatzl R). apply derivable_pt_lim_power; assumption. Qed. Lemma q2_2_1_eq : forall s t a b, 0 < t -> s ^ 2 = ((t - a * b /t) /2) ^ 2 -> 4 * (s ^ 2 + ((a + b) / 2) ^ 2) * (s ^ 2 + a * b) = (t ^ 2 + a ^ 2) * (t ^ 2 + b ^ 2)* ((1 + a * b / t ^ 2) / 2) ^ 2. intros s t a b t0 q; rewrite q; field; lt0. Qed. Lemma q2_2_1_a : forall a b, 0 < a -> 0 < b -> 0 < (a + b)/2. (* TODO : move earlier *) intros; lt0. Qed. Lemma q2_2_1_g : forall a b, 0 < a -> 0 < b -> 0 < sqrt (a * b). intros; lt0. Qed. Lemma der_pos : forall a b x, 0 < x -> 0 < a -> 0 < b -> 0 < (1 + a * b / x ^ 2) / 2. intros; lt0. Qed. Lemma q2_2_1_aux : forall a b, 0 < a -> 0 < b -> up_infinite_integrable (fun t => / sqrt ((t ^ 2 + a ^ 2) * (t ^ 2 + b ^ 2))) (sqrt (a * b)). intros a b a0 b0. apply up_infinite_integrable_break with 0. apply q2_1_1; auto. apply continuity_implies_RiemannInt;[lt0 | intros; reg; lt0 ]. Qed. Lemma q2_3_1_ri : forall b, 0 < b -> Riemann_integrable (fun t => /sqrt((t ^ 2 + 1 ^ 2) * (t ^ 2 + b ^ 2))) 0 (sqrt b). intros; apply continuity_implies_RiemannInt. apply Rlt_le, sqrt_lt_R0; assumption. intros; reg;[apply Rlt_le | apply Rgt_not_eq, sqrt_lt_R0]; apply q2_body_pos; psatzl R. Qed. Lemma q2_3_1_ui : forall b, 0 < b -> up_infinite_integrable (fun t => /sqrt((t ^ 2 + 1 ^ 2) * (t ^ 2 + b ^ 2))) (sqrt b). intros b b0. apply up_infinite_integrable_break with (2 := q2_3_1_ri b b0). apply q2_1_1; psatzl R. Qed. Lemma derivable_pt_lim_inv : (* TODO : Check this proof is not done inside a big one. *) forall x, x <> 0 -> derivable_pt_lim Rinv x (- / x ^ 2). assert (main : forall x, 0 < x -> derivable_pt_lim Rinv x (- / x ^ 2)). intros x x0. apply (derivable_pt_lim_eq (fun y => Rpower y (-1)) Rinv x (x / 2) (x + 1)). psatzl R. intros; rewrite Rpower_Ropp, Rpower_1; psatzl R. replace (-/ x ^ 2) with ((-1) * Rpower x (-1 - 1)). apply derivable_pt_lim_power; assumption. replace (-1 - 1) with (-INR 2) by (simpl; ring). rewrite Rpower_Ropp, Rpower_pow; [ring | assumption]. intros x xn0; destruct (Rle_dec x 0);[ | apply main; psatzl R]. apply (derivable_pt_lim_eq (fun y => (-1) * / ((-1) * y)) Rinv x (x - 1) (x / 2)). psatzl R. intros; field; psatzl R. replace (- / x ^ 2) with ((-1) * ((-/(-1 * x)^2) * (-1 * 1))) by (field;psatzl R). apply derivable_pt_lim_scal. apply (derivable_pt_lim_comp (fun y => (-1) * y)). apply derivable_pt_lim_scal. apply derivable_pt_lim_id. apply main; psatzl R. Qed. Lemma q2_3_1 : forall b (b0 : 0 < b), upInt ((q2_3_1_ui _ b0) : _ (fun t => /sqrt ((t ^ 2 + 1 ^ 2) * (t ^ 2 + b ^ 2))) (sqrt b)) = RiemannInt ((q2_3_1_ri _ b0) : _ (fun t => / sqrt ((t ^ 2 + 1 ^ 2) * (t ^ 2 + b ^ 2))) 0 (sqrt b)). intros b b0; assert (sqrtb0 := Rlt_le _ _ (sqrt_lt_R0 _ b0)). rewrite <- R_dist_refl; apply Rle_antisym;[ | apply Rge_le, R_dist_pos]. apply prop_eps; intros eps ep; assert (ep2 : 0 < eps/2) by psatzl R. destruct (q2_3_1_ui b b0) as [h [l P]]; simpl. destruct (P _ ep2) as [K Pk]; clear P. assert (exists delta, 0 < delta /\ forall x, 0 < x < delta -> forall h : Riemann_integrable (fun t => / sqrt ((t ^ 2 + 1 ^ 2) * (t ^ 2 + b ^ 2))) x (sqrt b), R_dist (RiemannInt h) (RiemannInt (q2_3_1_ri _ b0)) < eps/2) as [dlt [dlt0 Pdlt]]. set (e4 := Rmin (eps/4 * b) (Rmin (sqrt b) (eps/2))). assert (e4sqrtb : e4 <= sqrt b). solve[unfold e4; rewrite Rmin_comm, <- Rmin_assoc; apply Rmin_l]. assert (ep4 : 0 < e4). apply Rmin_pos; [apply Rmult_lt_0_compat;[psatzl R | ] | apply Rmin_pos;[ | psatzl R] ]; try apply sqrt_lt_R0; assumption. exists e4. split;[assumption | ]. intros x intx h'. assert (h2 : Riemann_integrable (fun t => / sqrt ((t ^ 2 + 1 ^ 2) * (t ^ 2 + b ^ 2))) 0 x). apply (RiemannInt_P22 (q2_3_1_ri b b0)); psatzl R. rewrite <- (RiemannInt_P26 h2 h' (q2_3_1_ri b b0)). unfold R_dist. assert (t : forall u v, u - (v + u) = -v) by (intros; ring); rewrite t, Rabs_Ropp; clear t. assert (bnd : forall t, 0 < t -> / sqrt ((t ^ 2 + 1 ^ 2) * (t ^ 2 + b ^ 2)) < / b). intros t t0; apply Rinv_lt_contravar. apply Rmult_lt_0_compat;[assumption | apply sqrt_lt_R0; apply Rmult_lt_0_compat; apply Rplus_lt_0_compat; apply pow_lt; assumption || psatzl R]. apply Rlt_trans with (sqrt ((t ^ 2 + 1 ^ 2) * b ^ 2)). pattern b at 1; rewrite <- sqrt_Rsqr; try psatzl R. replace (Rsqr b) with (1 * b ^ 2) by (unfold Rsqr; ring). apply sqrt_lt_1_alt. split;[rewrite Rmult_1_l; apply pow2_ge_0 | apply Rmult_lt_compat_r;[apply pow_lt;assumption | ]]. assert (tt := pow_lt _ 2 t0); rewrite pow1; psatzl R. apply sqrt_lt_1_alt. split. apply Rlt_le, Rmult_lt_0_compat; [apply Rplus_lt_0_compat | ]; apply pow_lt; psatzl R. apply Rmult_lt_compat_l;[apply Rplus_lt_0_compat; apply pow_lt; psatzl R |]. assert (tt := pow_lt _ 2 t0); psatzl R. assert (bnd0 : forall t, 0 < t -> 0 < / sqrt ((t ^ 2 + 1 ^ 2) * (t ^ 2 + b ^ 2))). intros t t0; apply Rinv_0_lt_compat, sqrt_lt_R0, q2_body_pos; psatzl R. assert (ripos : 0 <= RiemannInt h2). pattern 0 at 1; replace 0 with (RiemannInt (RiemannInt_P14 0 x 0)). apply RiemannInt_P19; try psatzl R. intros y inty; apply Rlt_le, bnd0; psatzl R. rewrite RiemannInt_P15; psatzl R. rewrite Rabs_pos_eq;[ | assumption]. apply Rle_lt_trans with (RiemannInt (RiemannInt_P14 0 x (/b))). apply RiemannInt_P19; try psatzl R. intros y inty; apply Rlt_le, bnd; psatzl R. rewrite RiemannInt_P15, Rminus_0_r. apply Rlt_trans with (/ b * e4). apply Rmult_lt_compat_l;[apply Rinv_0_lt_compat;assumption | psatzl R ]. unfold e4. apply Rle_lt_trans with (/ b * (eps / 4 * b)). apply Rmult_le_compat_l. apply Rlt_le, Rinv_0_lt_compat; assumption. apply Rmin_l. rewrite Rmult_comm, Rmult_assoc, Rinv_r;[psatzl R | apply Rgt_not_eq; assumption]. set (dlt' := Rmin (dlt/2) (Rmin (sqrt b / 2) (b / (Rmax K 0 + 1)))). assert (dlt'0 : 0 < dlt'). unfold dlt'; apply Rmin_pos;[psatzl R | ]. apply Rmin_pos;[assert (t := sqrt_lt_R0 _ b0); psatzl R | ]. apply Rmult_lt_0_compat;[psatzl R | ]. apply Rinv_0_lt_compat; apply Rlt_le_trans with (0 + 1);[psatzl R | ]. apply Rplus_le_compat_r, Rmax_r. assert (dlt'2 : dlt' < dlt). unfold dlt'. apply Rle_lt_trans with (1 := Rmin_l _ (Rmin (sqrt b / 2) (b / (Rmax K 0 + 1))));psatzl R. assert (mxk0 : 0 < Rmax K 0 + 1). assert (tt := Rmax_r K 0); psatzl R. assert (dlt'K : K < b / dlt'). unfold dlt'. apply Rlt_le_trans with (Rmax K 0 + 1). assert (tt := Rmax_l K 0); psatzl R. apply Rle_trans with (b / (b / (Rmax K 0 + 1))). replace (b / (b / (Rmax K 0 + 1))) with (Rmax K 0 + 1) by (field; psatzl R). psatzl R. apply Rmult_le_compat_l;[apply Rlt_le; assumption | ]. apply Rle_Rinv. apply Rmin_pos;[psatzl R | apply Rmin_pos;[ |apply Rmult_lt_0_compat; auto]]. assert (t := sqrt_lt_R0 _ b0); psatzl R. apply Rinv_0_lt_compat; assumption. apply Rmult_lt_0_compat;[| apply Rinv_0_lt_compat]; assumption. rewrite Rmin_assoc; apply Rmin_r. assert (dlt'sqrt2 : dlt' <= sqrt b / 2). unfold dlt'; rewrite (Rmin_comm (sqrt b / 2)), Rmin_assoc. apply Rle_trans with (sqrt b / 2);[apply Rmin_r | psatzl R]. assert (dlt'sqrt : dlt' <= sqrt b) by psatzl R. assert (ridlt' : Riemann_integrable (fun t => / sqrt ((t ^ 2 + 1 ^ 2) * (t ^ 2 + b ^ 2))) dlt' (sqrt b)). apply (RiemannInt_P23 (q2_3_1_ri b b0)); psatzl R. apply Rle_lt_trans with (1 := R_dist_tri _ _ (RiemannInt ridlt')). replace eps with (eps/2 + eps/2) by psatzl R. apply Rplus_lt_compat;[ | apply Pdlt; psatzl R]. clear Pdlt dlt'2. assert (sqrtblt : sqrt b < b / dlt'). pattern b at 2; rewrite <- Rsqr_sqrt; unfold Rsqr; [ | apply Rlt_le; assumption]. apply Rmult_lt_reg_r with dlt';[assumption | ]. unfold Rdiv; rewrite !Rmult_assoc, Rinv_l, Rmult_1_r;[ | psatzl R]. apply Rmult_lt_compat_l;[apply sqrt_lt_R0| ]; try assumption. psatzl R. assert (ribdivdlt' : Riemann_integrable (fun x => /sqrt ((x ^ 2 + 1 ^ 2) * (x ^ 2 + b ^ 2))) (sqrt b) (b/dlt')). destruct (q2_3_1_ui _ b0) as [tmp _]; apply tmp; assumption. assert (bsqrtb : b / sqrt b = sqrt b). pattern b at 1; rewrite <- Rsqr_sqrt; unfold Rsqr;[field| ]; psatzl R. rewrite <- bsqrtb in ribdivdlt'. set (ri2 := Riemann_integrable_Ropp (RiemannInt_P1 ribdivdlt')). assert (t := RiemannInt_variable_change1' (fun x => -/sqrt ((x ^ 2 + 1 ^ 2) * (x ^ 2 + b ^ 2))) (fun x => /sqrt ((x ^ 2 + 1 ^ 2) * (x ^ 2 + b ^ 2))) (fun x => b / x) (fun x => - b / x ^ 2) dlt' (sqrt b) dlt'sqrt ridlt' ri2); lazy beta in t. assert (bdivdlt'le : b / sqrt b <= b / dlt'). apply Rmult_le_compat_l;[apply Rlt_le; assumption | ]. apply Rle_Rinv;[ |apply sqrt_lt_R0 | ]; assumption. rewrite (Rmin_right _ _ bdivdlt'le), (Rmax_left _ _ bdivdlt'le) in t. assert (final : RiemannInt ridlt' = RiemannInt ri2). apply t; clear t. intros; replace (- b / x ^ 2) with (b * (- / x ^ 2));[|field; psatzl R]. apply derivable_pt_lim_scal, derivable_pt_lim_inv; psatzl R. intros x intx; split; (apply Rmult_le_compat_l;[psatzl R | apply Rle_Rinv; try psatzl R ]). intros; reg;[apply Rlt_le | apply Rgt_not_eq, sqrt_lt_R0 ]; apply q2_body_pos; psatzl R. intros; reg; apply Rgt_not_eq, pow_lt; psatzl R. intros x intx. unfold Rdiv; rewrite Ropp_mult_distr_l_reverse, Rmult_opp_opp, Rmult_assoc. rewrite <- Rinv_mult_distr. pattern (x ^ 2) at 3; rewrite <- sqrt_Rsqr; unfold Rsqr. assert (t : b = / (sqrt (/ (b ^ 2)))). replace (b ^ 2) with (Rsqr b) by (unfold Rsqr; ring). rewrite <- Rsqr_inv, sqrt_Rsqr; [field |apply Rlt_le, Rinv_0_lt_compat | ]; psatzl R. pattern b at 2; rewrite t; clear t. rewrite <- Rinv_mult_distr, <- !sqrt_mult_alt. apply f_equal; apply f_equal. field; psatzl R. apply Rlt_le, Rinv_0_lt_compat, pow_lt; assumption. solve[apply Rmult_le_pos; apply pow2_ge_0]. apply Rgt_not_eq, sqrt_lt_R0, Rinv_0_lt_compat, pow_lt; assumption. apply Rgt_not_eq, Rmult_lt_0_compat; apply sqrt_lt_R0. apply Rmult_lt_0_compat; apply pow_lt; psatzl R. apply q2_body_pos; psatzl R. apply pow2_ge_0. apply Rgt_not_eq, pow_lt; psatzl R. apply Rgt_not_eq, sqrt_lt_R0, q2_body_pos; psatzl R. rewrite final, R_dist_sym; clear t final. unfold ri2; rewrite <- RiemannInt_Ropp; generalize (RiemannInt_P1 ribdivdlt'). rewrite bsqrtb; clear ri2; intros ri3. rewrite <- (RiemannInt_P8 (RiemannInt_P1 ri3)). rewrite (RiemannInt_P5 _ (h _ sqrtblt)); apply Pk; assumption. Qed. Lemma mf_integrable : forall a b c d, 0 < a -> 0 < b -> Riemann_integrable (fun x => /sqrt ((x ^ 2 + a ^ 2) * (x ^ 2 + b ^ 2))) c d. intros; destruct (Rle_dec c d);[ | apply RiemannInt_P1]; (apply continuity_implies_RiemannInt; try psatzl R; intros; (reg;[apply Rlt_le | apply Rgt_not_eq, sqrt_lt_R0]); apply q2_body_pos; assumption). Qed. Lemma q2_2_1 : forall a b (a0 : 0 < a) (b0 : 0 < b), I_t a b = I_t ((a + b) / 2) (sqrt (a * b)). intros a b a0 b0. assert (upInt ((q2_1_1 _ _ a0 b0) : up_infinite_integrable (fun t => / sqrt ((t ^ 2 + a ^ 2) * (t ^ 2 + b ^ 2))) 0) = upInt ((q2_1_1 _ _ (q2_2_1_a _ _ a0 b0) (q2_2_1_g _ _ a0 b0)) : _ (fun t => / sqrt ((t ^ 2 + ((a + b) / 2) ^2) * (t ^ 2 + (sqrt (a * b))^ 2))) 0)); [ | unfold I_t; destruct (Rlt_dec 0 a) as [da0 | a_0];[ | case a_0; psatzl R]; destruct (Rlt_dec 0 b) as [db0 | b_0];[| case b_0; psatzl R]; destruct (Rlt_dec 0 ((a + b)/2)) as [da'0 |a'_0]; [ |case a'_0; assert (tmp := q2_2_1_a a b a0 b0); psatzl R]; destruct (Rlt_dec 0 (sqrt (a * b))) as [db'0 | b'_0]; [ | case b'_0; assert (tmp := q2_2_1_g a b a0 b0); psatzl R]; rewrite (upInt_eq _ _ _ (q2_1_1 a b a0 b0)), H; solve[apply upInt_eq]]. assert (ab0 : 0 < a * b) by (apply Rmult_lt_0_compat; assumption). assert (sab0 : 0 < sqrt (a * b)) by (apply sqrt_lt_R0; assumption). assert (Vsab0 : 0 < / sqrt (a * b)) by (apply Rinv_0_lt_compat; assumption). rewrite <- R_dist_refl; apply Rle_antisym;[ | apply Rge_le, R_dist_pos]. apply prop_eps; intros eps ep. assert (0 < eps / 2 /\ 0 < eps / 4) as [ep2 ep4] by psatzl R. assert (r_ab : Riemann_integrable (fun t : R => / sqrt ((t ^ 2 + a ^ 2) * (t ^ 2 + b ^ 2))) 0 (sqrt (a * b))). apply mf_integrable; assumption. assert (u_ab : up_infinite_integrable (fun t : R => / sqrt ((t ^ 2 + a ^ 2) * (t ^ 2 + b ^ 2))) (sqrt (a * b))). apply up_infinite_integrable_break with 0;[ | assumption]. solve[apply (q2_1_1 a b a0 b0)]. rewrite <- (upInt_break _ (sqrt (a * b)) 0 u_ab r_ab). destruct u_ab as [h [l P]];simpl; destruct (P _ ep4) as [K Pk]; clear P. assert (exists K3, 0 < K3 /\ forall x, 0 < x < /K3 -> forall h:Riemann_integrable (fun t : R => / sqrt ((t ^ 2 + a ^ 2) * (t ^ 2 + b ^ 2))) 0 x, 0 <= RiemannInt h < eps/4) as [K3 [K3_0 Pk3]]. exists (4 / eps * / (a * b)). split. unfold Rdiv; repeat (apply Rmult_lt_0_compat || apply Rinv_0_lt_compat); psatzl R. intros x intx. assert (forall y, 0 < y < x -> 0 <= / sqrt ((y ^ 2 + a ^ 2) * (y ^ 2 + b ^ 2)) <= / (a * b)). intros y _. split;[apply Rlt_le, Rinv_0_lt_compat, sqrt_lt_R0, q2_body_pos; assumption|]. apply Rle_Rinv;[apply Rmult_lt_0_compat; assumption | apply sqrt_lt_R0, q2_body_pos; assumption | ]. rewrite <- (sqrt_square (a * b));[|apply Rlt_le; assumption]. apply sqrt_le_1_alt; replace (a * b * (a * b)) with ((a * b) ^ 2) by ring. solve[apply q2_body_bound]. intros h'; assert (0 * (x - 0) <= RiemannInt h' <= / (a * b) * (x - 0)) as [t1 t2]. apply RiemannInt_const_bound; try psatzl R; assumption. split;[psatzl R |apply Rle_lt_trans with (1 := t2)]. apply (Rmult_lt_reg_l (a * b));[assumption | ]. rewrite <- Rmult_assoc, Rinv_r, Rmult_1_l, Rminus_0_r;[ | lt0]. replace (a * b * (eps / 4)) with (/(4/eps * /(a * b))) by (field; psatzl R). tauto. destruct (q2_1_1 _ _ (q2_2_1_a _ _ a0 b0) (q2_2_1_g _ _ a0 b0)) as [h2 [l2 P2]]; simpl. destruct (P2 _ ep2) as [K2 Pk2]; clear P2. set (u := Rmax (sqrt (a * b)) (Rmax K (Rmax (a * b) (Rmax 1 (Rmax (/ sqrt (a * b)) (Rmax (/(a * b)) (Rmax ((2 * K2 + 1)/ (a * b)) (Rmax (2 * K3 + 2) (2 * K2 + 2)))))))) + 1). assert (u1 : 1 < u) by (unfold u; Rmax_isol 1). assert (Ku : K < u) by (unfold u; Rmax_isol K). assert (K2u : 2 * K2 + 2 < u) by (unfold u; Rmax_isol (2 * K2 + 2)). assert (uab2 : a * b < u) by (unfold u; Rmax_isol (a * b)). assert (uab : sqrt (a * b) < u) by (unfold u; Rmax_isol (sqrt (a * b))). assert (u0 : 0 < u) by (apply Rlt_trans with (sqrt (a * b));assumption). assert (Vu0 : 0 < / u) by (apply Rinv_0_lt_compat; assumption). assert (K3u : 2 * K3 + 2 < u) by (unfold u; Rmax_isol (2 * K3 + 2)). assert (uVsab : /sqrt (a * b) < u) by (unfold u; Rmax_isol (/sqrt (a * b))). assert (uVab : /(a * b) < u) by (unfold u; Rmax_isol (/(a * b))). assert (K2u' : (2 * K2 + 1)/(a * b) < u) by (unfold u; Rmax_isol ((2 * K2 + 1)/(a * b))). assert (Vusab : /u < sqrt (a * b)). rewrite <- (Rinv_involutive (sqrt (a * b)));[ | apply Rgt_not_eq; assumption]. apply Rinv_lt_contravar;[apply Rmult_lt_0_compat; [apply Rinv_0_lt_compat|] |]; assumption. assert (intVu : 0 <= (/u) <= sqrt (a * b)) by (split; apply Rlt_le; assumption). assert (rVu : Riemann_integrable (fun t => /sqrt ((t ^ 2 + a ^ 2) * ( t ^ 2 + b ^ 2))) 0 (/u)). apply (RiemannInt_P22 r_ab intVu). assert (rVusab : Riemann_integrable (fun t => /sqrt ((t ^ 2 + a ^ 2) * ( t ^ 2 + b ^ 2))) (/u) (sqrt (a * b))). apply (RiemannInt_P23 r_ab intVu). replace eps with (eps/4 + /2 * (eps/2) + /2 * (eps/2) + eps/4) by psatzl R; rewrite R_dist_sym. apply Rle_lt_trans with (1 := R_dist_tri _ _ ((RiemannInt r_ab) + (RiemannInt (h u uab)))). apply Rplus_lt_compat;[ clear Pk l | apply Rle_lt_trans with (1 := R_dist_plus _ _ _ _); rewrite R_dist_eq, Rplus_0_l; apply Pk; assumption]. rewrite <- (RiemannInt_P26 rVu rVusab), <- (Rplus_0_l l2), !Rplus_assoc. apply Rle_lt_trans with (1 := R_dist_plus _ _ _ _). apply Rplus_lt_compat. assert (VuK3 : /u < / K3). apply Rinv_lt_contravar;[apply Rmult_lt_0_compat; assumption | psatzl R]. assert (t := Pk3 _ (conj Vu0 VuK3) rVu). unfold R_dist; rewrite Rabs_left1; destruct t; psatzl R. assert (incr : forall v v', 0 < v <= v' -> (v - a * b / v) / 2 <= (v' - a * b / v') / 2). intros v v' [v0 [vltv' | vqv']]. assert (tdr : forall c, v <= c <= v' -> derivable_pt_lim (fun x => (x - a * b / x) / 2) c ((1 + a * b/ c ^ 2) / 2)). intros; apply q2_2_1_derive; psatzl R. destruct (MVT_cor2 (fun x => (x - a * b/x)/2) (fun x => (1 + a * b / x ^ 2)/2) _ _ vltv' tdr) as [c [w ci]]. assert (t : forall v v', 0 <= v - v' -> v' <= v) by (intros; psatzl R). apply t; clear t; rewrite w; apply Rmult_le_pos; try psatzl R. apply Rlt_le, der_pos; psatzl R. rewrite vqv'; apply Rle_refl. assert (dr : forall x, (sqrt (a * b)) <= x <= u -> derivable_pt_lim (fun x => (x - a * b / x) / 2) x ((1 + a * b / x ^ 2) / 2)). intros; apply q2_2_1_derive; psatzl R. assert (incr' : forall x, sqrt (a * b) <= x <= u -> (sqrt(a * b) - a * b/sqrt (a * b)) / 2 <= (x - a * b/x) / 2 <= (u - a * b / u) / 2). intros; split; apply incr; psatzl R. assert (ct : forall x : R, (sqrt (a * b) - a * b / sqrt (a * b)) / 2 <= x <= (u - a * b / u) / 2 -> continuity_pt (fun s : R => / (2 * sqrt ((s ^ 2 + ((a + b) / 2) ^ 2) * (s ^ 2 + sqrt (a * b) ^ 2)))) x). intros x _; reg. apply Rlt_le, q2_body_pos; auto; psatzl R. apply Rgt_not_eq, Rmult_lt_0_compat;[psatzl R | ]. apply sqrt_lt_R0, q2_body_pos;auto; psatzl R. assert (ri2 : Riemann_integrable (fun s : R => / (2 * sqrt ((s ^ 2 + ((a + b) / 2) ^ 2) * (s ^ 2 + sqrt (a * b) ^ 2)))) ((sqrt (a * b) - a * b / sqrt (a * b)) / 2) ((u - a * b / u) / 2)). apply continuity_implies_RiemannInt;[apply incr; psatzl R | assumption]. assert (ctd : forall x : R, sqrt (a * b) <= x <= u -> continuity_pt (fun t : R => (1 + a * b / t ^ 2) / 2) x). intros; reg; apply Rgt_not_eq, pow_lt; psatzl R. assert (eq : forall x : R, sqrt (a * b) <= x <= u -> / sqrt ((x ^ 2 + a ^ 2) * (x ^ 2 + b ^ 2)) = (1 + a * b / x ^ 2) / 2 * / (2 * sqrt ((((x - a * b / x) / 2) ^ 2 + ((a + b) / 2) ^ 2) * (((x - a * b / x) / 2) ^ 2 + sqrt (a * b) ^ 2)))). pattern 2 at 2; replace 2 with (sqrt 4) by (replace 4 with (2 * 2) by ring; rewrite sqrt_square; psatzl R). intros x intx; set (s := (x - a * b / x)/2). rewrite <- sqrt_mult_alt, <- Rmult_assoc ;[ | psatzl R ]. replace (sqrt (a * b) ^ 2) with (Rsqr (sqrt (a * b))) by (unfold Rsqr; ring). rewrite Rsqr_sqrt;[ | apply Rlt_le, Rmult_lt_0_compat; assumption]. rewrite (q2_2_1_eq s x);[ | psatzl R | reflexivity]. rewrite (sqrt_mult_alt _ (((1 + a * b / x ^ 2) / 2) ^ 2)); [ | apply Rlt_le, q2_body_pos; assumption]. assert (t : forall x, 0 <= x -> sqrt (x ^ 2) = x) by (intros; simpl; rewrite Rmult_1_r, sqrt_square; psatzl R). rewrite t; clear t. rewrite Rinv_mult_distr, (Rmult_comm (/ _)). rewrite <- Rmult_assoc, Rinv_r, Rmult_1_l;[reflexivity | ]. apply Rgt_not_eq, der_pos; psatzl R. apply Rgt_not_eq, sqrt_lt_R0, q2_body_pos; assumption. apply Rgt_not_eq, der_pos; psatzl R. apply Rlt_le, der_pos; psatzl R. generalize ri2 (RiemannInt_variable_change' (fun s => / (2 * sqrt ((s ^ 2 + ((a + b) / 2) ^ 2) * (s ^ 2 + sqrt (a * b) ^ 2)))) _ (fun t => (t - a * b / t) / 2) (fun t => (1 + a * b/ t ^ 2) / 2) (sqrt (a * b)) u (Rlt_le _ _ uab) (h u uab) ri2 dr incr' ct ctd eq). clear ctd eq ct incr'. assert (dr_2 : forall x, (/u) <= x <= (sqrt (a * b)) -> derivable_pt_lim (fun x => (-1) * ((x - a * b / x) / 2)) x ((-1) * ((1 + a * b / x ^ 2) / 2))). intros; apply derivable_pt_lim_scal; apply q2_2_1_derive; psatzl R. assert (incr'_2 : forall x, (/u) <= x <= sqrt (a * b) -> (-1) * ((sqrt(a * b) - a * b/sqrt (a * b)) / 2) <= (-1) * ((x - a * b/x) / 2) <= (-1) * (((/u - a * b / /u)) / 2)). intros; split; (apply Rmult_le_compat_neg_l;[psatzl R | ]); apply incr; psatzl R. assert (ct_2 : forall x : R, (-1) * ((sqrt (a * b) - a * b / sqrt (a * b)) / 2) <= x <= (-1) * ((/u - a * b / /u) / 2) -> continuity_pt (fun s : R => -/ (2 * sqrt ((s ^ 2 + ((a + b) / 2) ^ 2) * (s ^ 2 + sqrt (a * b) ^ 2)))) x). intros x _; reg. apply Rlt_le, q2_body_pos; auto; psatzl R. apply Rgt_not_eq, Rmult_lt_0_compat;[psatzl R | ]. apply sqrt_lt_R0, q2_body_pos; auto; psatzl R. assert (ri2_pre : Riemann_integrable (fun s : R => -/ (2 * sqrt ((s ^ 2 + ((a + b) / 2) ^ 2) * (s ^ 2 + sqrt (a * b) ^ 2)))) ((-1) * ((sqrt (a * b) - a * b / sqrt (a * b)) / 2)) ((-1) * ((/u - a * b / /u) / 2))). apply continuity_implies_RiemannInt; [apply Rmult_le_compat_neg_l;[ | apply incr]; psatzl R | assumption]. assert (ri2_2 := RiemannInt_P1 ri2_pre). assert (ctd_2 : forall x : R, /u <= x <= sqrt (a * b) -> continuity_pt (fun t : R => (-1) * ((1 + a * b / t ^ 2) / 2)) x). intros; reg; apply Rgt_not_eq, pow_lt; psatzl R. assert (eq_2 : forall x : R, / u <= x <= sqrt (a * b) -> / sqrt ((x ^ 2 + a ^ 2) * (x ^ 2 + b ^ 2)) = ((-1) * ((1 + a * b / x ^ 2) / 2)) * -/ (2 * sqrt ((((-1) * ((x - a * b / x) / 2)) ^ 2 + ((a + b) / 2) ^ 2) * (((-1) * ((x - a * b / x) / 2)) ^ 2 + sqrt (a * b) ^ 2)))). intros x intx. set (form := ((-1 * ((x - a * b / x) / 2)) ^ 2 + ((a + b) / 2) ^ 2) * ((-1 * ((x - a * b / x) / 2)) ^ 2 + (sqrt (a * b)) ^ 2)). assert (0 < form) by (apply q2_body_pos; auto; psatzl R). assert (0 < sqrt form) by (apply sqrt_lt_R0; assumption). replace (-1 * ((1 + a * b / x ^ 2) / 2) * - / (2 * sqrt form)) with ((1 + a * b / x ^ 2) * /4 * / sqrt form) by (field;split;apply Rgt_not_eq;psatzl R). assert (sqrt2 : sqrt (a * b ) ^ 2 = a * b) by (simpl; rewrite Rmult_1_r, sqrt_sqrt;try apply Rlt_le; auto). replace form with (((1 + a * b / x ^ 2)/4) ^ 2 * ((x ^ 2 + a ^ 2) * (x ^ 2 + b ^ 2))) by (unfold form; rewrite sqrt2; field; apply Rgt_not_eq; psatzl R). assert (sqrt_sq : forall x, 0 <= x -> sqrt(x^2) = x) by (intros; simpl; rewrite Rmult_1_r, sqrt_square; auto). assert (0 < (1 + a * b / x ^ 2) /4) by lt0. rewrite (sqrt_mult_alt (_ ^ _)), sqrt_pow2;[ | lt0 | lt0]. rewrite (Rinv_mult_distr _ (sqrt _));[ | lt0 | lt0]. rewrite <- (Rmult_assoc _ (/ _) _), Rinv_r, Rmult_1_l; [reflexivity | lt0]. assert (t := RiemannInt_variable_change1' (fun s => -/ (2 * sqrt ((s ^ 2 + ((a + b) / 2) ^ 2) * (s ^ 2 + sqrt (a * b) ^ 2)))) _ (fun t => (-1) * ((t - a * b / t) / 2)) (fun t => (-1) * ((1 + a * b/ t ^ 2) / 2)) (/ u) (sqrt (a * b)) (Rlt_le _ _ Vusab) rVusab ri2_2). assert (ww_pre : /u <= /u <= sqrt (a * b)) by psatzl R. assert (ww := incr'_2 (/u) ww_pre); lazy beta in t. rewrite (Rmin_right (-1 * ((/ u - a * b / / u) / 2)) (-1 * ((sqrt (a * b) - a * b / sqrt (a * b)) / 2))), (Rmax_left (-1 * ((/ u - a * b / / u) / 2)) (-1 * ((sqrt (a * b) - a * b / sqrt (a * b)) / 2))) in t; [|psatzl R | psatzl R]. generalize ri2_2 (t dr_2 incr'_2 ct_2 ctd_2 eq_2); clear t. replace ((sqrt (a * b) - a * b / sqrt (a * b)) / 2) with 0 by (pattern (a * b) at 2; rewrite <- Rsqr_sqrt; unfold Rsqr;[field|];lt0). rewrite Rmult_0_r, Ropp_mult_distr_l_reverse, Rmult_1_l. replace (- ((/ u - a * b / / u) / 2)) with ((a * b * u - /u) / 2);[ | field; psatzl R]. clear ri2; intros ri1_2 q1 ri2 q2. rewrite q1, q2. assert (ri1_2' := RiemannInt_P1 ri1_2). rewrite (RiemannInt_P8 ri1_2 ri1_2'). assert (boundpos : 0 < (a * b * u - / u) / 2). apply Rmult_lt_0_compat;[ | psatzl R]. assert (1 < a * b * u). apply Rmult_lt_reg_l with (/(a * b));[lt0 | ]. rewrite Rmult_1_r, <- Rmult_assoc, Rinv_l, Rmult_1_l; lt0. assert (/u < 1) by (rewrite <- Rinv_1; apply Rinv_lt_contravar; psatzl R). psatzl R. assert (chf0 : forall x : R, - / (2 * sqrt ((x ^ 2 + ((a + b) / 2) ^ 2) * (x ^ 2 + sqrt (a * b) ^ 2))) = - / 2 * / sqrt ((x ^ 2 + ((a + b) / 2) ^ 2) * (x ^ 2 + sqrt (a * b) ^ 2))). intros; field; lt0. assert (chf := fun x (h : Rmin 0 ((a * b * u - / u) / 2) <= x <= Rmax 0 ((a * b * u - / u) / 2)) => chf0 x). assert (chf' := fun x (h : 0 < x < ((a * b * u - / u) / 2)) => chf0 x). assert (ri1_3 : Riemann_integrable (fun s : R => - / 2 * / sqrt ((s ^ 2 + ((a + b) / 2) ^ 2) * (s ^ 2 + sqrt (a * b) ^ 2))) 0 ((a * b * u - / u) / 2)). apply Riemann_integrable_eq with (1 := chf) (2 := ri1_2'); clear ri1_2'. rewrite (RiemannInt_P18 ri1_2' ri1_3 (Rlt_le _ _ boundpos) chf'). rewrite (RiemannInt_scal _ _ _ _ (mf_integrable ((a + b)/2) (sqrt (a * b)) _ _ (q2_2_1_a _ _ a0 b0)(q2_2_1_g _ _ a0 b0)) ri1_3). generalize (mf_integrable ((a + b) / 2) (sqrt (a * b)) 0 ((a * b * u - / u) / 2) (q2_2_1_a a b a0 b0) (q2_2_1_g a b a0 b0)); intros ri1_4. rewrite Ropp_mult_distr_l_reverse, Ropp_involutive. rewrite (RiemannInt_P5 _ (h2 _ boundpos)). replace l2 with (/ 2 * l2 + / 2 * l2) by field. clear chf chf' chf0 ri1_3 ri1_4 ri1_2'. assert (chf0 : forall x : R, / (2 * sqrt ((x ^ 2 + ((a + b) / 2) ^ 2) * (x ^ 2 + sqrt (a * b) ^ 2))) = / 2 * / sqrt ((x ^ 2 + ((a + b) / 2) ^ 2) * (x ^ 2 + sqrt (a * b) ^ 2))). intros; field; lt0. assert (chf := fun x (h : Rmin 0 ((u - a * b / u) / 2) <= x <= Rmax 0 ((u - a * b / u) / 2)) => chf0 x). assert (chf' := fun x (h : 0 < x < ((u - a * b / u) / 2)) => chf0 x). assert (a * b / u < 1). apply Rmult_lt_reg_r with u;[psatzl R | ]. unfold Rdiv; rewrite Rmult_assoc, Rinv_l; psatzl R. assert (boundpos2 : 0 < (u - a * b / u) / 2) by psatzl R. assert (ri2_1 : Riemann_integrable (fun s : R => / 2 * / sqrt ((s ^ 2 + ((a + b) / 2) ^ 2) * (s ^ 2 + sqrt (a * b) ^ 2))) 0 ((u - a * b / u) / 2)). apply Riemann_integrable_eq with (1 := chf) (2 := ri2). apply Rle_lt_trans with (1 := R_dist_plus _ _ _ _). rewrite R_dist_mult_l, Rabs_pos_eq;[ | psatzl R]. rewrite (RiemannInt_P18 ri2 ri2_1 (Rlt_le _ _ boundpos2) chf'). rewrite (RiemannInt_scal _ _ _ _ (mf_integrable ((a + b)/2) (sqrt (a * b)) _ _ (q2_2_1_a _ _ a0 b0)(q2_2_1_g _ _ a0 b0)) ri2_1). generalize (mf_integrable ((a + b) / 2) (sqrt (a * b)) 0 ((u - a * b / u)/2) (q2_2_1_a a b a0 b0) (q2_2_1_g a b a0 b0)); intros ri2_3. rewrite R_dist_mult_l, Rabs_pos_eq;[ | psatzl R]. rewrite (RiemannInt_P5 _ (h2 _ boundpos2)). apply Rplus_lt_compat; rewrite R_dist_sym. apply (Rmult_lt_compat_l (/2));[psatzl R| ]. apply Pk2. assert (/u < 1) by (rewrite <- Rinv_1; apply Rinv_lt_contravar; psatzl R). assert (2 * K2 + 1 < a * b * u);[ | psatzl R]. apply Rmult_lt_reg_r with (/(a * b));[lt0|]. rewrite (Rmult_comm (a * b)), (Rmult_assoc u). rewrite Rinv_r, Rmult_1_r;[| lt0]; assumption. apply (Rmult_lt_compat_l (/2));[psatzl R|]. apply Pk2. assert ( a * b / u < 1);[ | psatzl R]. apply Rmult_lt_reg_r with u;[|unfold Rdiv;rewrite Rmult_assoc,Rinv_l];psatzl R. Qed. Require Import Integral Derive Differential Locally Continuity. Lemma continuity_2d_pt_plus : forall f g x y, continuity_2d_pt f x y -> continuity_2d_pt g x y -> continuity_2d_pt (fun u v => f u v + g u v) x y. intros f g x y cf cg eps. destruct (cf (pos_div_2 eps)) as [delta1 P1]. destruct (cg (pos_div_2 eps)) as [delta2 P2]. assert (m0 : 0 < Rmin delta1 delta2). destruct delta1 as [d1 d1p]; destruct delta2 as [d2 d2p]. simpl in d1p, d2p |- *; apply Rmin_glb_lt; assumption. exists (mkposreal _ m0); simpl; intros u v ux vy. replace (f u v + g u v - (f x y + g x y)) with ((f u v - f x y) + (g u v - g x y)) by ring. apply Rle_lt_trans with (1 := Rabs_triang _ _). replace (pos eps) with (pos_div_2 eps + pos_div_2 eps) by (simpl; field). apply Rplus_lt_compat;[apply P1 | apply P2]. solve[apply Rlt_le_trans with (1 := ux); apply Rmin_l]. solve[apply Rlt_le_trans with (1 := vy); apply Rmin_l]. solve[apply Rlt_le_trans with (1 := ux); apply Rmin_r]. solve[apply Rlt_le_trans with (1 := vy); apply Rmin_r]. Qed. Lemma continuity_2d_pt_mult : forall f g x y, continuity_2d_pt f x y -> continuity_2d_pt g x y -> continuity_2d_pt (fun u v => f u v * g u v) x y. intros f g x y cf cg eps. assert (ndf : 0 < eps/(4 * (Rabs (g x y) + 1))). destruct eps; simpl; lt0. assert (ndg : 0 < (Rmin (eps/(4 * (Rabs (f x y) + 1))) ((Rabs (g x y)) + 1))). (* unfold Rdiv at 1; apply Rmult_lt_0_compat;[ | lt0]. *) apply Rmin_glb_lt;[destruct eps; simpl; lt0 | lt0]. destruct (cf (mkposreal _ ndf)) as [delta1 P1]. destruct (cg (mkposreal _ ndg)) as [delta2 P2]. assert (m0 : 0 < Rmin delta1 delta2). destruct delta1 as [d1 d1p]; destruct delta2 as [d2 d2p]. simpl in d1p, d2p |- *; apply Rmin_glb_lt; assumption. exists (mkposreal _ m0); simpl; intros u v ux vy. replace (f u v * g u v - f x y * g x y) with ((f u v - f x y) * g u v + f x y * (g u v - g x y)) by ring. replace (pos eps) with (pos_div_2 eps + pos_div_2 eps) by (simpl; field). apply Rle_lt_trans with (1 := Rabs_triang _ _). apply Rplus_lt_compat. rewrite Rabs_mult. apply Rle_lt_trans with (Rabs (f u v - f x y) * (2 * (Rabs (g x y) + 1))). apply Rmult_le_compat_l;[solve[apply Rabs_pos] | ]. assert (Rabs (g u v - g x y) < Rabs (g x y) + 1). apply Rlt_le_trans with (2 := Rmin_r (eps/(4 * (Rabs (f x y) + 1))) _). apply P2; apply Rlt_le_trans with (2 := Rmin_r delta1 _); assumption. replace (g u v) with ((g u v - g x y) + g x y) by ring. apply Rle_trans with (1 := Rabs_triang _ _); psatzl R. replace (pos (pos_div_2 eps)) with (eps/ (4 * (Rabs (g x y) + 1)) * (2 * (Rabs (g x y) + 1))) by (simpl; field; apply Rgt_not_eq; lt0). apply Rmult_lt_compat_r;[lt0 | ]. apply P1; apply Rlt_le_trans with (2 := Rmin_l _ delta2); assumption. rewrite Rabs_mult. destruct (Req_EM_T (Rabs (f x y)) 0) as [fxy0 | fxyn0]. rewrite fxy0, Rmult_0_l; case (pos_div_2 eps); intros; assumption. apply Rlt_trans with (Rabs (f x y) * (eps/(4*(Rabs (f x y) + 1)))). apply Rmult_lt_compat_l;[assert (t := Rabs_pos (f x y));psatzl R | ]. apply Rlt_le_trans with (2 := Rmin_l _ (Rabs (g x y) + 1)). apply P2; apply Rlt_le_trans with (2 := Rmin_r delta1 _); assumption. replace (pos (pos_div_2 eps)) with ((2 * (Rabs (f x y) + 1)) * (eps / (4 * (Rabs (f x y) + 1)))); [ | destruct eps; simpl; field; apply Rgt_not_eq; lt0]. apply Rmult_lt_compat_r;[lt0 | ]. assert (t := Rabs_pos (f x y)); psatzl R. Qed. Lemma continuity_2d_pt_id1 : forall x y, continuity_2d_pt (fun u v => u) x y. intros x y eps; exists eps; tauto. Qed. Lemma continuity_2d_pt_id2 : forall x y, continuity_2d_pt (fun u v => v) x y. intros x y eps; exists eps; tauto. Qed. Lemma continuity_2d_pt_const : forall x y c, continuity_2d_pt (fun u v => c) x y. intros x y c eps; exists eps; rewrite Rminus_eq0, Rabs_R0; intros; lt0. Qed. Lemma continuity_2d_pt_continuity : forall f g x y, continuity_pt f (g x y) -> continuity_2d_pt g x y -> continuity_2d_pt (fun x y => f (g x y)) x y. intros f g x y cf cg eps. destruct (cf eps (cond_pos eps)) as [delta [deltapos Pf]]. destruct (cg (mkposreal _ deltapos)) as [gamma Pg]. exists gamma; intros u v cu cv. destruct (Req_EM_T (g x y) (g u v)) as [eqg | neqg]. rewrite eqg, Rminus_eq0, Rabs_R0; lt0. apply (Pf (g u v)). split;[solve[unfold D_x, no_cond; tauto] | ]. apply (Pg u v); assumption. Qed. Lemma q2_body2_pos : forall a b t, 0 < a -> 0 < b -> 0 < a ^ 2 * cos t ^ 2 + b ^ 2 * sin t ^ 2. intros a b t a0 b0. replace (sin t ^ 2) with (Rsqr (sin t)) by (unfold Rsqr; ring). destruct (Req_EM_T ((cos t) ^ 2) 0) as [cos0 | cosn0]. rewrite sin2; replace (Rsqr (cos t)) with ((cos t) ^ 2) by (unfold Rsqr; ring). rewrite cos0, Rminus_0_r, Rmult_1_r, Rmult_0_r, Rplus_0_l; lt0. apply Rplus_lt_le_0_compat;[ | apply Rmult_le_pos;[lt0 | apply Rle_0_sqr]]. apply Rmult_lt_0_compat;[ | assert (t' := pow2_ge_0 (cos t))]; lt0. Qed. Lemma isd1 : forall y b t, 0 < y -> 0 < b -> is_derive (fun u : R => / sqrt (u ^ 2 * cos t ^ 2 + b ^ 2 * sin t ^ 2)) y (- / sqrt (y ^ 2 * cos t ^ 2 + b ^ 2 * sin t ^ 2) ^ 2 * (/ (2 * sqrt (y ^ 2 * cos t ^ 2 + b ^ 2 * sin t ^ 2)) * (INR 2 * y ^ 1 * 1 * cos t ^ 2 + 0))). intros y b t y0 b0. apply derivable_pt_lim_comp. apply (derivable_pt_lim_comp _ sqrt). apply derivable_pt_lim_plus. apply derivable_pt_lim_scal_right. apply (derivable_pt_lim_comp (fun v => v) (fun v => v ^ 2)). apply derivable_pt_lim_id. apply derivable_pt_lim_pow. apply derivable_pt_lim_const. apply derivable_pt_lim_sqrt, q2_body2_pos; assumption. apply derivable_pt_lim_inv, Rgt_not_eq, sqrt_lt_R0, q2_body2_pos; assumption. Qed. Lemma isd2 : forall a y t, 0 < a -> 0 < y -> is_derive (fun u : R => / sqrt (a ^ 2 * cos t ^ 2 + u ^ 2 * sin t ^ 2)) y (- / sqrt (a ^ 2 * cos t ^ 2 + y ^ 2 * sin t ^ 2) ^ 2 * (/ (2 * sqrt (a ^ 2 * cos t ^ 2 + y ^ 2 * sin t ^ 2)) * (0 + INR 2 * y ^ 1 * 1 * sin t ^ 2))). intros a y t a0 y0. apply derivable_pt_lim_comp. apply (derivable_pt_lim_comp _ sqrt). apply derivable_pt_lim_plus. apply derivable_pt_lim_const. apply derivable_pt_lim_scal_right. apply (derivable_pt_lim_comp (fun v => v) (fun v => v ^ 2)). apply derivable_pt_lim_id. apply derivable_pt_lim_pow. apply derivable_pt_lim_sqrt, q2_body2_pos; assumption. apply derivable_pt_lim_inv, Rgt_not_eq, sqrt_lt_R0, q2_body2_pos; assumption. Qed. Require Import AutoDerive. Lemma q2_1_2_bis_a : forall a b, 0 < a -> 0 < b -> is_derive (fun x => I_t x b) a (RInt (fun t : R => Derive (fun u : R => / sqrt (u ^ 2 * cos t ^ 2 + b ^ 2 * sin t ^ 2)) a) 0 (PI/2)). intros a b a0 b0. assert (gbody_pos : forall y t, 0 < y -> 0 < y ^ 2 * cos t ^ 2 + b ^ 2 * sin t ^ 2). intros; apply q2_body2_pos; assumption. assert (exder : locally (fun x : R => forall t : R, Rmin 0 (PI/2) <= t <= Rmax 0 (PI/2) -> ex_derive (fun u : R => / sqrt (u ^ 2 * cos t ^ 2 + b ^ 2 * sin t ^ 2)) x) a). exists (mkposreal _ a0); intros y ya t _. exists (- / sqrt (y ^ 2 * cos t ^ 2 + b ^ 2 * sin t ^ 2) ^ 2 * (/ (2 * sqrt (y ^ 2 * cos t ^ 2 + b ^ 2 * sin t ^ 2)) * (INR 2 * y ^ 1 * 1 * cos t ^ 2 + 0))). apply isd1; apply Rabs_lt_between in ya; simpl in ya; psatzl R. assert (ct2d : forall t, Rmin 0 (PI/2) <= t <= Rmax 0 (PI/2) -> continuity_2d_pt (fun u v => Derive (fun z => /sqrt (z ^ 2 * cos v ^ 2 + b ^ 2 * sin v ^ 2)) u) a t). intros t intt. apply (continuity_2d_pt_ext_loc (fun y t => (- / sqrt (y ^ 2 * cos t ^ 2 + b ^ 2 * sin t ^ 2) ^ 2 * (/ (2 * sqrt (y ^ 2 * cos t ^ 2 + b ^ 2 * sin t ^ 2)) * (INR 2 * y ^ 1 * 1 * cos t ^ 2 + 0))))). exists (pos_div_2 (mkposreal _ a0)); intros u v cu cv; simpl in cu, cv. assert (u0 : 0 < u) by (apply Rabs_lt_between in cu; psatzl R). apply eq_sym, is_derive_unique, isd1; assumption. assert (body_a := gbody_pos a t a0). assert (continuity_2d_pt (fun x y => x ^ 2 * cos y ^ 2 + b ^ 2 * sin y ^ 2) a t). apply continuity_2d_pt_plus. apply continuity_2d_pt_mult. apply (continuity_2d_pt_continuity (fun y => y ^ 2)). solve[reg]. apply continuity_2d_pt_id1. apply (continuity_2d_pt_continuity (fun y => y ^ 2)). solve[reg]. apply continuity_2d_pt_continuity; [apply continuity_cos | apply continuity_2d_pt_id2 ]. apply continuity_2d_pt_mult;[apply continuity_2d_pt_const | ]. apply (continuity_2d_pt_continuity (fun y => y ^ 2));[reg | ]. apply continuity_2d_pt_continuity; [apply continuity_sin | apply continuity_2d_pt_id2 ]. apply continuity_2d_pt_mult. apply (continuity_2d_pt_continuity (fun y => - / y)). solve[reg; lt0]. apply (continuity_2d_pt_continuity (fun y => sqrt y ^ 2)). solve[reg; lt0]. assumption. apply continuity_2d_pt_mult. apply (continuity_2d_pt_continuity (fun y => / (2 * sqrt y))). solve[reg; lt0]. assumption. apply (continuity_2d_pt_ext (fun u v => (2 * u * (cos v) ^ 2))). intros; simpl; ring. apply continuity_2d_pt_mult. apply continuity_2d_pt_mult; [apply continuity_2d_pt_const | apply continuity_2d_pt_id1 ]. apply (continuity_2d_pt_continuity (fun y => cos y ^ 2)). solve[reg]. apply continuity_2d_pt_id2. assert (exr : locally (fun y => ex_RInt (fun t => /sqrt (y ^ 2 * cos t ^ 2 + b ^ 2 * sin t ^ 2)) 0 (PI / 2)) a). exists (pos_div_2 (mkposreal _ a0)); intros y cy; simpl in cy. apply ex_RInt_correct_1. apply q2_1_2_aux; apply Rabs_lt_between in cy; psatzl R. generalize (derivable_pt_lim_param _ 0 (PI/2) a exder ct2d exr). apply derivable_pt_lim_eq with (a := a/2) (b := a + 1). psatzl R. intros y inty. assert (y0 : 0 < y) by psatzl R. rewrite (RInt_correct _ _ _ (q2_1_2_aux y b y0 b0)). rewrite q2_1_2_t; unfold I2_t. destruct (Rlt_dec 0 y) as [? | yn0];[ | clear - y0 yn0; psatzl R; psatzl R]. destruct (Rlt_dec 0 b) as [? | bn0];[ | clear - b0 bn0; psatzl R; psatzl R]. apply RiemannInt_P5. Qed. Lemma pow2_sqrt : forall x, 0 <= x -> sqrt x ^ 2 = x. intros x x0; simpl; rewrite Rmult_1_r, sqrt_sqrt; auto. Qed. Require Import AutoDerive. Lemma q2_body2_lb : forall a b t, Rmin (a ^ 2) (b ^ 2) <= a ^ 2 * cos t ^ 2 + b ^ 2 * sin t ^ 2. intros a b t; set (u := Rmin (a ^ 2) (b ^ 2)). rewrite <- (Rmult_1_r u), <- (sin2_cos2 t), Rplus_comm. replace (Rsqr (cos t)) with (cos t ^ 2) by (unfold Rsqr; ring). replace (Rsqr (sin t)) with (sin t ^ 2) by (unfold Rsqr; ring). rewrite Rmult_plus_distr_l; apply Rplus_le_compat. apply Rmult_le_compat_r;[apply pow2_ge_0 | apply Rmin_l]. apply Rmult_le_compat_r;[apply pow2_ge_0 | apply Rmin_r]. Qed. Lemma bound_I_deriv_a : forall a b, 0 < a -> 0 < b -> exists bound, forall x b', a < x < 4 * a -> b <= b' -> Rabs (Derive (fun y => I_t y b') x) <= bound. intros a b a0 b0. assert (exists bnd1, forall x t b', a < x -> x < 4 * a -> b <= b' -> Rabs (Derive (fun y => /sqrt(y ^ 2 * cos t ^ 2 + b' ^ 2 * sin t ^ 2)) x) <= bnd1) as [bnd1 P1]. exists (/Rmin (a ^ 2) (b ^ 2) * (/(2 * sqrt (Rmin (a ^ 2) (b ^ 2))) * (8 * a))). intros x t b' ax x2a bb'; assert (x0 : 0 < x) by psatzl R. assert (b'0 : 0 < b') by psatzl R. assert (dif : a ^ 2 * cos t ^ 2 + b ^ 2 * sin t ^ 2 <= x ^ 2 * cos t ^ 2 + b' ^ 2 * sin t ^ 2). apply Rplus_le_compat; apply Rmult_le_compat_r; try apply pow2_ge_0; apply pow_incr; psatzl R. assert (gbody := q2_body2_pos _ _ t x0 b'0). rewrite (is_derive_unique _ x _ (isd1 _ _ _ x0 b'0)). rewrite Rabs_mult; apply Rmult_le_compat; try apply Rabs_pos. rewrite Rabs_Ropp, Rabs_pos_eq;[ |lt0]. apply Rle_Rinv;[lt0 | lt0 | ]. rewrite pow2_sqrt;[|lt0]. solve[apply Rle_trans with (1 := q2_body2_lb a b t), dif]. rewrite Rabs_mult; apply Rmult_le_compat; try apply Rabs_pos. rewrite Rabs_pos_eq;[ | lt0]; apply Rle_Rinv;[lt0 | lt0 | ]. apply Rmult_le_compat_l;[lt0 | ]. solve[apply sqrt_le_1_alt, Rle_trans with (1 := q2_body2_lb a b t), dif]. replace (INR 2) with 2 by (simpl; ring); rewrite Rplus_0_r. rewrite Rabs_pos_eq;[ | solve[apply Rmult_le_pos;[lt0 | apply pow2_ge_0]]]. apply Rle_trans with (2 * x ^ 1 * 1 * 1);[ | psatzl R]. apply Rmult_le_compat_l;[lt0|]. rewrite <- (sin2_cos2 t). replace (cos t ^ 2) with (Rsqr (cos t)) by (unfold Rsqr;ring). assert (t' := Rle_0_sqr (sin t)); psatzl R. exists (PI/2 * bnd1); intros x b' ax bb'; assert (b'0 : 0 < b') by psatzl R. assert (x0 : 0 < x) by psatzl R. rewrite (is_derive_unique _ x _ (q2_1_2_bis_a x b' x0 b'0)). replace (PI/2 * bnd1) with (Rabs (PI/2 - 0) * bnd1) by (rewrite Rabs_pos_eq;[ring | assert (t := PI_RGT_0); psatzl R]). apply RInt_le_const. apply ex_RInt_cont; intros t _. apply (continuity_pt_eq (fun t => (- / sqrt (x ^ 2 * cos t ^ 2 + b' ^ 2 * sin t ^ 2) ^ 2 * (/ (2 * sqrt (x ^ 2 * cos t ^ 2 + b' ^ 2 * sin t ^ 2)) * (INR 2 * x ^ 1 * 1 * cos t ^ 2 + 0)))) _ 1 t). psatzl R. intros y _; apply eq_sym, is_derive_unique; apply isd1; assumption. reg; assert (t' := q2_body2_pos x b' t x0 b'0); lt0. intros; apply (P1 x t); try psatzl R. Qed. Lemma q2_1_2_bis_b : forall a b, 0 < a -> 0 < b -> is_derive (fun x => I_t a x) b (RInt (fun t : R => Derive (fun u : R => / sqrt (a ^ 2 * cos t ^ 2 + u ^ 2 * sin t ^ 2)) b) 0 (PI/2)). intros a b a0 b0. assert (gbody_pos : forall y t, 0 < y -> 0 < a ^ 2 * cos t ^ 2 + y ^ 2 * sin t ^ 2). intros; apply q2_body2_pos; assumption. assert (exder : locally (fun x : R => forall t : R, Rmin 0 (PI/2) <= t <= Rmax 0 (PI/2) -> ex_derive (fun u : R => / sqrt (a ^ 2 * cos t ^ 2 + u ^ 2 * sin t ^ 2)) x) b). exists (mkposreal _ b0); intros y yb t _. exists (- / sqrt (a ^ 2 * cos t ^ 2 + y ^ 2 * sin t ^ 2) ^ 2 * (/ (2 * sqrt (a ^ 2 * cos t ^ 2 + y ^ 2 * sin t ^ 2)) * (0 + INR 2 * y ^ 1 * 1 * sin t ^ 2))). apply isd2; apply Rabs_lt_between in yb; simpl in yb; psatzl R. assert (ct2d : forall t, Rmin 0 (PI/2) <= t <= Rmax 0 (PI/2) -> continuity_2d_pt (fun u v => Derive (fun z => /sqrt (a ^ 2 * cos v ^ 2 + z ^ 2 * sin v ^ 2)) u) b t). intros t intt. apply (continuity_2d_pt_ext_loc (fun y t => (- / sqrt (a ^ 2 * cos t ^ 2 + y ^ 2 * sin t ^ 2) ^ 2 * (/ (2 * sqrt (a ^ 2 * cos t ^ 2 + y ^ 2 * sin t ^ 2)) * (0 + INR 2 * y ^ 1 * 1 * sin t ^ 2))))). exists (pos_div_2 (mkposreal _ b0)); intros u v cu cv; simpl in cu, cv. assert (u0 : 0 < u) by (apply Rabs_lt_between in cu; psatzl R). apply eq_sym, is_derive_unique, isd2; assumption. assert (body_b := gbody_pos b t b0). assert (continuity_2d_pt (fun x y => a ^ 2 * cos y ^ 2 + x ^ 2 * sin y ^ 2) b t). apply continuity_2d_pt_plus. apply continuity_2d_pt_mult;[apply continuity_2d_pt_const | ]. apply (continuity_2d_pt_continuity (fun y => y ^ 2));[reg | ]. apply continuity_2d_pt_continuity; [apply continuity_cos | apply continuity_2d_pt_id2 ]. apply continuity_2d_pt_mult. apply (continuity_2d_pt_continuity (fun y => y ^ 2)). solve[reg]. apply continuity_2d_pt_id1. apply (continuity_2d_pt_continuity (fun y => y ^ 2)). solve[reg]. apply continuity_2d_pt_continuity; [apply continuity_sin | apply continuity_2d_pt_id2 ]. apply continuity_2d_pt_mult. apply (continuity_2d_pt_continuity (fun y => - / sqrt y ^ 2)). solve[reg; lt0]. assumption. apply continuity_2d_pt_mult. apply (continuity_2d_pt_continuity (fun y => / (2 * sqrt y))). solve[reg; lt0]. assumption. apply (continuity_2d_pt_ext (fun u v => (2 * u * (sin v) ^ 2))). intros; simpl; ring. apply continuity_2d_pt_mult. apply continuity_2d_pt_mult; [apply continuity_2d_pt_const | apply continuity_2d_pt_id1 ]. apply (continuity_2d_pt_continuity (fun y => sin y ^ 2)). solve[reg]. apply continuity_2d_pt_id2. assert (exr : locally (fun y => ex_RInt (fun t => /sqrt (a ^ 2 * cos t ^ 2 + y ^ 2 * sin t ^ 2)) 0 (PI / 2)) b). exists (pos_div_2 (mkposreal _ b0)); intros y cy; simpl in cy. apply ex_RInt_correct_1. apply q2_1_2_aux; apply Rabs_lt_between in cy; psatzl R. generalize (derivable_pt_lim_param _ 0 (PI/2) b exder ct2d exr). apply derivable_pt_lim_eq with (a := b/2) (b := b + 1). psatzl R. intros y inty. assert (y0 : 0 < y) by psatzl R. rewrite (RInt_correct _ _ _ (q2_1_2_aux a y a0 y0)). rewrite q2_1_2_t; unfold I2_t. destruct (Rlt_dec 0 a) as [? | yn0];[ | clear - y0 yn0; psatzl R; psatzl R]. destruct (Rlt_dec 0 y) as [? | bn0];[ | clear - b0 bn0; psatzl R; psatzl R]. apply RiemannInt_P5. Qed. Lemma bound_I_deriv_b : forall a b, 0 < a -> 0 < b -> exists bound, forall x a', b < x < 4 * b -> a <= a' -> Rabs (Derive (fun y => I_t a' y) x) <= bound. intros a b a0 b0. assert (exists bnd1, forall x t a', b < x -> x < 4 * b -> a <= a' -> Rabs (Derive (fun y => /sqrt(a' ^ 2 * cos t ^ 2 + y ^ 2 * sin t ^ 2)) x) <= bnd1) as [bnd1 P1]. exists (/Rmin (a ^ 2) (b ^ 2) * (/(2 * sqrt (Rmin (a ^ 2) (b ^ 2))) * (8 * b))). intros x t a' bx x2b aa'; assert (x0 : 0 < x) by psatzl R. assert (a'0 : 0 < a') by psatzl R. assert (dif : a ^ 2 * cos t ^ 2 + b ^ 2 * sin t ^ 2 <= a' ^ 2 * cos t ^ 2 + x ^ 2 * sin t ^ 2). apply Rplus_le_compat; apply Rmult_le_compat_r; try apply pow2_ge_0; apply pow_incr; psatzl R. assert (gbody := q2_body2_pos _ _ t a'0 x0). rewrite (is_derive_unique _ x _ (isd2 _ _ _ a'0 x0)). rewrite Rabs_mult; apply Rmult_le_compat; try apply Rabs_pos. rewrite Rabs_Ropp, Rabs_pos_eq;[ |lt0]. apply Rle_Rinv;[lt0 | lt0 | ]. rewrite pow2_sqrt;[|lt0]. solve[apply Rle_trans with (1 := q2_body2_lb a b t), dif]. rewrite Rabs_mult; apply Rmult_le_compat; try apply Rabs_pos. rewrite Rabs_pos_eq;[ | lt0]; apply Rle_Rinv;[lt0 | lt0 | ]. apply Rmult_le_compat_l;[lt0 | ]. solve[apply sqrt_le_1_alt, Rle_trans with (1 := q2_body2_lb a b t), dif]. replace (INR 2) with 2 by (simpl; ring); rewrite Rplus_0_l. rewrite Rabs_pos_eq;[ | solve[apply Rmult_le_pos;[lt0 | apply pow2_ge_0]]]. apply Rle_trans with (2 * x ^ 1 * 1 * 1);[ | psatzl R]. apply Rmult_le_compat_l;[lt0|]. rewrite <- (sin2_cos2 t). replace (sin t ^ 2) with (Rsqr (sin t)) by (unfold Rsqr;ring). assert (t' := Rle_0_sqr (cos t)); psatzl R. exists (PI/2 * bnd1); intros x a' bx aa'. assert (a'0 : 0 < a') by psatzl R. assert (x0 : 0 < x) by psatzl R. rewrite (is_derive_unique _ x _ (q2_1_2_bis_b a' x a'0 x0)). replace (PI/2 * bnd1) with (Rabs (PI/2 - 0) * bnd1) by (rewrite Rabs_pos_eq;[ring | assert (t := PI_RGT_0); psatzl R]). apply RInt_le_const. apply ex_RInt_cont; intros t _. apply (continuity_pt_eq (fun t => (- / sqrt (a' ^ 2 * cos t ^ 2 + x ^ 2 * sin t ^ 2) ^ 2 * (/ (2 * sqrt (a' ^ 2 * cos t ^ 2 + x ^ 2 * sin t ^ 2)) * (0 + INR 2 * x ^ 1 * 1 * sin t ^ 2)))) _ 1 t). psatzl R. intros y _; apply eq_sym, is_derive_unique; apply isd2; assumption. reg; assert (t' := q2_body2_pos a' x t a'0 x0); lt0. intros; apply (P1 x t); psatzl R. Qed. Lemma q2_2_1_bis : forall a b (a0 : 0 < a) (b0 : 0 < b) n, I_t (fst (ag a b n)) (snd (ag a b n)) = I_t a b. intros a b a0 b0; induction n. reflexivity. replace (fst (ag a b (S n))) with ((fst (ag a b n) + snd (ag a b n))/2) by (simpl; destruct (ag a b n); reflexivity). replace (snd (ag a b (S n))) with (sqrt ((fst (ag a b n) * snd (ag a b n)))) by (simpl; destruct (ag a b n); reflexivity). rewrite <- IHn; apply eq_sym, q2_2_1; destruct (ag_positive n a b); tauto. Qed. Lemma partial_derivative_bound_continuity_2d : forall f f1' f2' a b, (exists bound1, locally_2d (fun a' b' => is_derive (fun y => f y b') a' (f1' a' b') /\ Rabs (f1' a' b') <= bound1) a b) -> (exists bound2, locally_2d (fun a' b' => is_derive (fun y => f a' y) b' (f2' a' b') /\ Rabs (f2' a' b') <= bound2) a b) -> continuity_2d_pt f a b. intros f f1' f2' a b [bnd1 [d1 P1]] [bnd2 [d2 P2]] [eps ep]. assert (d1/2 < d1) by (destruct d1; simpl; psatzl R). assert (ctf2 : continuity_pt (fun y => f a y) b). apply derivable_continuous_pt; exists (f2' a b). destruct (P2 a b); try (rewrite Rminus_eq0, Rabs_R0; apply cond_pos). assumption. assert (ep2 : 0 < eps/2) by psatzl R. destruct (ctf2 _ ep2) as [delta1 [delta1p Pd1]]. set (delta2 := Rmin (delta1/2) (d1/2)). assert (delta2 < delta1). unfold delta2; apply Rle_lt_trans with (1 := Rmin_l _ _); psatzl R. assert (cond_snd_coord : forall v, Rabs (v - b) < delta2 -> Rabs (f a v - f a b) < eps/2). intros v cv; destruct (Req_EM_T v b) as [v0 |vn0]; [rewrite v0, Rminus_eq0, Rabs_R0; assumption | ]. apply Pd1;split;[split;unfold no_cond; auto | apply Rlt_trans with (1:=cv) ]. assumption. assert (0 < delta2) by (unfold delta2; lt0). assert (delta2 <= d1/2) by (apply Rmin_r). assert (0 <= bnd1) as [bnd2_0 | bnd2_0]. apply Rle_trans with (1 := Rabs_pos (f1' a b)). destruct (P1 a b); try (rewrite Rminus_eq0, Rabs_R0; apply cond_pos); assumption. assert (Rmin delta2 (eps/2 * /bnd1) <= d1 / 2). apply Rle_trans with (1 := Rmin_l _ _), Rmin_r. assert (pv : 0 < Rmin delta2 (eps/2 * /bnd1)) by lt0. exists (mkposreal _ pv). intros u v cu cv; simpl. replace (f u v - f a b) with ((f u v - f a v) + (f a v - f a b)) by ring. replace eps with (eps/2 + eps/2) by field. apply Rle_lt_trans with (1 := Rabs_triang _ _). apply Rplus_lt_compat. destruct (Req_EM_T u a) as [ua | una]; [rewrite ua, Rminus_eq0, Rabs_R0; psatzl R|]. assert (cu' : Rabs (u - a) < d1/2). apply Rlt_le_trans with (1 := cu), (Rle_trans _ _ _ (Rmin_l _ _)), Rmin_r. assert (exd1 : forall c, Rabs (c - a) <= d1/2 -> ex_derive (fun x => f x v) c). intros c cc; exists (f1' c v); apply P1; simpl in cv; psatzl R. destruct (MVT_cor4 (fun x => f x v) a _ exd1 u (Rlt_le _ _ cu')) as [c [dif cc]]. assert (ccd1 : Rabs (c - a) <= d1/2) by psatzl R. assert (isd1 : is_derive (fun x => f x v) c (f1' c v)). apply P1; simpl in cv; psatzl R. rewrite dif, (is_derive_unique _ _ _ isd1), Rabs_mult. destruct (P1 c v) as [_ f1'cb]; try (simpl in cv; psatzl R). apply Rle_lt_trans with (bnd1 * Rabs (u - a)). apply Rmult_le_compat_r;[solve [apply Rabs_pos]| assumption]. apply (Rmult_lt_reg_r (/bnd1));[lt0 | ]. rewrite (Rmult_comm bnd1), Rmult_assoc, Rinv_r, Rmult_1_r;[|lt0]. apply Rlt_le_trans with (1 := cu), Rmin_r. destruct (Req_EM_T v b) as [vb | vnb]. rewrite vb, Rminus_eq0, Rabs_R0; assumption. apply cond_snd_coord, Rlt_le_trans with (1 := cv), Rmin_l. assert (pv : 0 < delta2) by lt0. exists (mkposreal _ pv). simpl; intros u v cu cv. replace (f u v - f a b) with ((f u v - f a v) + (f a v - f a b)) by ring. apply Rle_lt_trans with (1 := Rabs_triang _ _). assert (exd1 : forall c, Rabs (c - a) <= d1/2 -> ex_derive (fun x => f x v) c). intros c cc; exists (f1' c v); apply P1; simpl in cv; psatzl R. assert (cu' : Rabs (u - a) <= d1/2) by psatzl R. destruct (MVT_cor4 (fun x => f x v) a _ exd1 u cu') as [c [dif cc]]. assert (isd1 : is_derive (fun x => f x v) c (f1' c v)) by (apply P1; simpl in cv; psatzl R). rewrite dif, (is_derive_unique _ _ _ isd1), Rabs_mult. destruct (P1 c v) as [_ f1'cb]; try (simpl in cv; psatzl R). rewrite <- bnd2_0 in f1'cb. assert (w: f1' c v = 0) by (apply Rabs_eq_0, Rle_antisym; auto; apply Rabs_pos). rewrite w, Rabs_R0, Rmult_0_l, Rplus_0_l. apply Rlt_trans with (1 := cond_snd_coord _ cv); psatzl R. Qed. Lemma continuity_2d_pt_I_t : forall a b, 0 < a -> 0 < b -> continuity_2d_pt (fun x y => I_t x y) a b. intros a b a0 b0. assert (a2_0 : 0 < a/2) by psatzl R. assert (b2_0 : 0 < b/2) by psatzl R. set (d := Rmin (a/2) (b/2)). assert (d <= a/2) by apply Rmin_l. assert (d <= b/2) by apply Rmin_r. assert (d0 : 0 < d) by (unfold d; lt0). apply (partial_derivative_bound_continuity_2d (fun x y => I_t x y)) with (f1' := fun x y => RInt (fun t => Derive (fun x => / sqrt(x ^ 2 * cos t ^ 2 + y ^ 2 * sin t ^ 2)) x) 0 (PI/2)) (f2' := fun x y => RInt (fun t => Derive (fun y => / sqrt(x ^ 2 * cos t ^ 2 + y ^ 2 * sin t ^ 2)) y) 0 (PI/2)). destruct (bound_I_deriv_a (a/2) (b/2) a2_0 b2_0) as [bnd1 P1]. exists bnd1; exists (mkposreal _ d0); intros u v cu cv. simpl in cu, cv; apply Rabs_lt_between in cu; apply Rabs_lt_between in cv. assert (u0 : 0 < u) by psatzl R; assert (v0 : 0 < v) by psatzl R. assert (isd := q2_1_2_bis_a u v u0 v0). split;[exact isd | rewrite <- (is_derive_unique _ _ _ isd)]. apply P1; psatzl R. destruct (bound_I_deriv_b (a/2) (b/2) a2_0 b2_0) as [bnd1 P1]. exists bnd1; exists (mkposreal _ d0); intros u v cu cv. simpl in cu, cv; apply Rabs_lt_between in cu; apply Rabs_lt_between in cv. assert (u0 : 0 < u) by psatzl R; assert (v0 : 0 < v) by psatzl R. assert (isd := q2_1_2_bis_b u v u0 v0). split;[exact isd | rewrite <- (is_derive_unique _ _ _ isd)]. apply P1; psatzl R. Qed. Lemma continuity_pt_I_t_a : forall a b, 0 < a -> 0 < b -> continuity_pt (fun y => I_t y b) a. intros a b a0 b0. apply derivable_continuous_pt. eapply exist; eapply q2_1_2_bis_a; assumption. Qed. Lemma continuity_pt_I_t_b : forall a b, 0 < a -> 0 < b -> continuity_pt (fun y => I_t a y) b. intros a b a0 b0. apply derivable_continuous_pt. eapply exist; eapply q2_1_2_bis_b; assumption. Qed. Lemma M_pos : forall a b, 0 < a -> 0 < b -> 0 < M a b. intros a b a0 b0. apply Rlt_le_trans with (snd (ag a b (0 + 1))); [apply ag_positive; assumption| ]. apply (growing_ineq (fun n => snd (ag a b (n + 1)))). apply bn_growing; psatzl R. apply (CV_shift' (fun n => (snd (ag a b n))) 1), M_def'; psatzl R. Qed. Lemma q2_2_2 : forall a b (a0 : 0 < a) (b0 : 0 < b), I_t a b = PI/2 * /M a b. intros a b a0 b0; apply Req_lt_aux; intros eps. assert (M_def := M_def _ _ (Rlt_le _ _ a0) (Rlt_le _ _ b0)). assert (M_def' := M_def' _ _ (Rlt_le _ _ a0) (Rlt_le _ _ b0)). assert (ct : continuity_pt (fun x => PI/2 * / x) (M a b)). reg; apply Rgt_not_eq, M_pos; assumption. assert (Mp : 0 < M a b) by (apply M_pos; assumption). destruct (continuity_2d_pt_I_t _ _ Mp Mp eps) as [delta P1]. destruct (M_def (pos delta) (cond_pos delta)) as [N1 Pn1]. destruct (M_def' (pos delta) (cond_pos delta)) as [N2 Pn2]. set (N := max N1 N2). rewrite <- (q2_2_1_bis a b a0 b0 N). replace (I_t (fst (ag a b N)) (snd (ag a b N)) - PI / 2 * / M a b) with ((I_t (fst (ag a b N)) (snd (ag a b N)) - I_t (M a b) (M a b)) + (I_t (M a b) (M a b) - PI / 2 * / M a b)) by ring. replace (I_t (M a b) (M a b) - PI / 2 * / M a b) with 0. rewrite Rplus_0_r. apply P1;[apply (Pn1 N), Max.le_max_l | apply (Pn2 N), Max.le_max_r]. rewrite q2_1_2_t; unfold I2_t. destruct (Rlt_dec 0 (M a b));[ | psatzl R; psatzl R]. rewrite <- RInt_correct, <- (RInt_ext (fun x => /M a b)), RInt_const;[ring |]. intros x intx; rewrite <- Rmult_plus_distr_l. replace (cos x ^ 2 + sin x ^ 2) with 1 by (rewrite <- (sin2_cos2 x); unfold Rsqr; ring). simpl; rewrite !Rmult_1_r, sqrt_square;[reflexivity | lt0]. Qed. Lemma Rsqr_pow2 : forall x, Rsqr x = x ^ 2. (* TODO : standard. *) intros; unfold Rsqr; ring. Qed. Lemma is_derive_ff : forall x, 0 < x < 1 -> is_derive ff x (- ((PI/2) * (/I_t 1 x ^ 2 * Derive (I_t 1) x))). intros x intx. replace (- ((PI/2) * (/I_t 1 x ^ 2 * Derive (I_t 1) x))) with ((PI/2) * (-/I_t 1 x ^ 2 * Derive (I_t 1) x)) by ring. apply (derivable_pt_lim_eq (fun y => (PI/2) / I_t 1 y) _ x 0 1). assumption. intros z intz; rewrite (q2_2_2 1 z Rlt_0_1 (proj1 intz)). unfold ff; field; split; [apply Rgt_not_eq, M_pos | ]; lt0. apply derivable_pt_lim_scal. apply (derivable_pt_lim_comp _ Rinv). apply Derive_correct; eapply ex_intro; eapply q2_1_2_bis_b; lt0. apply derivable_pt_lim_inv. assert (mp := M_pos 1 x); rewrite q2_2_2; lt0. Qed. Lemma ex_derive_ff : forall x, 0 < x < 1 -> ex_derive ff x. intros x intx; eapply ex_intro; eapply is_derive_ff; assumption. Qed. Lemma derive_ff_pos : forall x, 0 < x < 1 -> 0 < Derive ff x. intros x intx; rewrite (is_derive_unique _ _ _ (is_derive_ff x intx)). rewrite <- Ropp_mult_distr_r_reverse, <- Ropp_mult_distr_r_reverse. apply Rmult_lt_0_compat;[lt0 | ]. apply Rmult_lt_0_compat;[apply Rinv_0_lt_compat | ]. rewrite q2_2_2; assert (t := M_pos 1 x); lt0. set (f := fun t => (- / sqrt (1 ^ 2 * cos t ^ 2 + x ^ 2 * sin t ^ 2) ^ 2 * (/ (2 * sqrt (1 ^ 2 * cos t ^ 2 + x ^ 2 * sin t ^ 2)) * (0 + INR 2 * x ^ 1 * 1 * sin t ^ 2)))). assert (cmp : forall u, 0 <= u <= PI/2 -> 0 < 1 ^ 2 * cos u ^ 2 + x ^ 2 * sin u ^ 2). intros u intu; case (Req_EM_T u 0) as [u0 | un0]. simpl; rewrite u0, sin_0, cos_0, Rmult_0_l, !Rmult_1_l. rewrite Rmult_0_r, Rplus_0_r; lt0. assert (0 < sin u) by (apply sin_gt_0; lt0); rewrite <- Rpow_mult_distr; lt0. assert (ctd : forall t, 0 <= t <= PI/2 -> continuity_pt f t). intros u intu; unfold f; assert (cmpu := cmp u intu); reg; lt0. assert (ctd4 : forall t, PI/4 <= t <= PI/2 -> continuity_pt f t). intros u intu; apply ctd; psatzl R. assert (PI20 : 0 <= PI/2) by lt0. assert (PI24 : PI/4 <= PI/2) by psatzl R. destruct (continuity_ab_maj _ (PI/4) (PI/2) PI24 ctd4) as [mn [Pmn intmn]]. rewrite <- (Derive_ext (fun x => I_t 1 x));[ | reflexivity]. rewrite (is_derive_unique _ _ _ (q2_1_2_bis_b 1 x Rlt_0_1 (proj1 intx))). assert (exIf : ex_RInt f 0 (PI/2)). apply ex_RInt_cont; rewrite Rmin_left, Rmax_right; assumption. rewrite (RInt_ext _ f 0 (PI/2)) by (intros u; rewrite Rmin_left, Rmax_right; try assumption; intros intu; apply is_derive_unique, isd2; lt0). assert (ex_RInt f 0 (PI/4)) by (apply ex_RInt_included1 with (1 := exIf); lt0). assert (ex_RInt f (PI/4) (PI/2)) by (apply ex_RInt_included2 with (1 := exIf); lt0). rewrite <- (RInt_Chasles f 0 (PI/4) (PI/2)); [ | assumption | assumption ]. rewrite Ropp_plus_distr; apply Rplus_le_lt_0_compat. apply Rle_trans with (- RInt (fun _ => 0) 0 (PI/4)). rewrite RInt_const, Rmult_0_l, Ropp_0; apply Rle_refl. apply Ropp_le_contravar, RInt_le;[lt0 | assumption| apply ex_RInt_const| ]. intros u intu; unfold f. rewrite Rplus_0_l, Rmult_1_r, <- Ropp_0. rewrite !Ropp_mult_distr_l_reverse; apply Ropp_le_contravar. assert (intu' : 0 <= u <= PI/2) by psatzl R. assert (cmpu := cmp _ intu'). simpl INR; repeat apply Rmult_le_pos; try lt0; apply sin_ge_0; psatzl R. apply Rlt_le_trans with (- (RInt (fun _ => f mn) (PI/4) (PI/2))). rewrite RInt_const, <- Ropp_mult_distr_l_reverse. assert (t:= PI_RGT_0); apply Rmult_lt_0_compat;[ | psatzl R]. assert (0 < sin mn) by (apply sin_gt_0; psatzl R). assert (intm' : 0 <= mn <= PI/2) by psatzl R; assert (cmpmn := cmp _ intm'). unfold f; rewrite <- !Ropp_mult_distr_l_reverse, Ropp_involutive. simpl INR; rewrite Rplus_0_l; lt0. apply Ropp_le_contravar, RInt_le; try assumption; apply ex_RInt_const. Qed. Definition pre_w_ (n : nat) (a b : R) := sqrt (fst (ag a b n) ^ 2 - snd (ag a b n) ^ 2). Definition v_ (n : nat) (x : R) := snd (ag 1 x n). Definition w_ (n : nat) (x : R) := pre_w_ n 1 x. Lemma u_step : forall x n, u_ (S n) x = (u_ n x + v_ n x)/2. intros x n; unfold u_, v_; simpl; destruct (ag 1 x n); reflexivity. Qed. Lemma v_step : forall x n, v_ (S n) x = sqrt (u_ n x * v_ n x). intros x n; unfold u_, v_; simpl; destruct (ag 1 x n); reflexivity. Qed. Lemma u_pos : forall x n, 0 < x < 1 -> 0 < u_ n x. intros x n intx; unfold u_; destruct (ag_positive n 1 x); psatzl R. Qed. Lemma v_pos : forall x n, 0 < x < 1 -> 0 < v_ n x. intros x n intx; unfold v_; destruct (ag_positive n 1 x); psatzl R. Qed. Lemma cmp_u_v : forall x n, 0 < x < 1 -> v_ n x < u_ n x. intros x [ | n] intx. unfold u_, v_; simpl; psatzl R. destruct (ag_diff_maj 1 x (S n));[omega | psatzl R | psatzl R | ]. destruct (q1_1_1 1 x (S n)); try psatzl R; try omega. unfold u_, v_; psatzl R. Qed. Lemma pre_w_pos : forall x n, 0 < x < 1 -> 0 < u_ n x ^ 2 - v_ n x ^ 2. intros x n intx; assert (dif := cmp_u_v x n intx). assert (vp := v_pos x n intx). rewrite <- !Rsqr_pow2; apply Rlt_Rminus, Rsqr_incrst_1; psatzl R. Qed. Lemma w_pos : forall x n, 0 < x < 1 -> 0 < w_ n x. intros x n intx; apply sqrt_lt_R0, pre_w_pos; assumption. Qed. Lemma q3_1_1 : forall a b n, 0 < a -> 0 < b -> b < a -> 2 * M (fst (ag a b (S n))) (pre_w_ (S n) a b) = M (fst (ag a b n)) (pre_w_ n a b). intros a b n a0 b0 ba. assert (pos_ag := ag_positive n a b a0 b0). unfold pre_w_; rewrite ag_unfold; unfold fst, snd; lazy zeta beta. assert (dif := q1_1_1_cor a b n a0 b0 ba). destruct (ag a b n) as [a' b']; simpl in pos_ag, dif. rewrite <- (q1_2_1 ((a' + b')/2) _ 1); lazy zeta beta;[ | psatzl R | apply sqrt_pos]. rewrite !ag_unfold; unfold fst, snd; lazy zeta beta; unfold ag. rewrite pow2_sqrt;[ | lt0]. replace (((a' + b')/2) ^ 2 - a' * b') with (((a' - b')/2) ^ 2) by field. rewrite sqrt_pow2;[|psatzl R]. replace ((a' + b') / 2 + (a' - b') / 2) with a' by field. replace ((a' + b')/2 * ((a' - b') / 2)) with ((a' ^ 2 - b' ^ 2)/(2 ^ 2)) by field. rewrite sqrt_div_alt;[|psatzl R]. unfold Rdiv; rewrite sqrt_pow2, !(Rmult_comm _ (/2)), q1_2_3; try psatzl R. apply sqrt_pos. Qed. Lemma q3_1_1' : forall x n, 0 < x < 1 -> 2 ^ n * M (u_ n x) (w_ n x) = ff (sqrt (1 - x ^ 2)). intros x n intx; unfold u_, w_. induction n. unfold pre_w_, ag, ff, fst, snd; rewrite pow1, pow_O, Rmult_1_l; reflexivity. replace (2 ^ S n) with (2 ^ n * 2) by (simpl; ring); rewrite Rmult_assoc. rewrite q3_1_1; psatzl R. Qed. Lemma q3_1_2 : forall x, 0 < x < 1 -> Un_cv (fun n => 2 ^ n * ff (w_ n x / u_ n x)) (ff (sqrt (1 - x ^ 2)) / ff x). intros x intx. apply (Un_cv_ext (fun n => ff (sqrt(1 - x ^ 2)) / u_ n x)). intros n. destruct (ag_positive n 1 x) as [u_pos v_pos]; try psatzl R. replace (ff (w_ n x / u_ n x)) with (/u_ n x * (u_ n x * (ff (w_ n x / u_ n x)))) by (field; apply Rgt_not_eq; exact u_pos). rewrite <- q1_2_4; try assumption. rewrite <- Rmult_assoc, (Rmult_comm (2 ^ n)), Rmult_assoc. unfold Rdiv; rewrite Rmult_comm; apply f_equal. symmetry; apply q3_1_1'; assumption. apply Rlt_le, w_pos; assumption. assert (ctffx : continuity_pt Rinv (ff x)). apply derivable_continuous_pt; eapply exist; eapply derivable_pt_lim_inv. apply Rgt_not_eq, M_pos; psatzl R. apply CV_mult;[intros eps ep; exists 0%nat; intros; rewrite R_dist_eq; assumption | ]. apply continuity_seq;[assumption | apply M_def; psatzl R]. Qed. Lemma q3_1_3 : forall x, 0 < x < 1 -> Un_cv (fun n => w_ n x / u_ n x) 0. intros x intx. assert (0 < ff x) by (apply M_pos; psatzl R). replace 0 with (sqrt 0 / ff x) by (rewrite sqrt_0; field; lt0). apply CV_mult. unfold w_, pre_w_. apply continuity_seq. apply continuity_pt_sqrt; psatzl R. replace 0 with (ff x ^ 2 - ff x ^ 2) by ring. apply CV_plus. apply (continuity_seq (fun x => x ^ 2));[reg | apply M_def; psatzl R]. apply (continuity_seq (fun x => - x ^ 2));[reg | apply M_def'; psatzl R]. apply continuity_seq;[reg; lt0 | apply M_def; psatzl R]. Qed. Lemma q2_3_1' : forall x (x0 : 0 < x), I_t 1 x = 2 * RiemannInt (q2_3_1_ri x x0). intros x x0; unfold I_t. destruct (Rlt_dec 0 1) as [c10 | abs1];[ | psatzl R; psatzl R]. destruct (Rlt_dec 0 x) as [cx | absx];[ | psatzl R; psatzl R]. rewrite <- (upInt_break _ (sqrt x) 0 (q2_3_1_ui x x0) (q2_3_1_ri x x0)). rewrite q2_3_1; ring. Qed. (* General purpose section about arcsinh *) Definition arcsinh x := ln (x + sqrt (x ^ 2 + 1)). Lemma arcinh_l : forall x, arcsinh (sinh x) = x. intros x; unfold sinh, arcsinh. pattern 1 at 5; rewrite <- exp_0, <- (Rminus_eq0 x); unfold Rminus. rewrite exp_plus. match goal with |- context[sqrt ?a] => replace a with (((exp x + exp(-x))/2)^2) by field end. rewrite sqrt_pow2;[ | lt0]. match goal with |- context[ln ?a] => replace a with (exp x) by field end. rewrite ln_exp; reflexivity. Qed. Lemma sinh_arcsinh x : sinh (arcsinh x) = x. unfold sinh, arcsinh. assert (cmp : 0 < x + sqrt (x ^ 2 + 1)). destruct (Rle_dec x 0). replace (x ^ 2) with ((-x) ^ 2) by ring. assert (sqrt ((- x) ^ 2) < sqrt ((-x)^2+1)). apply sqrt_lt_1_alt. split;[apply pow2_ge_0 | psatzl R]. pattern x at 1; replace x with (- (sqrt ((- x) ^ 2))). assert (t:= sqrt_pos ((-x)^2)); psatzl R. rewrite sqrt_pow2; psatzl R. assert (0 < x) by psatzl R; lt0. rewrite exp_ln;[ | assumption]. rewrite exp_Ropp, exp_ln;[ | assumption]. apply Rminus_diag_uniq; unfold Rdiv; rewrite Rmult_minus_distr_r. assert (t: forall x y z, x - z = y -> x - y - z = 0);[ | apply t; clear t]. intros a b c H; rewrite <- H; ring. apply Rmult_eq_reg_l with (2 * (x + sqrt (x ^ 2 + 1)));[ | psatzl R]. field_simplify;[rewrite pow2_sqrt;[field | lt0] | lt0]. Qed. Lemma sinh_lt : forall x y, x < y -> sinh x < sinh y. intros x y xy; destruct (MVT_cor2 sinh cosh x y xy) as [c [Pc _]]. intros; apply derivable_pt_lim_sinh. apply Rplus_lt_reg_r with (Ropp (sinh x)); rewrite Rplus_opp_l, Rplus_comm. unfold Rminus at 1 in Pc; rewrite Pc; apply Rmult_lt_0_compat;[ | psatzl R]. unfold cosh; lt0. Qed. Lemma derivable_pt_lim_arcsinh : forall x, derivable_pt_lim arcsinh x (/sqrt (x ^ 2 + 1)). intros x; unfold arcsinh. assert (0 < x + sqrt (x ^ 2 + 1)). destruct (Rle_dec x 0);[ | assert (0 < x) by psatzl R; lt0]. replace (x ^ 2) with ((-x) ^ 2) by ring. assert (sqrt ((- x) ^ 2) < sqrt ((-x)^2+1)). apply sqrt_lt_1_alt. split;[apply pow2_ge_0 | psatzl R]. pattern x at 1; replace x with (- (sqrt ((- x) ^ 2))). assert (t:= sqrt_pos ((-x)^2)); psatzl R. rewrite sqrt_pow2; psatzl R. replace (/sqrt (x ^ 2 + 1)) with (/(x + sqrt (x ^ 2 + 1)) * (1 + (/(2 * sqrt (x ^ 2 + 1)) * (INR 2 * x ^ 1 + 0)))). apply (derivable_pt_lim_comp (fun x => x + sqrt (x ^ 2 + 1)) ln). apply (derivable_pt_lim_plus). apply derivable_pt_lim_id. apply (derivable_pt_lim_comp (fun x => x ^ 2 + 1) sqrt x). apply derivable_pt_lim_plus. apply derivable_pt_lim_pow. apply derivable_pt_lim_const. apply derivable_pt_lim_sqrt; lt0. apply derivable_pt_lim_ln; lt0. replace (INR 2 * x ^ 1 + 0) with (2 * x) by (simpl; ring). replace (1 + / (2 * sqrt (x ^ 2 + 1)) * (2 * x)) with (((sqrt (x ^ 2 + 1) + x))/sqrt (x ^ 2 + 1)) by (field; lt0). apply Rmult_eq_reg_l with (x + sqrt (x ^ 2 + 1));[ | lt0]. rewrite <- Rmult_assoc, Rinv_r;[field | ]; lt0. Qed. Lemma arcsinh_lt : forall x y, x < y -> arcsinh x < arcsinh y. intros x y xy. case (Rle_dec (arcsinh y) (arcsinh x));[ | psatzl R]. intros abs; case (Rlt_not_le _ _ xy). rewrite <- (sinh_arcsinh y), <- (sinh_arcsinh x). destruct abs as [lt | q];[ | rewrite q; psatzl R]. apply Rlt_le, sinh_lt; assumption. Qed. Lemma arcsinh_le : forall x y, x <= y -> arcsinh x <= arcsinh y. intros x y [xy | xqy]. apply Rlt_le, arcsinh_lt; assumption. rewrite xqy; apply Rle_refl. Qed. Lemma arcsinh_0 : arcsinh 0 = 0. unfold arcsinh; rewrite pow_ne_zero, !Rplus_0_l, sqrt_1, ln_1; [reflexivity |omega]. Qed. (* End of general purpose section about arcsinh *) Lemma q2_3_3 : (* Keeping multiplication by 2 out of the integral. *) forall x, 0 < x -> forall h : Riemann_integrable (fun y => /sqrt (y ^ 2 + x ^ 2)) 0 (sqrt x), RiemannInt h = arcsinh (/sqrt x). intros x x0 h. assert (s0 : 0 < sqrt x) by lt0. assert (heq : forall y, /sqrt (y ^ 2 + x ^ 2) = /x * /sqrt ((y / x) ^ 2 + 1)). intros; replace (y ^ 2 + x ^ 2) with (x ^ 2 * ((y / x) ^ 2 + 1)) by (field; lt0). rewrite sqrt_mult;[ | lt0 | lt0]. rewrite sqrt_pow2;[field;split; lt0 | psatzl R]. assert (ri1 : Riemann_integrable (fun y => / x * / sqrt ((y / x) ^ 2 + 1)) 0 (sqrt x)). apply RiemannInt_P6;[assumption | intros; reg; lt0]. rewrite (RiemannInt_ext _ _ _ _ h ri1); [ | intros; apply heq]. assert (s0' : 0/x < sqrt x/x) by (apply Rmult_lt_compat_r; lt0). assert (rim : Riemann_integrable (fun x => /sqrt (x ^ 2 + 1)) (0/x) (sqrt x / x)). apply RiemannInt_P6;[assumption |intros; reg; lt0]. assert (ric : Riemann_integrable (fun y => / x * /sqrt ((y / x) ^ 2 + 1)) 0 (sqrt x)). apply RiemannInt_P6;[lt0 |intros; reg; lt0 ]. assert (deras : forall y, 0 <= y <= sqrt x -> derivable_pt_lim (fun y => y/x) y (/x)). intros; rewrite <- (Rmult_1_l (/x)); unfold Rdiv; apply (derivable_pt_lim_scal_right (fun y => y)). apply derivable_pt_lim_id. assert (inb : forall y, 0 <= y <= sqrt x -> Rmin (0/x) ((sqrt x)/x) <= y/x <= Rmax (0/x) ((sqrt x)/x)). intros y inty; rewrite Rmin_left, Rmax_right; try psatzl R. split; apply Rmult_le_compat_r;lt0. assert (ct : forall y, Rmin (0 / x) (sqrt x / x) <= y <= Rmax (0 / x) (sqrt x / x) -> continuity_pt (fun y => /sqrt (y ^ 2 + 1)) y) by (intros; reg; lt0). assert (ctder : forall y : R, 0 <= y <= sqrt x -> continuity_pt (fun y : R => / x) y). solve[intros;reg]. rewrite <- (RiemannInt_ext _ _ _ _ ric), (RiemannInt_variable_change1 (fun y => /sqrt (y ^ 2 + 1)) (fun y => y / x) (fun y => / x) _ _ (Rlt_le _ _ s0) ric rim deras inb ct ctder); auto. assert (invs : sqrt x / x = / sqrt x) by (pattern x at 2; rewrite <- pow2_sqrt;[field | ];lt0). replace (arcsinh (/sqrt x)) with (arcsinh (sqrt x /x) - arcsinh (0 / x)) by (unfold Rdiv at 2; rewrite Rmult_0_l, arcsinh_0, invs; ring). apply (fun h h' h'' => antiderivative_Riemann _ arcsinh (0 / x) (sqrt x / x) h h' h'' rim); intros; try reg; try lt0; auto. split;[ | lt0]. intros y _; exists (exist _ (/sqrt (y ^ 2 + 1)) (derivable_pt_lim_arcsinh y)). reflexivity. Qed. Lemma q2_3_2 : forall eps, 0 < eps -> exists delta, 0 < delta /\ forall x (x0 : 0 < x), x < delta -> R_dist (RiemannInt (q2_3_1_ri x x0)/arcsinh(/sqrt x)) 1 < eps. intros eps ep. assert (ctinv : continuity_pt (fun x => /sqrt(x ^ 2 + 1)) 0) by (reg; lt0). destruct (ctinv _ ep) as [delta1 [dp1 Pd1]]. assert (dp : 0 < Rmin delta1 (Rmin ((delta1 / 2) ^ 2) 1) / 2) by lt0. exists (Rmin delta1 (Rmin ((delta1 / 2) ^ 2) 1) / 2);split;[assumption | ]. intros x x0 xd. assert (s0 : 0 <= sqrt x) by lt0. assert (ris : Riemann_integrable (fun t => /sqrt (t ^ 2 + x ^ 2)) 0 (sqrt x)). apply continuity_implies_RiemannInt;[lt0 | intros; reg; lt0]. assert (vris := q2_3_3 x x0 ris). assert (cmp : forall y : R, 0 < y < sqrt x -> (fun t : R => / sqrt ((t ^ 2 + 1 ^ 2) * (t ^ 2 + x ^ 2))) y <= (fun t : R => / sqrt (t ^ 2 + x ^ 2)) y). intros y inty; apply Rle_Rinv;[lt0 | lt0 | ]. apply sqrt_le_1_alt; assert (tmp := pow2_ge_0 y); rewrite pow1. assert (t : forall a b, 0 <= a -> 0 <= b -> b <= (a + 1) * b); [ | apply t; auto; try lt0; clear t]. intros a b a0 b0; pattern b at 1; rewrite <- Rmult_1_l. apply Rmult_le_compat_r; psatzl R. assert (rib : Riemann_integrable (fun t => /sqrt (((delta1/2)^2 + 1) * (t ^ 2 + x ^ 2))) 0 (sqrt x)). apply continuity_implies_RiemannInt;[lt0 | intros; reg; lt0]. assert (cmp' : forall y : R, 0 < y < sqrt x -> (fun t : R => / sqrt (((delta1/2) ^ 2 + 1) * (t ^ 2 + x ^ 2))) y <= (fun t : R => / sqrt ((t ^ 2 + 1 ^ 2) * (t ^ 2 + x ^ 2))) y). intros y inty; apply Rle_Rinv;[lt0 | lt0 | ]. apply sqrt_le_1_alt, Rmult_le_compat_r;[lt0 | ]. rewrite pow1; apply Rplus_le_compat_r, pow_incr; split; [lt0 | ]. apply Rle_trans with (1 := Rlt_le _ _ (proj2 inty)). rewrite <- (sqrt_pow2 (delta1/2));[ | lt0]. apply sqrt_le_1_alt, Rlt_le, Rlt_trans with (1 := xd). apply Rlt_le_trans with (Rmin delta1 (Rmin ((delta1 / 2) ^ 2) 1));[psatzl R|]. solve[rewrite Rmin_comm, <- Rmin_assoc; apply Rmin_l]. assert (scal : RiemannInt rib = /sqrt ((delta1/2) ^ 2 + 1) * RiemannInt ris). assert (rib' : Riemann_integrable (fun t => /sqrt ((delta1 / 2) ^ 2 + 1) * /sqrt (t ^ 2 + x ^ 2)) 0 (sqrt x)). apply continuity_implies_RiemannInt;[lt0 | intros; reg; lt0]. rewrite (RiemannInt_ext _ _ _ _ rib rib');[apply RiemannInt_scal | ]. intros; rewrite sqrt_mult, Rinv_mult_distr; lt0. unfold R_dist; rewrite <- Rabs_Ropp, Ropp_minus_distr'. assert (0 < arcsinh (/sqrt x)) by (rewrite <- arcsinh_0; apply arcsinh_lt; lt0). rewrite <- vris, Rabs_pos_eq. apply Rle_lt_trans with (1 - RiemannInt rib/RiemannInt ris). apply Rplus_le_compat_l, Ropp_le_contravar, Rmult_le_compat_r;[lt0 | ]. apply (RiemannInt_P19); lt0. (* An example of bad design of rewrite, to be used in discussion with F. Brehard *) unfold Rdiv at 1; rewrite scal, Rmult_assoc, Rinv_r, Rmult_1_r;[ | lt0]. pattern 1 at 1; replace 1 with (/sqrt (0 ^ 2 + 1)) by (rewrite pow_i, Rplus_0_l, sqrt_1, Rinv_1;[auto | omega]). assert (/sqrt ((delta1 / 2) ^ 2 + 1) <= /sqrt (0 ^ 2 + 1)). apply Rle_Rinv;[lt0 | lt0 | apply sqrt_le_1_alt, Rplus_le_compat_r, pow_incr]. psatzl R. rewrite <- (Rabs_pos_eq (_ - _)), <- Rabs_Ropp, Ropp_minus_distr';[| psatzl R]. apply Pd1; split;[split;[unfold no_cond; auto | lt0] | ]. unfold D_x, no_cond. simpl; unfold R_dist; rewrite Rabs_pos_eq; psatzl R. apply Rmult_le_reg_r with (RiemannInt ris);[lt0 | ]; rewrite Rmult_0_l. unfold Rdiv at 1; rewrite Rmult_minus_distr_r, Rmult_1_l, Rmult_assoc. rewrite Rinv_l, Rmult_1_r;[ | lt0]. assert (t := RiemannInt_P19 (q2_3_1_ri x x0) ris s0 cmp); psatzl R. Qed. (* This statement only becomes simple to express when using Derive (to mention the continuity of derivatives) *) Lemma derivable_u_n_v_n : forall x n, 0 < x < 1 -> {h1 : derivable_pt (u_ n) x & {h2 : derivable_pt (v_ n) x | 0 <= derive_pt _ _ h1 /\ 0 < derive_pt _ _ h2 /\ ((1 <= n)%nat -> 0 < derive_pt _ _ h1)}}. intros x n intx; induction n. unfold u_, v_; simpl. exists (exist _ 0 (derivable_pt_lim_const 1 x)). exists (exist _ 1 (derivable_pt_lim_id x)). split;[simpl; apply Rle_refl | ]. split;[simpl; exact Rlt_0_1 | ]. intros abs; inversion abs. destruct (ag_positive n 1 x) as [pu pv];try psatzl R. destruct IHn as [du [dv [dup [dvp _]]]]. assert (dus : derivable_pt_lim (u_ (S n)) x ((derive_pt _ _ du + derive_pt _ _ dv)/2)). apply derivable_pt_lim_ext with (fun x => (u_ n x + v_ n x) / 2). intros y; rewrite u_step; reflexivity. apply derivable_pt_lim_scal_right; apply derivable_pt_lim_plus. destruct du; assumption. destruct dv; assumption. assert (dvs : derivable_pt_lim (v_ (S n)) x (/(2 * sqrt (u_ n x * v_ n x)) * (derive_pt _ _ du * v_ n x + u_ n x *derive_pt _ _ dv))). apply derivable_pt_lim_ext with (fun x => sqrt (u_ n x * v_ n x)). intros; rewrite v_step; reflexivity. apply (derivable_pt_lim_comp (fun x => u_ n x * v_ n x) sqrt). apply derivable_pt_lim_mult;[destruct du; assumption|destruct dv; assumption]. apply derivable_pt_lim_sqrt. apply Rmult_lt_0_compat;[exact pu | exact pv]. set (pdus := exist _ _ dus); set (pdvs := exist _ _ dvs). assert (dus_pos : 0 < derive_pt (u_ (S n)) x pdus). unfold pdus; simpl. apply Rmult_lt_0_compat;[ | lt0]. solve[apply Rplus_le_lt_0_compat;[apply dup | apply dvp]]. exists pdus; exists pdvs. split;[apply Rlt_le, dus_pos | split;[ | intros; apply dus_pos]]. unfold pdvs; simpl; apply Rmult_lt_0_compat;[lt0 | ]. apply Rplus_le_lt_0_compat. apply Rmult_le_pos;[assumption | apply Rlt_le; exact pv]. apply Rmult_lt_0_compat;[exact pu | assumption]. Qed. Lemma ct_derive : forall x n, 0 < x < 1 -> continuity_pt (Derive (u_ n)) x /\ continuity_pt (Derive (v_ n)) x. intros x n intx; induction n. split; intros eps ep; exists 1; split; try apply Rlt_0_1; intros; rewrite ?Derive_const, ?Derive_id, R_dist_eq; assumption. assert (Rmin x (1 - x) <= x) by apply Rmin_l. assert (Rmin x (1 - x) <= 1 - x) by apply Rmin_r. assert (0 < Rmin x (1 - x)) by (apply Rmin_glb_lt; psatzl R). split. (* bad case of need to rewrite under lambdas. *) apply (continuity_pt_eq (fun x => (Derive (u_ n) x + Derive (v_ n) x)/2) _ (Rmin x (1 - x))); auto. intros z intz'; apply Rabs_lt_between in intz'. assert (intz : 0 < z < 1) by psatzl R. destruct (derivable_u_n_v_n z n intz) as [du [dv [_ [dvp dup']]]]. rewrite (Derive_ext (u_ (S n)) (fun x => /2 * (u_ n x + v_ n x))). rewrite Derive_scal, Derive_plus; try field; apply ex_derive_equiv_1; assumption. solve[intros; rewrite u_step; field]. reg; tauto. apply (continuity_pt_eq (fun x => (/(2 * sqrt (u_ n x * v_ n x)) * (Derive (u_ n) x * v_ n x + u_ n x * Derive (v_ n) x))) _ (Rmin x (1 - x))); auto. intros z intz'; apply Rabs_lt_between in intz'. assert (intz : 0 < z < 1) by psatzl R. destruct (derivable_u_n_v_n z n intz) as [du [dv [_ [dvp dup']]]]. assert (uv_pos := conj (u_pos z n intz) (v_pos z n intz)). rewrite (Derive_ext (v_ (S n)) (fun x => sqrt (u_ n x * v_ n x)) _ (fun z => v_step z n)). rewrite (Derive_comp sqrt); [ | apply ex_derive_equiv_1; reg; lt0 | apply ex_derive_equiv_1; reg]. replace (Derive sqrt (u_ n z * v_ n z)) with (/(2 * sqrt (u_ n z * v_ n z))). solve [rewrite Derive_mult; auto; apply ex_derive_equiv_1; auto]. apply eq_sym, is_derive_unique, derivable_pt_lim_sqrt; lt0. assert (continuity_pt (u_ n) x /\ continuity_pt (v_ n) x). destruct (derivable_u_n_v_n x n intx) as [du [dv [_ [dvp dup']]]]. split; apply derivable_continuous_pt; assumption. assert (uv_pos := conj (u_pos x n intx) (v_pos x n intx)). reg;[tauto | tauto | tauto | tauto | lt0 | lt0]. Qed. Lemma derivable_w_n : forall x n, 0 < x < 1 -> derivable_pt_lim (w_ n) x (/ (2 * sqrt (u_ n x ^ 2 - v_ n x ^ 2)) * (INR 2 * u_ n x ^ 1 * Derive (u_ n) x - INR 2 * v_ n x ^ 1 * Derive (v_ n) x)). intros x n intx. destruct (derivable_u_n_v_n x n intx) as [u' [v' ww]]. apply (derivable_pt_lim_comp _ sqrt). apply derivable_pt_lim_minus. apply (derivable_pt_lim_comp (u_ n) (fun x => x ^ 2)). apply Derive_correct, ex_derive_equiv_1; assumption. apply derivable_pt_lim_pow. apply (derivable_pt_lim_comp (v_ n) (fun x => x ^ 2)). apply Derive_correct, ex_derive_equiv_1; assumption. apply derivable_pt_lim_pow. apply derivable_pt_lim_sqrt, pre_w_pos; assumption. Qed. Definition k_ n x := / (2 ^ n) * ln (u_ n x / w_ n x). Lemma derivable_pt_lim_k_n : forall x n, 0 < x < 1 -> derivable_pt_lim (k_ n) x (/(2 ^ n) * (/(u_ n x / w_ n x) * ((Derive (u_ n) x * w_ n x - Derive (w_ n) x * u_ n x) / (w_ n x) ^ 2))). intros x n intx. apply derivable_pt_lim_scal. apply (derivable_pt_lim_comp _ ln). rewrite <- Rsqr_pow2. apply derivable_pt_lim_div. destruct (derivable_u_n_v_n x n intx) as [exderu _ ]. apply Derive_correct, ex_derive_equiv_1; assumption. apply Derive_correct, ex_derive_equiv_1. eapply exist; eapply derivable_w_n; assumption. apply Rgt_not_eq, w_pos; assumption. apply derivable_pt_lim_ln. apply Rmult_lt_0_compat;[apply u_pos | apply Rinv_0_lt_compat, w_pos]; assumption. Qed. Lemma w_simpl : forall x n, 0 < x < 1 -> w_(n + 1) x = (u_ n x - v_ n x)/2. intros x n intx; replace (n + 1)%nat with (S n) by ring; unfold w_, pre_w_. generalize (u_pos x n intx) (v_pos x n intx) (pre_w_pos x n intx). unfold u_, v_; simpl ag; destruct (ag 1 x n) as [a' b']; unfold fst, snd. intros a'0 b'0 dif; rewrite <- !Rsqr_pow2 in dif. assert (t : forall A B, 0 < A - B -> B < A) by (intros; psatzl R); apply t , Rsqr_incrst_0 in dif; try lt0; clear t. rewrite pow2_sqrt;[ | lt0]. match goal with |- context [sqrt ?A] => replace A with (((a' - b')/2) ^ 2) by field end. rewrite sqrt_pow2; psatzl R. Qed. Lemma q3_2_2 : forall x n, 0 < x < 1 -> Derive (k_ n) x/v_ n x ^ 2 = Derive (k_ (S n)) x/v_ (S n) x ^ 2. intros x n intx. assert (t := derivable_pt_lim_k_n x n intx). rewrite (is_derive_unique (k_ n) x _ t); clear t. assert (t := derivable_w_n x n intx). rewrite (is_derive_unique (w_ n) x _ t); clear t. replace (INR 2) with 2 by (simpl; ring). assert (eqf : forall x, 0 < x < 1 -> / (2 ^ (S n)) * ln ((u_ n x + v_ n x)/(u_ n x - v_ n x)) = k_ (S n) x). intros y inty; unfold k_; symmetry. rewrite u_step. replace (S n) with (n + 1)%nat by ring; rewrite w_simpl;[ | assumption]. repeat apply f_equal; field. intros abs; assert (abs' := pre_w_pos y n inty); case (Rlt_not_eq _ _ abs'). apply Rminus_diag_uniq in abs; rewrite abs; psatzl R. assert (derf : derivable_pt_lim (fun x => /(2 ^ S n) * ln ((u_ n x + v_ n x) / (u_ n x - v_ n x))) x (/(2 ^ S n) * (/((u_ n x + v_ n x)/(u_ n x - v_ n x)) * (((Derive (u_ n) x + Derive (v_ n) x) * (u_ n x - v_ n x) - (Derive (u_ n) x - Derive (v_ n) x) * (u_ n x + v_ n x))/ (u_ n x - v_ n x)^ 2)))). destruct (derivable_u_n_v_n x n intx) as [du [dv _]]. apply derivable_pt_lim_scal. apply (derivable_pt_lim_comp _ ln). rewrite <- Rsqr_pow2. apply (derivable_pt_lim_div (fun x => u_ n x + v_ n x) (fun x => u_ n x - v_ n x)). apply derivable_pt_lim_plus. apply Derive_correct, ex_derive_equiv_1; assumption. apply Derive_correct, ex_derive_equiv_1; assumption. apply derivable_pt_lim_minus. apply Derive_correct, ex_derive_equiv_1; assumption. apply Derive_correct, ex_derive_equiv_1; assumption. intros abs; assert (abs' := pre_w_pos x n intx); case (Rlt_not_eq _ _ abs'). apply Rminus_diag_uniq in abs; rewrite abs; psatzl R. apply derivable_pt_lim_ln. generalize (u_pos x n intx) (v_pos x n intx) (cmp_u_v x n intx); intros; lt0. replace (Derive (k_ (S n)) x) with (/(2 ^ S n) * (/((u_ n x + v_ n x)/(u_ n x - v_ n x)) * (((Derive (u_ n) x + Derive (v_ n) x) * (u_ n x - v_ n x) - (Derive (u_ n) x - Derive (v_ n) x) * (u_ n x + v_ n x))/ (u_ n x - v_ n x)^ 2))) by (symmetry; apply is_derive_unique, (derivable_pt_lim_eq _ _ _ _ _ _ intx eqf derf)). change (sqrt (u_ n x ^ 2 - v_ n x ^ 2)) with (w_ n x). assert (up := u_pos x n intx); assert (vp := v_pos x n intx). assert (pwp := pre_w_pos x n intx). rewrite v_step, pow2_sqrt;[ | lt0]. change (2 ^ S n) with (2 * 2 ^ n). apply Rminus_diag_uniq; field_simplify. replace (w_ n x ^ 2) with (u_ n x ^ 2 - v_ n x ^ 2). field_simplify; try (unfold Rdiv; rewrite !Rmult_0_l; reflexivity). rewrite <- !(Rmult_comm (u_ n x ^ 2 - v_ n x ^ 2)), !Rmult_assoc, <- !Rmult_minus_distr_l. apply Rgt_not_eq;repeat apply Rmult_lt_0_compat; try lt0. replace (u_ n x ^ 3 * v_ n x ^ 2 - u_ n x * v_ n x ^ 4) with ((u_ n x * v_ n x ^ 2) * (u_ n x ^ 2 - v_ n x ^ 2)) by ring; lt0. unfold w_, pre_w_; rewrite pow2_sqrt; [reflexivity | apply Rlt_le, pre_w_pos; assumption]. assert (t := cmp_u_v x n intx); assert (t' := w_pos x n intx). repeat split; lt0. Qed. Lemma q3_2_3 : forall x n, 0 < x < 1 -> Derive (k_ n) x = v_ n x ^ 2 / (x * (1 - x ^ 2)). intros x n intx; assert (0 < x * x < 1). split;[| replace 1 with (1 * 1) by ring; apply Rmult_le_0_lt_compat]; lt0. induction n. rewrite (is_derive_unique _ _ _ (derivable_pt_lim_k_n x 0 intx)). unfold w_, pre_w_, u_, v_, Rdiv; simpl. rewrite !Rmult_1_r, Rinv_1, !Rmult_1_l. replace (Derive (fun _ => 1) x) with 0 by (symmetry; apply is_derive_unique, derivable_pt_lim_const). replace (Derive (fun x0 => sqrt (1 - x0 * (x0 * 1))) x) with (/(2 * (sqrt (1 - x * (x * 1)))) * (0 - INR 2 * x ^ 1)). simpl; rewrite !Rmult_1_r; field_simplify; try psatzl R; try lt0. rewrite pow2_sqrt;[ | psatzl R]. field; simpl; rewrite Rmult_1_r; psatzl R. symmetry; apply is_derive_unique. apply (derivable_pt_lim_comp _ sqrt). apply derivable_pt_lim_minus. apply derivable_pt_lim_const. apply (derivable_pt_lim_pow x 2). apply derivable_pt_lim_sqrt; rewrite Rmult_1_r; psatzl R. replace (Derive (k_ (S n)) x) with ((Derive (k_ n) x / v_ n x ^ 2) * v_(S n) x ^ 2). rewrite IHn; field; assert (t' := v_pos x n intx); psatzl R. rewrite (q3_2_2 x n intx); field; apply Rgt_not_eq, v_pos; assumption. Qed. Lemma q1_3_2_v : forall n x, (1 <= n)%nat -> 0 <= x -> 0 <= ff x - v_ n x <= Rabs(1 - x)/2^n. intros n x n1 x0; unfold v_. assert (t' := Rlt_le _ _ Rlt_0_1). assert (tmp := ag_diff_maj 1 x n n1 t' x0). assert (t1 := CV_shift' _ 1 (ff x) (M_def 1 x t' x0)). assert (t := decreasing_ineq _ (ff x) (an_decreasing 1 x t' x0) t1 (n - 1)). assert (ff x <= fst (ag 1 x n)). apply Rle_trans with (1 := t). replace (n - 1 + 1)%nat with n by omega; apply Rle_refl. split;[ | psatzl R]. assert (t2 := CV_shift' _ 1 (ff x) (M_def' 1 x t' x0)). assert (t3 := growing_ineq _ (ff x) (bn_growing 1 x t' x0) t2 (n - 1)). assert (snd (ag 1 x n) <= ff x);[ | psatzl R]. apply Rle_trans with (2 := t3). replace (n - 1 + 1)%nat with n by omega; apply Rle_refl. Qed. Lemma cvu_v_ff : forall x (x0 : 0 < x), CVU v_ ff x (pos_div_2 (mkposreal x x0)). intros x x0. intros eps ep; destruct (cv_div2 (Rmax (Rabs (1 - 3/2 * x)) (Rabs (1 - x / 2))) eps ep) as [N Pn]. exists (N + 1)%nat; intros n y Nn dyx. assert (n1 : (1 <= n)%nat) by omega. unfold Boule in dyx; apply Rabs_lt_between in dyx; unfold pos_div_2, pos in dyx. assert (y0 : 0 <= y) by psatzl R. destruct (q1_3_2_v n y n1 y0) as [difpos difbound]. rewrite Rabs_pos_eq;[ | psatzl R]. apply Rle_lt_trans with (1 := proj2 (q1_3_2_v n y n1 y0)). assert (Nn' : (n >= N)%nat) by lia. assert (Pn' := Pn n Nn'); unfold R_dist in Pn'. apply Rabs_lt_between in Pn'; rewrite Rminus_0_r in Pn'. destruct Pn' as [_ Pn2]. apply Rlt_trans with (2 := Pn2), Rmult_lt_compat_r;[lt0 | ]. unfold Rmax; case (Rle_dec (Rabs (1 - 3/2 * x)) (Rabs (1 - x /2))); unfold Rabs; destruct (Rcase_abs (1 - 3/2 * x)); destruct (Rcase_abs (1 - x/2)); destruct (Rcase_abs (1 - y));try psatzl R. Qed. Lemma CVU_derive_k_n : forall lb ub, 0 < lb < ub -> ub < 1 -> forall c delta, (forall y, Boule c delta y -> lb < y < ub) -> CVU (fun n x => Derive (k_ n) x) (fun x => ff x ^ 2/(x * (1 - x ^ 2))) c delta. intros lb ub [ub0 ul] lb1 x delta Pb. assert (ctpoly : forall y, lb <= y <= ub -> continuity_pt (fun z => z * (1 - z ^ 2)) y) by (intros; reg). destruct (continuity_ab_min (fun x => x * (1 - x ^ 2)) lb ub (Rlt_le _ _ ul) ctpoly) as [bot [pbot inbounds]]; clear ctpoly. assert (0 < bot * (1 - bot ^ 2)). replace (1 - bot ^ 2) with ((1 + bot) * (1 - bot)) by ring; lt0. assert (bnd : forall y n, 0 < y < 1 -> u_ n y - v_ n y <= 1 / 2 ^ n). intros y [ | n] inty. unfold u_, v_; simpl; psatzl R. assert (tmp1 : (1 <= S n)%nat) by omega. assert (tmp2 : 0 <= y) by psatzl R. assert (tmp3 : 0 <= 1) by psatzl R. unfold u_, v_; destruct (ag_diff_maj 1 y (S n) tmp1 tmp3 tmp2) as [t1 t2]. apply Rle_trans with (1 := t2), Rmult_le_compat_r;[lt0 | ]. rewrite Rabs_pos_eq; psatzl R. intros eps ep. assert (dpos : 0 < eps * (bot * (1 - bot ^ 2))) by lt0. destruct (cv_div2 1 _ dpos) as [N Pn]; exists (N + 1)%nat; intros n y nN dyx. assert (nN' : (n >= N)%nat) by lia. apply Pb in dyx. (* bug: why do I have to clear the context here? *) assert (inty : 0 < y < 1) by (clear -dyx ub0 ul lb1; psatzl R). rewrite q3_2_3;[ | psatzl R]. assert (t : forall a b c, a/c - b/c = (a-b)/c) by (intros; unfold Rdiv; ring). rewrite t, Rabs_pos_eq; clear t. apply Rle_lt_trans with ((ff y ^ 2 - v_ n y ^ 2)/(bot *(1- bot^ 2))). apply Rmult_le_compat_l. destruct (q1_3_2_v n y); try psatzl R; try lia. assert (vp := v_pos y n inty). assert (v_ n y ^ 2 <= ff y ^ 2);[ | psatzl R]. rewrite <- !Rsqr_pow2; apply Rsqr_incr_1; psatzl R. assert (bot * (1 - bot ^ 2) <= y * (1 - y ^ 2)). apply pbot; psatzl R. apply Rle_Rinv; psatzl R. destruct (q1_3_2_v n y) as [c1 c2]; try psatzl R; try lia. apply Rmult_lt_reg_r with (bot * (1 - bot ^ 2));[lt0 | ]. unfold Rdiv; rewrite Rmult_assoc, Rinv_l, Rmult_1_r;[|lt0]. replace (ff y ^ 2 - v_ n y ^ 2) with ((ff y + v_ n y) * (ff y - v_ n y)) by ring. destruct n as [ | n];[elimtype False; clear -nN; omega | ]. assert (nN2 : (n >= N)%nat) by omega. assert (Pn' := Pn n nN2); unfold R_dist in Pn'; rewrite Rminus_0_r in Pn'. rewrite Rabs_pos_eq in Pn';[ | lt0]. apply Rle_lt_trans with (2 * (ff y - v_ (S n) y)). apply Rmult_le_compat_r;[psatzl R | ]. assert (ff y <= 1). assert (y0 : 0 <= y) by psatzl R. assert (t := q1_3_2 1 y (le_n _) y0). rewrite Rabs_pos_eq in t;[ | psatzl R]. unfold u_ in t; simpl in t; rewrite Rmult_1_r in t; psatzl R. psatzl R. replace (eps * (bot * (1 - bot ^ 2))) with (2 * ((eps * (bot * (1 - bot ^ 2)))/2)) by field. apply Rmult_lt_compat_l;[lt0 | ]. apply Rle_lt_trans with (1 := c2). replace (Rabs (1 - y) / 2 ^ S n) with ((Rabs (1 - y)/2 ^n) / 2) by (simpl; field; lt0). apply Rmult_lt_compat_r;[lt0 | ]. apply Rle_lt_trans with (2 := Pn'), Rmult_le_compat_r;[lt0 |]. rewrite Rabs_pos_eq; psatzl R. apply Rmult_le_pos. destruct (q1_3_2_v n y) as [c1 c2]; try psatzl R; try lia. replace (ff y ^ 2 - v_ n y ^ 2) with ((ff y + v_ n y) * (ff y - v_ n y)) by ring. assert (vp := v_pos y n inty). apply Rmult_le_pos; psatzl R. assert (bot * (1 - bot ^ 2) <= y * (1 - y ^ 2)) by (apply pbot; psatzl R); lt0. Qed. Lemma equiv_ln_arcsinh : forall f, (forall n, 0 < f n) -> Un_cv f 0 -> Un_cv (fun n => ln (/f n)/arcsinh (/f n)) 1. intros f fp cvf. assert (ctv : continuity_pt Rinv 1) by (reg; lt0). intros eps ep. destruct (ctv eps ep) as [eps' [ep' Pe']]. destruct (cvf 1 Rlt_0_1) as [N1 Pn1]. destruct (cvf (exp (-(ln 3/eps'))) (exp_pos _)) as [N2 Pn2]. exists (N1 + N2)%nat; intros n nN. assert (nN1 : (N1 <= n)%nat) by lia. assert (nN2 : (N2 <= n)%nat) by lia. assert (0 < f n) by auto. assert (1 < / f n). generalize (Pn1 n nN1); unfold R_dist; rewrite Rminus_0_r. intros cf; apply Rabs_lt_between in cf. rewrite <- Rinv_1; apply Rinv_lt_contravar;[lt0 | tauto]. assert (0 < ln (/ f n)) by (rewrite <- ln_1; apply ln_increasing; lt0). assert (0 < arcsinh (/ f n)). rewrite <- arcsinh_0; apply arcsinh_lt; psatzl R. assert (1 < (/ f n) ^ 2). simpl; rewrite Rmult_1_r, <- (Rmult_1_r 1). apply Rmult_le_0_lt_compat; lt0. assert (0 < sqrt ((/ f n) ^ 2 + 1)) by lt0. assert (/f n < /f n + sqrt ((/f n)^2 + 1)) by psatzl R. assert (sqrt ((/f n) ^ 2 + 1) < sqrt (2 ^ 2 * (/ f n) ^ 2)). apply sqrt_lt_1_alt; psatzl R. assert (/f n + sqrt ((/f n) ^ 2 + 1) < 3 * / f n). replace (3 * / f n) with (/ f n + 2 * / f n) by ring. apply Rplus_lt_compat_l. rewrite <- (sqrt_pow2 2);[ | lt0]. pattern (/ f n) at 2; rewrite <- (sqrt_pow2 (/ f n)); try lt0. rewrite <- sqrt_mult; lt0. replace (ln (/ f n) / arcsinh (/ f n)) with (/( (arcsinh (/ f n))/ln (/f n))) by (field;split; lt0). rewrite <- Rinv_1. destruct (Req_EM_T ((arcsinh (/ f n) / ln (/ f n))) 1) as [q | nq]. rewrite q, R_dist_eq; assumption. apply Pe';split;[unfold D_x, no_cond; auto | ]. simpl; unfold R_dist, arcsinh, Rdiv; rewrite Rabs_pos_eq. apply Rlt_trans with (ln (3 * / f n)/ln(/f n) - 1). apply Rplus_lt_compat_r; apply Rmult_lt_compat_r;[lt0 | ]. apply ln_increasing. rewrite Rplus_comm; lt0. assumption. unfold Rdiv, Rminus; rewrite ln_mult, Rmult_plus_distr_r, Rinv_r; try lt0. rewrite Rplus_assoc, Rplus_opp_r, Rplus_0_r. apply Rmult_lt_reg_r with (/eps' * ln (/ f n));[lt0 | ]. rewrite <- (Rmult_assoc eps'), Rinv_r, Rmult_1_l;[ | lt0]. rewrite Rmult_assoc, (Rmult_comm (/ ln (/ f n))), Rmult_assoc. rewrite Rinv_r, Rmult_1_r;[ | lt0]. rewrite ln_Rinv, <- (Ropp_involutive (_ * _));[ | lt0]; apply Ropp_lt_contravar. rewrite <- (ln_exp (- _)); apply ln_increasing; try lt0. generalize (Pn2 _ nN2); unfold R_dist; rewrite Rminus_0_r; intros main. apply Rabs_lt_between in main. tauto. assert (1 <= ln (/ f n + sqrt ((/ f n) ^ 2 + 1)) * / ln (/ f n));[ | psatzl R]. apply Rmult_le_reg_r with (ln (/ f n));[lt0 | ]. unfold Rdiv; rewrite Rmult_1_l, Rmult_assoc, Rinv_l, Rmult_1_r;[ | lt0]. apply ln_le;[lt0 | lt0]. Qed. Lemma q2_3_ri_pos : forall b (b0 : 0 < b), 0 < RiemannInt (q2_3_1_ri b b0). intros b b0. apply Rlt_le_trans with (/sqrt ((b + 1) * (b + b ^ 2)) * (sqrt b - 0)). rewrite Rminus_0_r; lt0. rewrite <- (RiemannInt_P15 (RiemannInt_P14 0 (sqrt b) _)). apply RiemannInt_P19; [lt0 | ]. intros x intx; unfold fct_cte; apply Rle_Rinv;[lt0 | lt0 | ]. apply sqrt_le_1_alt. assert (x ^ 2 <= b). rewrite <- (pow2_sqrt b);[ | lt0]. simpl; rewrite Rmult_1_r; apply Rmult_le_compat; lt0. apply Rmult_le_compat; lt0. Qed. Lemma q2_3_4 : forall f, (forall n, 0 < f n) -> Un_cv f 0 -> Un_cv (fun n => ff (f n) * (/(PI/2) * -ln (f n))) 1. intros f fp cvf. apply (Un_cv_ext (fun n => (/((RiemannInt (q2_3_1_ri (f n) (fp n))) / arcsinh (/sqrt (f n))) * (ln (/sqrt (f n)) / arcsinh (/sqrt (f n)))))). intros n; unfold ff. assert (fnp : 0 < f n) by auto. replace (M 1 (f n)) with ((PI/2) * / I_t 1 (f n)) by (rewrite (q2_2_2 1 (f n) Rlt_0_1 (fp n)); field; split; [apply Rgt_not_eq, M_pos; auto; psatzl R | lt0]). rewrite (Rmult_comm (/(PI/2))), !Rmult_assoc, (Rmult_comm (PI/2)). rewrite (q2_3_1' _ (fp n)). assert (t := q2_3_ri_pos _ (fp n)). assert (0 < arcsinh (/sqrt (f n))) by (rewrite <- arcsinh_0; apply arcsinh_lt; lt0). replace (ln (/sqrt (f n))) with (-ln (f n)/2); [field; repeat split; lt0 | ]. rewrite <- (Ropp_involutive (ln (f _))). pattern (f n) at 1; rewrite <- pow2_sqrt;[ | lt0]. rewrite ln_pow;[ | lt0]. rewrite <- Ropp_mult_distr_r_reverse, ln_Rinv;[ | lt0]; simpl; field. replace 1 with (1 * 1) by ring. assert (sfp : forall n, 0 < sqrt (f n)) by (intros; apply sqrt_lt_R0, fp). assert (cvsf : Un_cv (fun n => sqrt (f n)) 0). rewrite <- sqrt_0; apply continuity_seq;[reg; lt0 | assumption]. apply CV_mult;[ | apply (equiv_ln_arcsinh (fun n => sqrt (f n))); solve[auto]]. rewrite <- Rinv_1; apply continuity_seq;[ reg; lt0 | ]. intros eps ep; destruct (q2_3_2 eps ep) as [delta [dp Pd]]. destruct (cvf delta dp) as [N Pn]; exists N; intros n nN; apply Pd. replace (f n) with (R_dist (f n) 0); [apply Pn; assumption | ]. unfold R_dist; rewrite Rminus_0_r; apply Rabs_pos_eq, Rlt_le; exact (fp n). Qed. Lemma q3_1_3_cor : forall x, 0 < x < 1 -> Un_cv (fun n => k_ n x) ((PI/2) * ff x / ff (sqrt (1 - x ^ 2))). intros x intx. assert (cv0 := q3_1_3 x intx). assert (fp : forall n, (0 < w_ n x / u_ n x)). intros n; apply Rmult_lt_0_compat;[ | apply Rinv_0_lt_compat]. apply w_pos; lt0. apply u_pos; lt0. apply Un_cv_ext with (fun n => (ff (w_ n x / u_ n x) * ((/(PI/2)) * -ln (w_ n x / u_ n x))) * (/(ff (w_ n x / u_ n x) * ((/(PI/2)) * -ln (w_ n x / u_ n x))) * k_ n x)). intros n; field. assert (wp : 0 < w_ n x) by (apply w_pos; psatzl R). assert (up : 0 < u_ n x) by (apply u_pos; psatzl R). assert (ln (w_ n x / u_ n x) <> 0). apply Rlt_not_eq; rewrite <- ln_1; apply ln_increasing;[lt0 | ]. apply (Rmult_lt_reg_r (u_ n x));[lt0 | ]; rewrite Rmult_1_l. unfold Rdiv; rewrite Rmult_assoc, Rinv_l, Rmult_1_r;[ | lt0]. assert (pw := pre_w_pos x n intx). change (w_ n x) with (sqrt (u_ n x ^ 2 - v_ n x ^ 2)). pattern (u_ n x) at 2; rewrite <- (sqrt_pow2 (u_ n x));[ | lt0]. apply sqrt_lt_1_alt; split;[lt0 | ]. assert (vp : 0 < v_ n x ^ 2) by (apply pow_lt, v_pos; lt0); psatzl R. assert (0 < ff (w_ n x / u_ n x)) by (unfold ff; apply M_pos; lt0). repeat split; auto; lt0. rewrite <- (Rmult_1_l (_ * _ / _)). apply CV_mult. apply (q2_3_4 (fun n => w_ n x / u_ n x)); assumption. apply Un_cv_ext with (fun n => (PI / 2) * /(2 ^ n * ff (w_ n x / u_ n x))). intros n; unfold k_. assert (wp : 0 < w_ n x) by (apply w_pos; psatzl R). assert (up : 0 < u_ n x) by (apply u_pos; psatzl R). replace (ln (u_ n x / w_ n x)) with (-(ln (w_ n x / u_ n x))) by (rewrite <- ln_Rinv;[ apply f_equal; field| ]; lt0). field. assert (ln (w_ n x / u_ n x) <> 0). apply Rlt_not_eq; rewrite <- ln_1; apply ln_increasing;[lt0 | ]. apply (Rmult_lt_reg_r (u_ n x));[lt0 | ]; rewrite Rmult_1_l. unfold Rdiv; rewrite Rmult_assoc, Rinv_l, Rmult_1_r;[ | lt0]. assert (pw := pre_w_pos x n intx). change (w_ n x) with (sqrt (u_ n x ^ 2 - v_ n x ^ 2)). pattern (u_ n x) at 2; rewrite <- (sqrt_pow2 (u_ n x));[ | lt0]. apply sqrt_lt_1_alt; split;[lt0 | ]. assert (vp : 0 < v_ n x ^ 2) by (apply pow_lt, v_pos; lt0); psatzl R. assert (0 < ff (w_ n x / u_ n x)) by (unfold ff; apply M_pos; lt0). repeat split; auto; lt0. unfold Rdiv at 3; rewrite Rmult_assoc; apply CV_mult. intros eps ep; exists 0%nat; intros; rewrite R_dist_eq; assumption. assert (0 < 1 - x ^ 2) by (replace (1 - x ^ 2) with ((1 + x) * (1 - x)) by ring;lt0). replace (ff x * / ff (sqrt (1 - x ^ 2))) with (/ (ff (sqrt (1 - x ^ 2)) / ff x)). apply continuity_seq. reg; apply Rgt_not_eq;apply Rmult_lt_0_compat; [|apply Rinv_0_lt_compat];apply M_pos; lt0. apply q3_1_2; assumption. field. split; apply Rgt_not_eq, M_pos; try lt0. Qed. Lemma q3_3_1 : forall x, 0 < x < 1 -> derivable_pt_lim (fun x => (PI/2) * ff x / ff (sqrt (1 - x ^ 2))) x (ff x ^ 2/(x * (1 - x ^ 2))). intros x intx. assert (d0 : 0 < Rmin (x / 2) ((1 - x) / 2)) by (apply Rmin_glb_lt; lt0). set (delta := mkposreal _ d0). assert (delta <= (x / 2)) by apply Rmin_l. assert (delta <= (1 - x) / 2) by apply Rmin_r. assert (dern : forall y n, Boule x delta y -> is_derive (k_ n) y (Derive (k_ n) y)). intros y n dyx; unfold Boule in dyx; apply Rabs_lt_between in dyx. apply Derive_correct, ex_derive_equiv_1. eapply exist, derivable_pt_lim_k_n; psatzl R. assert (cv_k_n : forall y : R, Boule x delta y -> Un_cv (fun n : nat => k_ n y) ((fun x : R => PI / 2 * ff x / ff (sqrt (1 - x ^ 2))) y)). intros y dyx; unfold Boule in dyx; apply Rabs_lt_between in dyx. apply q3_1_3_cor; psatzl R. assert (cvu_dk_n : CVU (fun n x => Derive (k_ n) x) (fun x => ff x ^ 2 / (x * (1 - x ^ 2))) x delta). apply (CVU_derive_k_n (x - delta) (x + delta)); [assert (tmp := cond_pos delta); psatzl R | psatzl R | ]. intros y dyx; unfold Boule in dyx; apply Rabs_lt_between in dyx; psatzl R. assert (ctf :forall y : R, Boule x delta y -> continuity_pt (fun x : R => ff x ^ 2 / (x * (1 - x ^ 2))) y). intros y dyx; unfold Boule in dyx; apply Rabs_lt_between in dyx. reg. apply q1_3_3; psatzl R. replace (1 - y ^ 2) with ((1 + y) * (1 - y)) by ring; lt0. apply (derivable_pt_lim_CVU k_ (fun n x => Derive (k_ n) x) (fun x => (PI/2) * ff x / ff (sqrt (1 - x ^ 2))) (fun x => ff x ^ 2 / (x * (1 - x ^ 2))) x x delta (Boule_center _ _) dern cv_k_n cvu_dk_n ctf). Qed. Lemma q3_3_2 : PI = 2 * sqrt 2 * ff (/sqrt 2)^3/Derive ff (/sqrt 2). assert (ints2 : 0 < /sqrt 2 < 1). split;[lt0 | ]. pattern 1 at 3; replace 1 with (/sqrt 1) by (rewrite sqrt_1, Rinv_1;reflexivity). apply Rinv_lt_contravar;[lt0 | apply sqrt_lt_1_alt; psatzl R]. assert (t := q3_3_1 (/sqrt 2) ints2). assert (t' : forall x, 0 < x < 1 -> is_derive (fun x => PI/2 * ff x / ff (sqrt (1 - x ^ 2))) x (PI/2 * ((Derive ff x * ff (sqrt (1 - x ^ 2)) - (Derive ff (sqrt (1 - x ^ 2)) * (/(2 * sqrt (1 - x ^ 2)) * (0 - INR 2 * x ^ 1))) * ff x)/ ff (sqrt (1 - x ^ 2)) ^ 2))). intros x intx. assert (0 < 1 - x ^ 2) by (replace (1 - x ^ 2) with ((1 + x) * (1 - x)) by ring; lt0). assert (1 - x ^ 2 < 1) by (assert (t' := pow_lt x 2 (proj1 intx)); psatzl R). apply (derivable_pt_lim_ext (fun x => PI/2 * (ff x /ff(sqrt(1-x^2))))); [intros y; unfold Rdiv; ring | ]. apply derivable_pt_lim_scal. rewrite <- (Rsqr_pow2 (ff _)). apply (derivable_pt_lim_div ff (fun x => ff (sqrt (1 - x ^ 2))) x). apply Derive_correct, ex_derive_ff; assumption. apply (derivable_pt_lim_comp _ ff). apply (derivable_pt_lim_comp _ sqrt). apply derivable_pt_lim_minus. apply derivable_pt_lim_const. apply derivable_pt_lim_pow. apply derivable_pt_lim_sqrt; assumption. apply Derive_correct, ex_derive_ff; split;[lt0 | ]. pattern 1 at 2; rewrite <- sqrt_1; apply sqrt_lt_1_alt; split;lt0. unfold ff; apply Rgt_not_eq, M_pos; lt0. generalize (uniqueness_limite _ _ _ _ t (t' _ ints2)). assert (0 < Derive ff (/sqrt 2)). apply derive_ff_pos. split; [lt0 | ]. pattern 1 at 3; replace 1 with (/sqrt 1) by (rewrite sqrt_1, Rinv_1; auto). apply Rinv_lt_contravar, sqrt_lt_1_alt; lt0. replace ((/sqrt 2) ^ 2) with (/2) by (rewrite <- Rinv_pow, pow2_sqrt; lt0). replace (1 - /2) with (/2) by field; simpl INR. replace (sqrt (/2)) with (/sqrt 2) by (symmetry; apply sqrt_lem_1; try lt0; rewrite <- Rinv_mult_distr, sqrt_sqrt; try lt0). replace ((/sqrt 2) ^ 1) with (/sqrt 2) by ring. assert (0 < ff (/sqrt 2)) by (unfold ff; apply M_pos; lt0). assert (0 < Derive ff (/sqrt 2)). apply derive_ff_pos;split;[lt0 | ]. pattern 1 at 3; replace 1 with (/sqrt 1) by (rewrite sqrt_1, Rinv_1; auto). apply Rinv_lt_contravar, sqrt_lt_1_alt; lt0. intros tmp; apply f_equal with (f := fun x => x * (2 / ((Derive ff (/ sqrt 2) * ff (/ sqrt 2) - Derive ff (/ sqrt 2) * (/ (2 * / sqrt 2) * (0 - 2 * (/ sqrt 2) ^ 1)) * ff (/ sqrt 2)) / ff (/ sqrt 2) ^ 2))) in tmp. match goal with id : _ * _ = ?b * ?c |- _ => assert (tmp2 : PI = b * c) end. assert (0 < ff (/sqrt 2)) by (unfold ff; apply M_pos; lt0). field; repeat split; try lt0. match goal with |- ?a <> 0 => replace a with (4 * (Derive ff (/sqrt 2) * ff (/sqrt 2))) by ring; lt0 end. rewrite <- tmp2 in tmp; rewrite <- tmp; clear tmp tmp2. field; repeat split; try lt0. match goal with |- ?a <> 0 => replace a with (4 * (Derive ff (/sqrt 2) * ff (/sqrt 2))) by ring; lt0 end. Qed. Definition y_ n x := u_ n x / v_ n x. Lemma y_0 : y_ 0 (1/sqrt 2) = sqrt 2. Proof. unfold y_, u_, v_; simpl. field. lt0. Qed. Definition z_ n x := Derive (v_ n) x / Derive (u_ n) x. Lemma q4_1_1 : forall x n, 0 < x < 1 -> 1 < y_ n x. intros x n intx. unfold y_; replace (u_ n x) with (v_ n x + (u_ n x - v_ n x)) by ring. unfold Rdiv; rewrite Rmult_plus_distr_r. assert (up := u_pos x n intx). assert (vp := v_pos x n intx). assert (cmp_u_v := cmp_u_v x n intx). rewrite Rinv_r;[ | assert (t := v_pos x n intx);psatzl R]. pattern 1 at 1; replace 1 with (1 + 0) by ring; apply Rplus_lt_compat_l. lt0. Qed. Lemma q4_1_1' : forall lb ub, 0 < lb < ub -> ub < 1 -> forall c (delta : posreal), lb < c - delta -> c + delta < ub -> CVU y_ (fun _ => 1) c delta. intros lb ub [lb0 lu] u1 c delta lcd cdu. assert (dps : 0 < (ub - lb)/2) by psatzl R. assert (lu' : lb <= ub) by psatzl R. intros eps ep. assert (deltap : 0 < eps * lb) by lt0. destruct (cv_div2 1 _ deltap) as [N Pn]. exists (N + 1)%nat. unfold Boule; intros n y nN inty'. apply Rabs_lt_between in inty'; simpl in inty'. assert (nN' : (N <= n)%nat) by lia. simpl in inty'; assert (inty : 0 < y < 1) by psatzl R. destruct (ag_diff_maj 1 y n) as [dp db];[lia | psatzl R |psatzl R | ]. rewrite <- Rabs_Ropp, Ropp_minus_distr', Rabs_pos_eq. unfold y_. assert (y0 : 0 < y) by psatzl R. assert (v_n0 : 0 < v_ n y) by (apply v_pos; psatzl R). apply Rmult_lt_reg_r with (v_ n y); [lt0 | rewrite Rmult_minus_distr_r, Rmult_1_l]. unfold Rdiv; rewrite Rmult_assoc, Rinv_l, Rmult_1_r;[ | lt0]. apply Rlt_trans with (eps * lb). apply Rle_lt_trans with (1 := db). apply Rlt_trans with (1 / 2 ^ n). apply Rmult_lt_compat_r;[| rewrite Rabs_pos_eq]; lt0. generalize (Pn n nN'); unfold R_dist; rewrite Rminus_0_r, Rabs_pos_eq;[|lt0]. tauto. apply Rmult_lt_compat_l;[lt0 | ]. apply Rlt_le_trans with y;[psatzl R | ]. apply Rle_trans with (sqrt (1 * y)). rewrite Rmult_1_l. apply Rsqr_incr_0;[ | lt0 | lt0]. rewrite Rsqr_sqrt;[ | lt0]; unfold Rsqr; pattern y at 3. rewrite <- Rmult_1_r. apply Rmult_le_compat_l; lt0. replace (sqrt (1 * y)) with (v_ (0 + 1) y) by (rewrite plus_0_l; reflexivity). assert (ntf : (n = pred n + 1)%nat) by lia. rewrite ntf. apply Rge_le. apply (growing_prop _ _ _ (bn_growing 1 y (Rlt_le _ _ Rlt_0_1) (Rlt_le _ _ y0))). lia. unfold y_; assert (t := cmp_u_v y n inty). assert (t' := v_pos y n inty). apply Rlt_le, (Rmult_lt_reg_r (v_ n y));[psatzl R | ]. unfold Rdiv; rewrite Rmult_0_l, Rmult_minus_distr_r, Rmult_assoc, Rinv_l, Rmult_1_r, Rmult_1_l; psatzl R. Qed. Lemma q4_1_2y : forall x n, 0 < x < 1 -> y_ (n + 1) x = (1 + y_ n x) /(2 * (sqrt (y_ n x))). intros x n intx; unfold y_. replace (n + 1)%nat with (S n) by ring; rewrite u_step, v_step. assert (0 < u_ n x) by (apply u_pos; psatzl R). assert (0 < v_ n x) by (apply v_pos; psatzl R). replace (sqrt (u_ n x / v_ n x)) with (sqrt ((u_ n x * v_ n x)/(v_ n x) ^ 2)). rewrite sqrt_div, sqrt_pow2; try lt0. field; split; lt0. apply f_equal; field; lt0. Qed. Lemma q4_1_2z : forall x n, (1 <= n)%nat -> 0 < x < 1 -> z_ (n + 1) x = (1 + y_ n x * z_ n x)/((1 + z_ n x) * sqrt (y_ n x)). intros x n n1 intx; unfold z_, y_. replace (n + 1)%nat with (S n) by ring. destruct (derivable_u_n_v_n x n intx) as [du [dv [ dunn [dvp dup]]]]. assert (n1' := n1); apply dup in n1'. assert (du' := ex_derive_equiv_1 _ _ du). assert (dv' := ex_derive_equiv_1 _ _ dv). assert (dvp' := dvp); rewrite Derive_equiv in dvp'. assert (dup' := n1'); rewrite Derive_equiv in dup'. rewrite (Derive_ext (u_ (S n)) (fun x => /2 * (u_ n x + v_ n x)) x); [ | intros; rewrite u_step; field]. rewrite Derive_scal, Derive_plus; try (apply ex_derive_equiv_1; assumption). rewrite (Derive_ext (v_ (S n)) (fun x => sqrt (u_ n x * v_ n x))); [ | intros; rewrite v_step; reflexivity]. assert (0 < u_ n x) by (apply u_pos; lt0). assert (0 < v_ n x) by (apply v_pos; lt0). assert (pp : 0 < u_ n x * v_ n x) by lt0. rewrite (Derive_comp sqrt);[ | eapply ex_intro; apply derivable_pt_lim_sqrt;lt0 | apply ex_derive_mult; assumption]. rewrite Derive_mult; auto. rewrite (is_derive_unique _ _ _ (derivable_pt_lim_sqrt _ pp)). replace (sqrt (u_ n x / v_ n x)) with (sqrt ((u_ n x ^ 2)/(u_ n x * v_ n x))); [ | apply f_equal; field; lt0]. rewrite sqrt_div, sqrt_pow2; try lt0. set (s := sqrt (u_ n x * v_ n x)). rewrite <- (pow2_sqrt (u_ n x)), <- (pow2_sqrt (v_ n x)); try lt0. unfold s; rewrite sqrt_mult; try lt0. field; repeat split; lt0. Qed. Lemma q4_1_3 : forall x n, 0 < x < 1 -> (1 <= n)%nat -> 1 <= z_ n x. intros x n intx h; induction h. unfold z_. rewrite (Derive_ext (v_ 1) sqrt); [ | intros t; rewrite v_step; try lt0; change (v_ 0 t) with t; change (u_ 0 t) with 1; rewrite Rmult_1_l; reflexivity]. rewrite (Derive_ext (u_ 1) (fun x => /2 * (1 + x))); [ | intros t; rewrite u_step; try lt0; change (v_ 0 t) with t; change (u_ 0 t) with 1; unfold Rdiv; ring]. rewrite (is_derive_unique _ _ _ (derivable_pt_lim_sqrt x (proj1 intx))). rewrite Derive_scal, Derive_plus, ?Derive_const, Derive_id; [ | apply ex_derive_const | apply ex_derive_id]. replace (/(2 * sqrt x) / (/ 2 * (0 + 1))) with (/sqrt x) by (field;lt0). apply (Rmult_le_reg_l (sqrt x)); [lt0 | rewrite Rinv_r, Rmult_1_r;[|lt0]]. rewrite <- sqrt_1; apply sqrt_le_1_alt; psatzl R. (* reasoning 1 + s ^ 2 z/ ((1 + z) s) => 1 1 + s ^ 2 z => (1 + z) s 1 - s => z * (s * (1 - s)) 1 <= z * s 1/s <= z *) replace (S m) with (m + 1)%nat by ring; rewrite q4_1_2z; auto. assert (y1 := q4_1_1 x m intx). assert (0 < (1 + z_ m x) * sqrt (y_ m x)). rewrite Rplus_comm; lt0. apply (Rmult_le_reg_r ((1 + z_ m x) * sqrt (y_ m x)));[assumption | ]. unfold Rdiv; rewrite Rmult_assoc, Rinv_l, Rmult_1_r, Rmult_1_l;[|lt0]. pattern (y_ m x) at 2; rewrite <- pow2_sqrt;[|lt0]. rewrite Rmult_plus_distr_r, Rmult_1_l. apply Rplus_le_reg_l with (-sqrt(y_ m x) + -sqrt (y_ m x) ^ 2 * z_ m x). match goal with |- ?a <= ?b => replace a with (-(z_ m x * sqrt (y_ m x)) * (sqrt (y_ m x) - 1)) by ring; replace b with (-1 * (sqrt (y_ m x) - 1)) by ring end. assert (1 <= sqrt (y_ m x)). rewrite <- sqrt_1; apply sqrt_le_1_alt; lt0. apply Rmult_le_compat_r;[psatzl R | ]. apply Ropp_le_contravar; rewrite <- (Rmult_1_r 1). apply Rmult_le_compat; psatzl R. Qed. Lemma q4_1_3_c1 : forall x n, 0 < x < 1 -> Derive (u_ n) x <= Derive (v_ n) x. intros x [ | n] intx. rewrite (Derive_ext (u_ 0) (fun _ => 1));[ | intros; reflexivity]. rewrite (Derive_ext (v_ 0) (fun y => y));[ | intros; reflexivity]. rewrite Derive_const, Derive_id; psatzl R. replace (S n) with (n + 1)%nat by ring. destruct (derivable_u_n_v_n x (n + 1) intx) as [du [dv [ dunn [dvp dup]]]]. assert (dvp' := dvp); rewrite Derive_equiv in dvp'. assert (dup' : (1 <= n + 1)%nat) by lia. apply dup in dup'; rewrite Derive_equiv in dup'. apply Rmult_le_reg_r with (/Derive (u_ (n + 1)) x);[lt0 | ]. rewrite Rinv_r;[ | lt0]. apply q4_1_3;[assumption | lia]. Qed. Lemma q4_1_3_c2 : forall x, 0 < x < 1 -> Un_growing (fun n => Derive (u_ n) x). intros x intx n; rewrite (Derive_ext (u_ (S n)) (fun x => /2 * (u_ n x + v_ n x))); [ | intros; rewrite u_step; unfold Rdiv; ring ]. destruct (derivable_u_n_v_n x n intx) as [edu [edv [du [dv _]]]]. rewrite Derive_scal, Derive_plus; try (apply ex_derive_equiv_1; assumption). assert (t := q4_1_3_c1 x n intx); psatzl R. Qed. Lemma sqrt_lt : forall x, 1 < x -> sqrt x < x. intros x x1. assert (x0 : 0 < x) by (apply Rlt_trans with (1 := Rlt_0_1)(2 := x1)). assert (s0 : 0 < sqrt x) by (apply sqrt_lt_R0; assumption). pattern x at 2; rewrite <- sqrt_sqrt;[|apply Rlt_le; assumption]. pattern (sqrt x) at 1; rewrite <- Rmult_1_l. apply Rmult_lt_compat_r;[assumption | ]. rewrite <- sqrt_1; apply sqrt_lt_1_alt;split;[apply Rlt_le, Rlt_0_1|assumption]. Qed. Lemma q4_1_4 : forall x n, 0 < x < 1 -> (1 <= n)%nat -> y_ (n + 1) x <= z_ (n + 1) x <= sqrt (y_ n x). intros x n intx n1. generalize (q4_1_1 x n intx); intros; assert (0 < y_ n x) by lt0. assert (sqrt (y_ n x) < y_ n x);[apply sqrt_lt; assumption | ]. assert (t := q4_1_3 x n intx n1). assert (z_ (n + 1) x <= sqrt (y_ n x));[ | split;[|assumption]]. rewrite q4_1_2z; auto. unfold Rdiv; rewrite Rinv_mult_distr, <- !Rmult_assoc; try lt0. apply Rmult_le_reg_r with (sqrt (y_ n x));[lt0 | ]. rewrite !Rmult_assoc, Rinv_l, Rmult_1_r, sqrt_sqrt; try lt0. apply Rmult_le_reg_r with (1 + z_ n x);[lt0 | ]. rewrite Rmult_assoc, Rinv_l, Rmult_1_r;[ | lt0]. apply Rplus_le_reg_r with (- (y_ n x * z_ n x)); ring_simplify; lt0. rewrite q4_1_2y, q4_1_2z; auto. apply Rmult_le_reg_r with (2 * (1 + z_ n x) * (sqrt (y_ n x)));[lt0 | ]. field_simplify; [ | try lt0 | lt0]. unfold Rdiv; rewrite Rinv_1, !Rmult_1_r. apply Rplus_le_reg_r with (- (y_ n x * z_ n x + y_ n x + 1)); ring_simplify. replace (y_ n x * z_ n x - y_ n x) with (y_ n x * (z_ n x - 1)) by ring. apply Rle_trans with (1 * (z_ n x - 1) + 1);[psatzl R | ]. apply Rplus_le_compat_r, Rmult_le_compat_r; psatzl R. split;[lt0 | psatzl R ]. Qed. Lemma q4_1_4_c : forall lb ub, 0 < lb < ub -> ub < 1 -> forall c (delta : posreal), lb < c - delta -> c + delta < ub -> CVU z_ (fun _ => 1) c delta. intros lb ub lu0 u1 c delta c1 c2. assert (t := q4_1_1' lb ub lu0 u1 c delta c1 c2). intros eps ep; destruct (t _ ep) as [N Pn]; clear t. exists (S (S N)); intros n y nN dyc. destruct n as [|n]; [inversion nN | assert (nN' : (N <= n)%nat) by lia ]. assert (inty : 0 < y < 1) by (apply Rabs_lt_between in dyc; psatzl R). assert (t := q4_1_1 y n inty). assert (sn1 : (1 <= S n)%nat) by lia. assert (n1 : (1 <= n)%nat) by lia. assert (t' := q4_1_3 y _ inty sn1). generalize (Pn n y nN' dyc); rewrite <-(Rabs_Ropp (1 - y_ n y)), <- (Rabs_Ropp (1 - z_ (S n) y)), !Rabs_pos_eq; try lt0; intros. generalize (q4_1_4 y n inty n1), (sqrt_lt (y_ n y) t); replace (n + 1)%nat with (S n) by ring; intros; psatzl R. Qed. Lemma q4_1_5_p : forall lb ub, 0 < lb < ub -> ub < 1 -> forall c (delta : posreal), lb < c - delta -> c + delta < ub -> exists n_0, forall n, (n_0 <= n)%nat -> forall x, Boule c delta x -> (sqrt (y_ n x) - 1) ^ 2 <= (z_ n x - 1) / z_ n x. intros lb ub lu0 u1 c d c1 c2. destruct (q4_1_1' lb ub lu0 u1 c d c1 c2 (/2)) as [N1 Pn1];[psatzl R | ]. exists (S (S N1)); intros [ | n] nN1 x bx;[inversion nN1 | ]. assert (nN1' : (N1 <= (n + 1))%nat) by lia. assert (Pn1' := Pn1 _ _ nN1' bx). assert (bx' := bx). apply Rabs_lt_between in bx. assert (intx : 0 < x < 1) by psatzl R. assert (1 < y_ n x) by (apply q4_1_1; assumption). assert (1 < y_ (n + 1) x) by (apply q4_1_1; assumption). assert (1 < sqrt (y_ (n + 1) x)) by (rewrite <- sqrt_1; apply sqrt_lt_1_alt; psatzl R). destruct (q4_1_4 x n intx);[lia | ]. apply Rle_trans with ((z_ (S n) x - 1)/sqrt (y_ n x)). apply Rle_trans with ((sqrt (y_ (n + 1) x) - 1)/sqrt (y_ n x)). replace (S n) with (n + 1)%nat by ring. simpl; rewrite Rmult_1_r; apply Rmult_le_compat_l;[lt0 | ]. apply Rmult_le_reg_l with (sqrt (y_ n x));[lt0 |rewrite Rinv_r;[ | lt0]]. assert (nN2 : (N1 <= n)%nat) by lia. assert (Pn2 := Pn1 n x nN2 bx'). rewrite <- Rabs_Ropp, Rabs_pos_eq in Pn2;[|lt0]. assert (sqrt (y_ n x) < y_ n x) by (apply sqrt_lt; assumption). assert (sqrt (y_ n x) < 2) by psatzl R. assert (sqrt (y_ (n + 1) x) - 1 < /2). assert (Pn3 := Pn1 _ x nN1' bx'). rewrite <- Rabs_Ropp, Rabs_pos_eq in Pn3;[|lt0]. assert (sqrt (y_ (n + 1) x) < y_ (n + 1) x);[ | psatzl R]. apply sqrt_lt; assumption. replace 1 with (2 */2) by field. apply Rmult_le_compat; lt0. apply Rmult_le_compat_r;[lt0 | ]. destruct (q4_1_4 x (S n) intx);[lia | ]. assert (sqrt (y_ (n + 1) x) < y_ (n + 1) x). apply sqrt_lt; assumption. replace (S n) with (n + 1)%nat by ring; psatzl R. replace (S n) with (n + 1)%nat by ring. assert (n11 : (1 <= n + 1)%nat) by lia. generalize (q4_1_3 x (n + 1) intx n11); intros. apply Rmult_le_compat_l;[psatzl R | ]. apply Rle_Rinv;lt0. Qed. Lemma q4_1_5 : forall lb ub, 0 < lb < ub -> ub < 1 -> forall c (delta : posreal), lb < c - delta -> c + delta < ub -> exists n_0, forall n, (n_0 <= n)%nat -> forall x, Boule c delta x -> Derive (v_ (n + 1)) x <= Derive (v_ n) x. intros lb ub lu0 u1 c d c1 c2. destruct (q4_1_5_p lb ub lu0 u1 c d c1 c2) as [N Pn]. exists (N + 1)%nat; intros n nN x bx; assert (nN' : (N <= n)%nat) by lia. assert (n1 : (1 <= n)%nat) by lia. assert (pintx := bx); apply Rabs_lt_between in pintx. assert ((sqrt (y_ n x) - 1) ^ 2 <= (z_ n x -1)/z_ n x). apply (Pn n nN' x bx). assert (intx : 0 < x < 1) by psatzl R. destruct (derivable_u_n_v_n x n intx) as [du [dv [dunn [duv dup]]]]. assert (ex_derive (u_ n) x) by (apply ex_derive_equiv_1; assumption). assert (ex_derive (v_ n) x) by (apply ex_derive_equiv_1; assumption). rewrite !Derive_equiv in dup, duv; assert (dup' := n1); apply dup in dup'. assert (n2 : (1 <= n + 1)%nat) by lia. destruct (derivable_u_n_v_n x (n + 1) intx) as [dU [dV [dUnn [dUv dUp]]]]. assert (ex_derive (u_ (n + 1)) x) by (apply ex_derive_equiv_1; assumption). assert (ex_derive (v_ (n + 1)) x) by (apply ex_derive_equiv_1; assumption). rewrite !Derive_equiv in dUp, dUv; assert (dUp' := n2); apply dUp in dUp'. assert (main : Derive (u_(n + 1)) x = Derive (v_ n) x * (z_ n x + 1)/(2 * z_ n x)). rewrite (Derive_ext _ (fun x => /2 * (u_ n x + v_ n x))); [| intros; replace (n+1)%nat with (S n) by ring; rewrite u_step; field]. rewrite Derive_scal, Derive_plus; auto. unfold z_; field; split; lt0. replace (Derive (v_ (n + 1)) x) with (z_ (n + 1) x * Derive (u_ (n + 1)) x) by (unfold z_; field; lt0). assert (0 < z_ n x) by (assert (t := q4_1_3 x n intx n1); psatzl R). rewrite main; unfold Rdiv; rewrite Rinv_mult_distr;[ | lt0 | lt0]. rewrite <- !Rmult_assoc, <- (Rmult_comm (Derive _ _)), !Rmult_assoc. pattern (Derive (v_ n) x) at 2; rewrite <- Rmult_1_r. apply Rmult_le_compat_l;[lt0 | ]. apply Rmult_le_reg_r with (z_ n x);[lt0 | ]. rewrite !Rmult_assoc, Rinv_l, Rmult_1_r, Rmult_1_l;[ | lt0]. assert (0 < y_ n x) by (assert (t := (q4_1_1 x n intx)); psatzl R). rewrite q4_1_2z; auto; pattern (y_ n x) at 1; rewrite <- sqrt_sqrt;[ | lt0]. apply (Rmult_le_reg_r ((1 + z_ n x) * sqrt (y_ n x)));[lt0 | ]. unfold Rdiv; rewrite (Rmult_comm (_ * / _)). rewrite <- (Rmult_assoc _ _ (/ (_ * _))), (Rmult_assoc _ (/ (_ * _))). rewrite Rinv_l, Rmult_1_r; [ | lt0]. match goal with |- ?a <= ?b => apply Rplus_le_reg_l with (Ropp b) end. rewrite Rplus_opp_l. match goal with |- ?a <= 0 => replace a with ((z_ n x ^ 2 * ((sqrt (y_ n x) - 1) ^ 2 - 1) + z_ n x * ((sqrt (y_ n x) - 1) ^ 2 - 1 + 1) + 1) / 2) by field end. assert (remove_half : forall a, a <= 0 -> a/2 <= 0) by (intros; psatzl R); apply remove_half; clear remove_half. rewrite Rmult_plus_distr_l, !Rmult_minus_distr_l. apply Rle_trans with (z_ n x ^ 2 * ((z_ n x - 1)/z_ n x) - z_ n x ^ 2 + z_ n x * ((z_ n x - 1)/z_ n x) + 1). rewrite !Rmult_1_r. assert (cancel : forall a b, a - b + b = a) by (intros; ring); rewrite cancel; clear cancel. apply Rplus_le_compat_r. apply Rplus_le_compat. apply Rplus_le_compat_r. apply Rmult_le_compat_l;[lt0 | assumption]. apply Rmult_le_compat_l;[lt0 | assumption]. field_simplify; psatzl R. Qed. Lemma Boule_convex : forall c d x y z, Boule c d x -> Boule c d y -> x <= z <= y -> Boule c d z. intros c d x y z bx b_y intz. apply Rabs_lt_between in bx; apply Rabs_lt_between in b_y. apply Rabs_def1; psatzl R. Qed. Lemma CVU_derivable : forall f f' g g' c d, CVU f' g' c d -> (forall x, Boule c d x -> Un_cv (fun n => f n x) (g x)) -> (forall n x, Boule c d x -> derivable_pt_lim (f n) x (f' n x)) -> forall x, Boule c d x -> derivable_pt_lim g x (g' x). intros f f' g g' c d cvu cvp dff' x bx. set (rho_ := fun n y => if Req_EM_T y x then f' n x else ((f n y - f n x)/ (y - x))). set (rho := fun y => if Req_EM_T y x then g' x else (g y - g x)/(y - x)). assert (ctrho : forall n z, Boule c d z -> continuity_pt (rho_ n) z). intros n z bz. destruct (Req_EM_T x z) as [xz | xnz]. rewrite <- xz. intros eps' ep'. destruct (dff' n x bx eps' ep') as [alp Pa]. exists (pos alp);split;[apply cond_pos | ]. intros z'; unfold rho_, D_x, dist, R_met; simpl; intros [[_ xnz'] dxz']. destruct (Req_EM_T z' x) as [abs | _]. case xnz'; symmetry; exact abs. destruct (Req_EM_T x x) as [_ | abs];[ | case abs; reflexivity]. pattern z' at 1; replace z' with (x + (z' - x)) by ring. apply Pa;[psatzl R | exact dxz']. destruct (Ball_in_inter c c d d z bz bz) as [delta Pd]. assert (dz : 0 < Rmin delta (Rabs (z - x))). apply Rmin_glb_lt;[apply cond_pos | apply Rabs_pos_lt; psatzl R]. assert (t' : forall y : R, R_dist y z < Rmin delta (Rabs (z - x)) -> (fun z : R => (f n z - f n x) / (z - x)) y = rho_ n y). intros y dyz; unfold rho_; destruct (Req_EM_T y x) as [xy | xny]. rewrite xy in dyz. destruct (Rle_dec delta (Rabs (z - x))). rewrite Rmin_left, R_dist_sym in dyz; unfold R_dist in dyz; psatz R. rewrite Rmin_right, R_dist_sym in dyz; unfold R_dist in dyz; psatzl R. reflexivity. apply (continuity_pt_eq (fun z => (f n z - f n x)/(z - x)) (rho_ n) _ z dz t'); clear t'. reg;[ | psatzl R]. apply derivable_continuous_pt; eapply exist. apply dff'; assumption. assert (CVU rho_ rho c d ). intros eps ep. assert (ep8 : 0 < eps/8) by psatzl R. destruct (cvu _ ep8) as [N Pn1]. assert (cauchy1 : forall n p, (N <= n)%nat -> (N <= p)%nat -> forall z, Boule c d z -> Rabs (f' n z - f' p z) < eps/4). intros n p nN pN z bz; replace (eps/4) with (eps/8 + eps/8) by field. rewrite <- Rabs_Ropp. replace (-(f' n z - f' p z)) with (g' z - f' n z - (g' z - f' p z)) by ring. apply Rle_lt_trans with (1 := Rabs_triang _ _); rewrite Rabs_Ropp. apply Rplus_lt_compat; apply Pn1; assumption. assert (step_2 : forall n p, (N <= n)%nat -> (N <= p)%nat -> forall y, Boule c d y -> x <> y -> Rabs ((f n y - f n x)/(y - x) - (f p y - f p x)/(y - x)) < eps/4). intros n p nN pN y b_y xny. assert (mm0 : (Rmin x y = x /\ Rmax x y = y) \/ (Rmin x y = y /\ Rmax x y = x)). destruct (Rle_dec x y). rewrite Rmin_left, Rmax_right; psatzl R. rewrite Rmin_right, Rmax_left; psatzl R. assert (mm : Rmin x y < Rmax x y). destruct mm0 as [[q1 q2] | [q1 q2]]; generalize (Rminmax x y); rewrite q1, q2; intros; psatzl R. assert (dm : forall z, Rmin x y <= z <= Rmax x y -> is_derive (fun x => f n x - f p x) z (f' n z - f' p z)). intros z intz; apply derivable_pt_lim_minus. apply dff'; apply Boule_convex with (Rmin x y) (Rmax x y); destruct mm0 as [[q1 q2] | [q1 q2]]; revert intz; rewrite ?q1, ?q2; intros; try assumption. apply dff'; apply Boule_convex with (Rmin x y) (Rmax x y); destruct mm0 as [[q1 q2] | [q1 q2]]; revert intz; rewrite ?q1, ?q2; intros; try assumption. replace ((f n y - f n x) / (y - x) - (f p y - f p x) / (y - x)) with (((f n y - f p y) - (f n x - f p x))/(y - x)) by (field; psatzl R). destruct (MVT_cor2 (fun x => f n x - f p x) (fun x => f' n x - f' p x) (Rmin x y) (Rmax x y) mm dm) as [z [Pz inz]]. destruct mm0 as [[q1 q2] | [q1 q2]]. replace ((f n y - f p y - (f n x - f p x))/(y - x)) with ((f n (Rmax x y) - f p (Rmax x y) - (f n (Rmin x y) - f p (Rmin x y)))/ (Rmax x y - Rmin x y)) by (rewrite q1, q2; reflexivity). unfold Rdiv; rewrite Pz, Rmult_assoc, Rinv_r, Rmult_1_r. apply cauchy1; auto. apply Boule_convex with (Rmin x y) (Rmax x y); revert inz; rewrite ?q1, ?q2; intros; assumption || psatzl R. rewrite q1, q2; psatzl R. replace ((f n y - f p y - (f n x - f p x))/(y - x)) with ((f n (Rmax x y) - f p (Rmax x y) - (f n (Rmin x y) - f p (Rmin x y)))/ (Rmax x y - Rmin x y)). unfold Rdiv; rewrite Pz, Rmult_assoc, Rinv_r, Rmult_1_r. apply cauchy1; auto. apply Boule_convex with (Rmin x y) (Rmax x y); revert inz; rewrite ?q1, ?q2; intros; assumption || psatzl R. rewrite q1, q2; psatzl R. rewrite q1, q2; field; psatzl R. assert (unif_ac : forall n p, (N <= n)%nat -> (N <= p)%nat -> forall y, Boule c d y -> Rabs (rho_ n y - rho_ p y) <= eps/2). intros n p nN pN y b_y. destruct (Req_dec x y) as [xy | xny]. destruct (Ball_in_inter c c d d x bx bx) as [delta Pdelta]. destruct (ctrho n y b_y _ ep8) as [d' [dp Pd]]. destruct (ctrho p y b_y _ ep8) as [d2 [dp2 Pd2]]. assert (0 < (Rmin (Rmin d' d2) delta)/2) by lt0. apply Rle_trans with (1 := R_dist_tri _ _ (rho_ n (y + Rmin (Rmin d' d2) delta/2))). replace (eps/2) with (eps/8 + (eps/4 + eps/8)) by field. apply Rplus_le_compat. rewrite R_dist_sym; apply Rlt_le, Pd;split;[split;[exact I | psatzl R] | ]. simpl; unfold R_dist. unfold Rminus; rewrite (Rplus_comm y), Rplus_assoc, Rplus_opp_r, Rplus_0_r. rewrite Rabs_pos_eq;[ | psatzl R]. apply Rlt_le_trans with (Rmin (Rmin d' d2) delta);[psatzl R | ]. apply Rle_trans with (Rmin d' d2); apply Rmin_l. apply Rle_trans with (1 := R_dist_tri _ _ (rho_ p (y + Rmin (Rmin d' d2) delta/2))). apply Rplus_le_compat. apply Rlt_le. replace (rho_ n (y + Rmin (Rmin d' d2) delta / 2)) with ((f n (y + Rmin (Rmin d' d2) delta / 2) - f n x)/ ((y + Rmin (Rmin d' d2) delta / 2) - x)). replace (rho_ p (y + Rmin (Rmin d' d2) delta / 2)) with ((f p (y + Rmin (Rmin d' d2) delta / 2) - f p x)/ ((y + Rmin (Rmin d' d2) delta / 2) - x)). apply step_2; auto; try psatzl R. assert (0 < pos delta) by (apply cond_pos). apply Boule_convex with y (y + delta/2). assumption. destruct (Pdelta (y + delta/2)); auto. rewrite xy; unfold Boule; rewrite Rabs_pos_eq; try psatzl R; auto. split; try psatzl R. apply Rplus_le_compat_l, Rmult_le_compat_r;[lt0 | apply Rmin_r]. unfold rho_. destruct (Req_EM_T (y + Rmin (Rmin d' d2) delta/2) x);psatzl R. unfold rho_. destruct (Req_EM_T (y + Rmin (Rmin d' d2) delta / 2) x); psatzl R. apply Rlt_le, Pd2; split;[split;[exact I | psatzl R] | ]. simpl; unfold R_dist. unfold Rminus; rewrite (Rplus_comm y), Rplus_assoc, Rplus_opp_r, Rplus_0_r. rewrite Rabs_pos_eq;[ | psatzl R]. apply Rlt_le_trans with (Rmin (Rmin d' d2) delta); [psatzl R |]. apply Rle_trans with (Rmin d' d2). solve[apply Rmin_l]. solve[apply Rmin_r]. apply Rlt_le, Rlt_le_trans with (eps/4);[ | psatzl R]. unfold rho_; destruct (Req_EM_T y x); solve[auto]. assert (unif_ac' : forall p, (N <= p)%nat -> forall y, Boule c d y -> Rabs (rho y - rho_ p y) < eps). assert (cvrho : forall y, Boule c d y -> Un_cv (fun n => rho_ n y) (rho y)). intros y b_y; unfold rho_, rho; destruct (Req_EM_T y x). intros eps' ep'; destruct (cvu eps' ep') as [N2 Pn2]. exists N2; intros n nN2; rewrite R_dist_sym; apply Pn2; assumption. apply CV_mult. apply CV_minus. apply cvp; assumption. apply cvp; assumption. intros eps' ep'; simpl; exists 0%nat; intros; rewrite R_dist_eq; assumption. intros p pN y b_y. replace eps with (eps/2 + eps/2) by field. assert (ep2 : 0 < eps/2) by psatzl R. destruct (cvrho y b_y _ ep2) as [N2 Pn2]. apply Rle_lt_trans with (1 := R_dist_tri _ _ (rho_ (max N N2) y)). apply Rplus_lt_le_compat. solve[rewrite R_dist_sym; apply Pn2, Max.le_max_r]. apply unif_ac; auto; solve [apply Max.le_max_l]. exists N; intros; apply unif_ac'; solve[auto]. intros eps ep. destruct (CVU_continuity _ _ _ _ H ctrho x bx eps ep) as [delta [dp Pd]]. exists (mkposreal _ dp); intros h hn0 dh. replace ((g (x + h) - g x) / h) with (rho (x + h)). replace (g' x) with (rho x). apply Pd; unfold D_x, no_cond;split;[split;[auto | psatzl R] | ]. simpl; unfold R_dist; replace (x + h - x) with h by ring; exact dh. unfold rho; destruct (Req_EM_T x x) as [ _ | abs];[ | case abs]; reflexivity. unfold rho; destruct (Req_EM_T (x + h) x) as [abs | _];[psatzl R | ]. replace (x + h - x) with h by ring; reflexivity. Qed. Definition interval_dec l u x : {l <= x <= u}+{~l <= x <= u}. destruct (Rle_dec l x) as [lx | nlx]. destruct (Rle_dec x u) as [xu | nxu]. left; split; assumption. right; psatzl R. right; psatzl R. Qed. Lemma Un_growing_shift : (* standard *) forall k un, Un_growing un -> Un_growing (fun n => un (n + k)%nat). intros k un P n; apply P. Qed. Lemma CVU_cv : forall f g c d, CVU f g c d -> (*standard. *) forall x, Boule c d x -> Un_cv (fun n => f n x) (g x). intros f g c d cvu x bx eps ep; destruct (cvu eps ep) as [N Pn]. exists N; intros n nN; rewrite R_dist_sym; apply Pn; assumption. Qed. Lemma CVU_ext_lim : forall f g1 g2 c d, CVU f g1 c d -> (forall x, Boule c d x -> g1 x = g2 x) -> CVU f g2 c d. intros f g1 g2 c d cvu q eps ep; destruct (cvu _ ep) as [N Pn]. exists N; intros; rewrite <- q; auto. Qed. Lemma q4_1_5_c2 : forall lb ub, 0 < lb < ub -> ub < 1 -> forall c (delta : posreal), lb < c - delta -> c + delta < ub -> CVU (fun n => Derive (u_ n)) (Derive ff) c delta. intros lb ub lu0 u1 c d c1 c2. assert (lu : lb < ub) by tauto. set (lb' := lb/2); set (ub' := (1 + ub)/2). assert (0 < lb' < ub' /\ ub' < 1) as [lu0' u1'] by (unfold lb', ub'; psatzl R). set (lb2 := (lb' + lb)/2); set (ub2 := (ub' + ub)/2). set (c'' := (lb2 + ub2)/2); set (d'' := (ub2 - lb2)/2). assert (d''0 : 0 < d'') by (unfold d'', lb2, ub2, ub', lb' ; psatzl R). set (delta'' := mkposreal d'' d''0). set (c' := (lb + ub)/2); set (d' := (ub - lb)/2). assert (d'0 : 0 < d') by (unfold d'; psatzl R). set (delta' := mkposreal d' d'0). assert (c1' : lb' < c' - d') by (unfold lb', c', d'; psatzl R). assert (c1'' : lb' < c'' - d'') by (unfold c'', d'', lb2, ub2, lb', ub' ; psatzl R). assert (c2' : c' + d' < ub') by (unfold ub', c', d'; psatzl R). assert (c2'' : c'' + d'' < ub') by (unfold c'', d'', lb2, ub2, lb', ub', c', d'; psatzl R). assert (ball : forall x, Boule c' (mkposreal _ d'0) x <-> lb < x < ub). intros x; split. intros bx; apply Rabs_lt_between in bx; simpl in bx; unfold c', d' in bx. psatzl R. intros intx; apply Rabs_def1; simpl; unfold c', d'; psatzl R. destruct (q4_1_5 lb' ub' lu0' u1' c'' delta'' c1'' c2'') as [n_0 difv]. assert (mkl : forall x, c' - delta' <= x <= c' + delta' -> {l | Un_cv (fun n => Derive (u_ n) x) l}). intros x;unfold delta'; simpl; intros intx. assert (intx' : 0 < x < 1) by psatzl R. assert (gr_shift : Un_growing (fun n => Derive (u_ (n + n_0)) x)) by (apply (Un_growing_shift n_0 (fun n => Derive (u_ n) x)), q4_1_3_c2; assumption). assert (ub_shift : has_ub (fun n => Derive (u_ (n + n_0)) x)). exists (Derive (v_ (n_0)) x); apply Un_bound_imp. intros n; apply Rle_trans with (Derive (v_ (n + n_0)) x). apply q4_1_3_c1; assumption. induction n;[solve[apply Rle_refl] | ]. replace (S n + n_0)%nat with (n + n_0 + 1)%nat by ring. apply Rle_trans with (2 := IHn), difv;[lia | ]. assert (c'' - d'' < c' - d') by (unfold c'', d'', c', d', lb2, ub2, lb', ub'; psatzl R). assert (c' + d' < c'' + d'') by (unfold c'', d'', c', d', lb2, ub2, lb', ub'; psatzl R). unfold delta''; apply Rabs_def1; simpl; psatzl R. destruct (growing_cv _ gr_shift ub_shift) as [l dunl]. exists l; apply CV_shift with n_0; assumption. assert (cvu_dif : CVU (fun n x => Derive (u_ (n + (n_0 + 1))) x - Derive (v_ (n + (n_0 + 1))) x) (fun _ => 0) c d). assert (cvdif : forall x : R, lb <= x <= ub -> Un_cv (fun n => Derive (u_ n) x - Derive (v_ n) x) 0). intros x intx; assert (intx' : 0 < x < 1) by psatzl R. apply CV_shift with (n_0 + 1)%nat. apply (Un_cv_ext (fun n => (1 - z_ (n + (n_0 + 1)) x) * Derive (u_ (n + (n_0 + 1))) x)). intros n; unfold z_; field. destruct (derivable_u_n_v_n x (n + (n_0 + 1)) intx') as [dU [dV [dUnn [dUv dUp]]]]. assert (ex_derive (u_ (n + (n_0 + 1))) x) by (apply ex_derive_equiv_1; assumption). assert (n2 : (1 <= (n + (n_0 + 1)))%nat) by lia. rewrite !Derive_equiv in dUp; assert (dUp' := n2); apply dUp in dUp'; lt0. assert (new_int : c' - delta' <= x <= c' + delta'). unfold c', delta', d'; simpl; psatzl R. destruct (mkl x new_int) as [l Pl]. rewrite <- (Rmult_0_l l); rewrite <- (Rminus_eq0 1). apply CV_mult. apply CV_minus. intros; exists 0%nat; intros; rewrite R_dist_eq; assumption. apply (CV_shift' (fun i => z_ i x) (n_0 + 1)). apply (CVU_cv z_ (fun x => 1) c'' delta''). apply (q4_1_4_c lb' ub' lu0' u1' c'' delta''); assumption. apply Rabs_def1; simpl; unfold c'', d'', lb2, ub2, lb', ub'; psatzl R. apply (CV_shift' (fun n => Derive (u_ n) x)); assumption. assert (cvdif' : forall x, lb <= x <= ub -> Un_cv (fun n => Derive (u_ (n + (n_0 + 1))) x - Derive (v_ (n + (n_0 + 1))) x) 0). intros; apply (CV_shift' (fun n => Derive (u_ n) x - Derive (v_ n) x)). apply cvdif; assumption. assert (ctdif : forall n x, lb <= x <= ub -> continuity_pt (fun y => Derive (u_ (n + (n_0 + 1))) y - Derive (v_ (n + (n_0 + 1))) y) x). intros n x intx; assert (intx' : 0 < x < 1) by psatzl R. destruct (ct_derive x (n + (n_0 + 1)) intx') as [du dv]; reg; assumption. assert (ct0 : forall x, lb <= x <= ub -> continuity_pt (fun _ => 0) x). unfold continuity_pt; intros; exists 1; split;[psatzl R | ]. intros; rewrite R_dist_eq; assumption. assert (grdif : forall x, lb <= x <= ub -> Un_growing (fun n => Derive (u_ (n + (n_0 + 1))) x - Derive (v_ (n + (n_0 + 1))) x)). intros x intx n; clear ct0 ctdif cvdif' cvdif. assert (intx' : 0 < x < 1) by psatzl R. assert (gru : Derive (u_ (n + (n_0 + 1))) x <= Derive (u_ (S n + (n_0 + 1))) x). apply q4_1_3_c2; assumption. assert (grv : Derive (v_ (S n + (n_0 + 1))) x <= Derive (v_ (n + (n_0 + 1))) x). replace (S n + (n_0 + 1))%nat with ((n + 1) + n_0 + 1)%nat by ring. replace (n + (n_0 + 1))%nat with (n + 1 + n_0)%nat by ring. apply difv;[lia | ]. apply Rabs_def1; simpl; unfold c'', d'', lb2, ub2, lb', ub'; psatzl R. psatzl R. apply (Dini lb ub (proj2 lu0) _ (fun _ => 0) cvdif' ctdif ct0 grdif). intros x bx; apply Rabs_lt_between in bx; psatzl R. assert (cdlu : forall x, lb <= x <= ub -> c' - d' <= x <= c' + d') by (intros; unfold c', d'; psatzl R). set (ffu' := fun x => match interval_dec lb ub x with left h => let (l, _) := mkl x (cdlu _ h) in l | right h => 0 end). assert (dffu' : CVU (fun n => Derive (u_ n)) ffu' c d). intros eps ep; destruct (cvu_dif eps ep) as [N Pn]. exists (N + (n_0 + 1))%nat. intros n x nN bx; assert (bx' := bx); apply Rabs_lt_between in bx'. assert (cmp : forall n m, (N + n_0 <= n)%nat -> (N + n_0 <= m)%nat -> Derive (u_ m) x <= Derive (v_ n) x). intros m p mN pN. apply Rle_trans with (Derive (u_ (max m p)) x). apply (tech9 (fun n => Derive (u_ n) x));[ | lia]. apply q4_1_3_c2; psatzl R. apply Rle_trans with (Derive (v_ (max m p)) x). apply q4_1_3_c1; psatzl R. assert (m <= max m p)%nat by lia. assert (rc :forall k, (m <= k)%nat -> Derive (v_ k) x <= Derive (v_ m) x). intros k cmp; induction cmp as [| m' lem' IH]. solve[apply Rle_refl]. apply Rle_trans with (2 := IH). replace (S m') with (m' + 1)%nat by ring; apply difv. lia. apply Rabs_def1; simpl; unfold c'', d'', lb2, ub2, lb', ub'; psatzl R. solve[auto]. rewrite Rabs_pos_eq. apply Rle_lt_trans with (Derive (v_ n) x - Derive (u_ n) x). apply Rplus_le_compat_r. apply Rle_cv_lim with (fun n => (Derive (u_ n) x)) (fun _ => Derive (v_ n) x). intros m; apply Rle_trans with (Derive (u_ (max m (N + n_0))) x). apply (tech9 (fun n => Derive (u_ n) x));[ | lia]. apply q4_1_3_c2; psatzl R. apply cmp; lia. unfold ffu'; destruct (interval_dec lb ub x);[ | psatzl R]. destruct (mkl x (cdlu x a)); assumption. intros; exists O; intros; rewrite R_dist_eq; assumption. assert (nN' : (N <= n - (n_0 + 1))%nat) by lia. generalize (Pn _ _ nN' bx). replace (n - (n_0 + 1) + (n_0 + 1))%nat with n by lia. rewrite Rabs_pos_eq. intros; psatzl R. assert (Derive (u_ n) x <= Derive (v_ n) x) by (apply cmp; lia). psatzl R. assert (Derive (u_ n) x <= ffu' x); [ | psatzl R]. apply (growing_ineq (fun n => Derive (u_ n) x)). apply q4_1_3_c2; psatzl R. unfold ffu'; destruct (interval_dec lb ub x);[ | psatzl R]. destruct (mkl x (cdlu x a)); assumption. assert (cv_u : forall x, Boule c d x -> Un_cv (fun n => u_ n x) (ff x)). intros x bx; apply Rabs_lt_between in bx. assert (intx : 0 < x < 1) by psatzl R. apply M_def; psatzl R. assert (du : forall n x, Boule c d x -> is_derive (u_ n) x (Derive (u_ n) x)). intros n x bx; apply Rabs_lt_between in bx. assert (intx : 0 < x < 1) by psatzl R. apply Derive_correct; destruct (derivable_u_n_v_n x n intx) as [du [dv _]]. apply ex_derive_equiv_1; assumption. assert (dff_ffu' := CVU_derivable u_ _ ff ffu' c d dffu' cv_u du). apply (CVU_ext_lim _ ffu');[exact dffu' | ]. intros x bx; rewrite (is_derive_unique _ _ _ (dff_ffu' x bx)). reflexivity. Qed. Lemma q4_2_1 : Un_cv (fun n => (v_ n (/sqrt 2) ^ 2 * u_ n (/sqrt 2)) / Derive (u_ n) (/sqrt 2)) (PI / (2 * sqrt 2)). assert (ints : 0 < /sqrt 2 < 1). split;[lt0 | pattern 1 at 3; rewrite <- Rinv_1]. apply Rinv_lt_contravar;[lt0 | ]. pattern 1 at 1; rewrite <- sqrt_1; apply sqrt_lt_1_alt; psatzl R. assert (dfs := derive_ff_pos (/sqrt 2) ints). replace (PI/(2*sqrt 2)) with ((ff(/sqrt 2) ^ 2 * ff(/sqrt 2))/Derive ff (/sqrt 2)). apply CV_mult;[apply CV_mult | ]. apply (continuity_seq (fun x => x ^ 2)). reg. apply M_def'; lt0. apply M_def; lt0. apply (continuity_seq Rinv). reg; lt0. assert (lu0 : 0 < /8 < 7/8) by psatzl R. assert (u1 : 7/8 < 1) by psatzl R. assert (h2 : 0 < /4) by psatzl R. assert (d1 : /8 < /2 - /4) by psatzl R. assert (d2 : /2 + /4 < 7/8) by psatzl R. intros eps ep. destruct (q4_1_5_c2 _ _ lu0 u1 (/2) (mkposreal _ h2) d1 d2 _ ep) as [N Pn]. exists N; intros n nN; rewrite R_dist_sym. apply (Pn n (/sqrt 2)). assumption. unfold Boule, pos; rewrite Rabs_pos_eq. assert (/sqrt 2 < 3/4);[ | psatzl R]. replace (3/4) with (/sqrt ((4/3) ^ 2)). apply Rinv_lt_contravar;[lt0 | ]. apply sqrt_lt_1_alt; split; psatzl R. rewrite sqrt_pow2;[ | psatzl R]; field. assert (/2 <= /sqrt 2);[ | psatzl R]. apply Rle_Rinv;[lt0 | lt0 | apply Rlt_le, sqrt_lt; psatzl R]. rewrite q3_3_2; field; split; lt0. Qed. Lemma Rdiv_plus_distr : forall a b c, (a + b)/c = a/c + b/c. intros a b c; unfold Rdiv; apply Rmult_plus_distr_r. Qed. Fixpoint agmpi n := match n with 0%nat => (2 + sqrt 2) | S p => agmpi p * (1 + y_ n (/sqrt 2)) / (1 + z_ n (/sqrt 2)) end. Lemma agmpi_step n : agmpi n = match n with 0%nat => (2 + sqrt 2) | S p => agmpi p * (1 + y_ n (/sqrt 2)) / (1 + z_ n (/sqrt 2)) end. destruct n as [ | p]; reflexivity. Qed. Lemma cv_agm : Un_cv agmpi PI. assert (ints : 0 < /sqrt 2 < 1). split;[lt0 | pattern 1 at 3; rewrite <- Rinv_1; apply Rinv_lt_contravar;[lt0 | ]]. pattern 1 at 1; rewrite <- sqrt_1; apply sqrt_lt_1_alt; psatzl R. apply (Un_cv_ext (fun n => 2 * sqrt 2 * ((v_ (n + 1) (/sqrt 2) ^ 2 * u_ (n + 1) (/sqrt 2)) / Derive (u_ (n + 1)) (/sqrt 2)))). induction n. simpl plus; rewrite v_step, u_step. replace (u_ 0 (/sqrt 2)) with 1 by reflexivity. replace (v_ 0 (/sqrt 2)) with (/sqrt 2) by reflexivity. rewrite Rmult_1_l, pow2_sqrt;[ | lt0]. rewrite Derive_ext with (g := fun x => /2 * (1 + x)); [ | intros; unfold u_; simpl; field]. rewrite Derive_scal, Derive_plus, ?Derive_const, ?Derive_id; try solve[apply ex_derive_const| apply ex_derive_id| ring]. match goal with |- ?a = _ => assert (qa : a = (2 * sqrt 2 + 2) / sqrt 2);[field; lt0 | rewrite qa ] end. pattern 2 at 3; rewrite <- (sqrt_sqrt 2), Rdiv_plus_distr; unfold Rdiv; [ | lt0]. rewrite !Rmult_assoc, Rinv_r, !Rmult_1_r;[ | lt0]. reflexivity. destruct (derivable_u_n_v_n (/sqrt 2) (n + 1)) as [du [dv [dunn [dvp dup]]]]; try assumption. assert (dup' : (1 <= n + 1)%nat) by lia; apply dup in dup'. assert (ex_derive (u_ (n + 1)) (/sqrt 2)) by (apply ex_derive_equiv_1, du). assert (ex_derive (v_ (n + 1)) (/sqrt 2)) by (apply ex_derive_equiv_1, dv). assert (0 < Derive (u_ (n + 1)) (/sqrt 2)) by (rewrite <- (Derive_equiv _ _ du); assumption). assert (0 < Derive (v_ (n + 1)) (/sqrt 2)) by (rewrite <- (Derive_equiv _ _ dv); assumption). rewrite agmpi_step, <- IHn, !Rmult_assoc; repeat apply f_equal; simpl (S n + 1)%nat. replace (Derive (u_ (S (n + 1))) (/sqrt 2)) with (/2 * (Derive (u_ (n + 1)) (/sqrt 2) + Derive (v_ (n + 1)) (/sqrt 2))). replace (v_ (S (n + 1)) (/sqrt 2) ^ 2) with (u_ (n + 1) (/sqrt 2) * v_ (n + 1) (/sqrt 2)). rewrite u_step. replace (S n) with (n + 1)%nat by ring; unfold y_, z_. assert (t := v_pos (/sqrt 2) (n + 1) ints). field; repeat split; lt0. rewrite v_step, pow2_sqrt; [reflexivity | apply Rlt_le, Rmult_lt_0_compat;[apply u_pos|apply v_pos];assumption]. rewrite (Derive_ext (u_ (S _)) (fun x => /2 * (u_ (n + 1) x + v_ (n + 1) x))). rewrite Derive_scal, Derive_plus; reflexivity || assumption. intros; rewrite u_step; field. apply (CV_shift' (fun n => 2 * sqrt 2 * ((v_ n (/sqrt 2) ^ 2 * u_ n (/sqrt 2)) / Derive (u_ n) (/sqrt 2)))). replace PI with ((2 * sqrt 2) * (PI/(2 * sqrt 2))) by (field; lt0). apply CV_mult. intros eps ep; exists 0%nat; intros n n0; rewrite R_dist_eq; assumption. apply q4_2_1. Qed.