# Library Coq.Reals.PartSum

```   Require Import Rbase. Require Import Rfunctions. Require Import Rseries. Require Import Rcomplete. Require Import Max. Open Local Scope R_scope. Lemma tech1 :  forall (An:nat -> R) (N:nat),    (forall n:nat, (n <= N)%nat -> 0 < An n) -> 0 < sum_f_R0 An N. intros; induction N as [| N HrecN]. simpl in |- *; apply H; apply le_n. simpl in |- *; apply Rplus_lt_0_compat. apply HrecN; intros; apply H; apply le_S; assumption. apply H; apply le_n. Qed. Lemma tech2 :  forall (An:nat -> R) (m n:nat),    (m < n)%nat ->    sum_f_R0 An n =    sum_f_R0 An m + sum_f_R0 (fun i:nat => An (S m + i)%nat) (n - S m). intros; induction n as [| n Hrecn]. elim (lt_n_O _ H). cut ((m < n)%nat \/ m = n). intro; elim H0; intro. replace (sum_f_R0 An (S n)) with (sum_f_R0 An n + An (S n));  [ idtac | reflexivity ]. replace (S n - S m)%nat with (S (n - S m)). replace (sum_f_R0 (fun i:nat => An (S m + i)%nat) (S (n - S m))) with  (sum_f_R0 (fun i:nat => An (S m + i)%nat) (n - S m) +   An (S m + S (n - S m))%nat); [ idtac | reflexivity ]. replace (S m + S (n - S m))%nat with (S n). rewrite (Hrecn H1). ring. apply INR_eq; rewrite S_INR; rewrite plus_INR; do 2 rewrite S_INR;  rewrite minus_INR. rewrite S_INR; ring. apply lt_le_S; assumption. apply INR_eq; rewrite S_INR; repeat rewrite minus_INR. repeat rewrite S_INR; ring. apply le_n_S; apply lt_le_weak; assumption. apply lt_le_S; assumption. rewrite H1; rewrite <- minus_n_n; simpl in |- *. replace (n + 0)%nat with n; [ reflexivity | ring ]. inversion H. right; reflexivity. left; apply lt_le_trans with (S m); [ apply lt_n_Sn | assumption ]. Qed. Lemma tech3 :  forall (k:R) (N:nat),    k <> 1 -> sum_f_R0 (fun i:nat => k ^ i) N = (1 - k ^ S N) / (1 - k). intros; cut (1 - k <> 0). intro; induction N as [| N HrecN]. simpl in |- *; rewrite Rmult_1_r; unfold Rdiv in |- *; rewrite <- Rinv_r_sym. reflexivity. apply H0. replace (sum_f_R0 (fun i:nat => k ^ i) (S N)) with  (sum_f_R0 (fun i:nat => k ^ i) N + k ^ S N); [ idtac | reflexivity ];  rewrite HrecN;  replace ((1 - k ^ S N) / (1 - k) + k ^ S N) with   ((1 - k ^ S N + (1 - k) * k ^ S N) / (1 - k)). apply Rmult_eq_reg_l with (1 - k). unfold Rdiv in |- *; do 2 rewrite <- (Rmult_comm (/ (1 - k)));  repeat rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym;  [ do 2 rewrite Rmult_1_l; simpl in |- *; ring | apply H0 ]. apply H0. unfold Rdiv in |- *; rewrite Rmult_plus_distr_r; rewrite (Rmult_comm (1 - k));  repeat rewrite Rmult_assoc; rewrite <- Rinv_r_sym. rewrite Rmult_1_r; reflexivity. apply H0. apply Rminus_eq_contra; red in |- *; intro; elim H; symmetry in |- *;  assumption. Qed. Lemma tech4 :  forall (An:nat -> R) (k:R) (N:nat),    0 <= k -> (forall i:nat, An (S i) < k * An i) -> An N <= An 0%nat * k ^ N. intros; induction N as [| N HrecN]. simpl in |- *; right; ring. apply Rle_trans with (k * An N). left; apply (H0 N). replace (S N) with (N + 1)%nat; [ idtac | ring ]. rewrite pow_add; simpl in |- *; rewrite Rmult_1_r;  replace (An 0%nat * (k ^ N * k)) with (k * (An 0%nat * k ^ N));  [ idtac | ring ]; apply Rmult_le_compat_l. assumption. apply HrecN. Qed. Lemma tech5 :  forall (An:nat -> R) (N:nat), sum_f_R0 An (S N) = sum_f_R0 An N + An (S N). intros; reflexivity. Qed. Lemma tech6 :  forall (An:nat -> R) (k:R) (N:nat),    0 <= k ->    (forall i:nat, An (S i) < k * An i) ->    sum_f_R0 An N <= An 0%nat * sum_f_R0 (fun i:nat => k ^ i) N. intros; induction N as [| N HrecN]. simpl in |- *; right; ring. apply Rle_trans with (An 0%nat * sum_f_R0 (fun i:nat => k ^ i) N + An (S N)). rewrite tech5; do 2 rewrite <- (Rplus_comm (An (S N)));  apply Rplus_le_compat_l. apply HrecN. rewrite tech5; rewrite Rmult_plus_distr_l; apply Rplus_le_compat_l. apply tech4; assumption. Qed. Lemma tech7 : forall r1 r2:R, r1 <> 0 -> r2 <> 0 -> r1 <> r2 -> / r1 <> / r2. intros; red in |- *; intro. assert (H3:= Rmult_eq_compat_l r1 _ _ H2). rewrite <- Rinv_r_sym in H3; [ idtac | assumption ]. assert (H4:= Rmult_eq_compat_l r2 _ _ H3). rewrite Rmult_1_r in H4; rewrite <- Rmult_assoc in H4. rewrite Rinv_r_simpl_m in H4; [ idtac | assumption ]. elim H1; symmetry in |- *; assumption. Qed. Lemma tech11 :  forall (An Bn Cn:nat -> R) (N:nat),    (forall i:nat, An i = Bn i - Cn i) ->    sum_f_R0 An N = sum_f_R0 Bn N - sum_f_R0 Cn N. intros; induction N as [| N HrecN]. simpl in |- *; apply H. do 3 rewrite tech5; rewrite HrecN; rewrite (H (S N)); ring. Qed. Lemma tech12 :  forall (An:nat -> R) (x l:R),    Un_cv (fun N:nat => sum_f_R0 (fun i:nat => An i * x ^ i) N) l ->    Pser An x l. intros; unfold Pser in |- *; unfold infinit_sum in |- *; unfold Un_cv in H;  assumption. Qed. Lemma scal_sum :  forall (An:nat -> R) (N:nat) (x:R),    x * sum_f_R0 An N = sum_f_R0 (fun i:nat => An i * x) N. intros; induction N as [| N HrecN]. simpl in |- *; ring. do 2 rewrite tech5. rewrite Rmult_plus_distr_l; rewrite <- HrecN; ring. Qed. Lemma decomp_sum :  forall (An:nat -> R) (N:nat),    (0 < N)%nat ->    sum_f_R0 An N = An 0%nat + sum_f_R0 (fun i:nat => An (S i)) (pred N). intros; induction N as [| N HrecN]. elim (lt_irrefl _ H). cut ((0 < N)%nat \/ N = 0%nat). intro; elim H0; intro. cut (S (pred N) = pred (S N)). intro; rewrite <- H2. do 2 rewrite tech5. replace (S (S (pred N))) with (S N). rewrite (HrecN H1); ring. rewrite H2; simpl in |- *; reflexivity. assert (H2:= O_or_S N). elim H2; intros. elim a; intros. rewrite <- p. simpl in |- *; reflexivity. rewrite <- b in H1; elim (lt_irrefl _ H1). rewrite H1; simpl in |- *; reflexivity. inversion H. right; reflexivity. left; apply lt_le_trans with 1%nat; [ apply lt_O_Sn | assumption ]. Qed. Lemma plus_sum :  forall (An Bn:nat -> R) (N:nat),    sum_f_R0 (fun i:nat => An i + Bn i) N = sum_f_R0 An N + sum_f_R0 Bn N. intros; induction N as [| N HrecN]. simpl in |- *; ring. do 3 rewrite tech5; rewrite HrecN; ring. Qed. Lemma sum_eq :  forall (An Bn:nat -> R) (N:nat),    (forall i:nat, (i <= N)%nat -> An i = Bn i) ->    sum_f_R0 An N = sum_f_R0 Bn N. intros; induction N as [| N HrecN]. simpl in |- *; apply H; apply le_n. do 2 rewrite tech5; rewrite HrecN. rewrite (H (S N)); [ reflexivity | apply le_n ]. intros; apply H; apply le_trans with N; [ assumption | apply le_n_Sn ]. Qed. Lemma uniqueness_sum :  forall (An:nat -> R) (l1 l2:R),    infinit_sum An l1 -> infinit_sum An l2 -> l1 = l2. unfold infinit_sum in |- *; intros. case (Req_dec l1 l2); intro. assumption. cut (0 < Rabs ((l1 - l2) / 2)); [ intro | apply Rabs_pos_lt ]. elim (H (Rabs ((l1 - l2) / 2)) H2); intros. elim (H0 (Rabs ((l1 - l2) / 2)) H2); intros. set (N:= max x0 x); cut (N >= x0)%nat. cut (N >= x)%nat. intros; assert (H7:= H3 N H5); assert (H8:= H4 N H6). cut (Rabs (l1 - l2) <= R_dist (sum_f_R0 An N) l1 + R_dist (sum_f_R0 An N) l2). intro; assert (H10:= Rplus_lt_compat _ _ _ _ H7 H8);  assert (H11:= Rle_lt_trans _ _ _ H9 H10); unfold Rdiv in H11;  rewrite Rabs_mult in H11. cut (Rabs (/ 2) = / 2). intro; rewrite H12 in H11; assert (H13:= double_var); unfold Rdiv in H13;  rewrite <- H13 in H11. elim (Rlt_irrefl _ H11). apply Rabs_right; left; change (0 < / 2) in |- *; apply Rinv_0_lt_compat;  cut (0%nat <> 2%nat);  [ intro H20; generalize (lt_INR_0 2 (neq_O_lt 2 H20)); unfold INR in |- *; intro; assumption | discriminate ]. unfold R_dist in |- *; rewrite <- (Rabs_Ropp (sum_f_R0 An N - l1));  rewrite Ropp_minus_distr'. replace (l1 - l2) with (l1 - sum_f_R0 An N + (sum_f_R0 An N - l2));  [ idtac | ring ]. apply Rabs_triang. unfold ge in |- *; unfold N in |- *; apply le_max_r. unfold ge in |- *; unfold N in |- *; apply le_max_l. unfold Rdiv in |- *; apply prod_neq_R0. apply Rminus_eq_contra; assumption. apply Rinv_neq_0_compat; discrR. Qed. Lemma minus_sum :  forall (An Bn:nat -> R) (N:nat),    sum_f_R0 (fun i:nat => An i - Bn i) N = sum_f_R0 An N - sum_f_R0 Bn N. intros; induction N as [| N HrecN]. simpl in |- *; ring. do 3 rewrite tech5; rewrite HrecN; ring. Qed. Lemma sum_decomposition :  forall (An:nat -> R) (N:nat),    sum_f_R0 (fun l:nat => An (2 * l)%nat) (S N) +    sum_f_R0 (fun l:nat => An (S (2 * l))) N = sum_f_R0 An (2 * S N). intros. induction N as [| N HrecN]. simpl in |- *; ring. rewrite tech5. rewrite (tech5 (fun l:nat => An (S (2 * l))) N). replace (2 * S (S N))%nat with (S (S (2 * S N))). rewrite (tech5 An (S (2 * S N))). rewrite (tech5 An (2 * S N)). rewrite <- HrecN. ring. apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR. ring. Qed. Lemma sum_Rle :  forall (An Bn:nat -> R) (N:nat),    (forall n:nat, (n <= N)%nat -> An n <= Bn n) ->    sum_f_R0 An N <= sum_f_R0 Bn N. intros. induction N as [| N HrecN]. simpl in |- *; apply H. apply le_n. do 2 rewrite tech5. apply Rle_trans with (sum_f_R0 An N + Bn (S N)). apply Rplus_le_compat_l. apply H. apply le_n. do 2 rewrite <- (Rplus_comm (Bn (S N))). apply Rplus_le_compat_l. apply HrecN. intros; apply H. apply le_trans with N; [ assumption | apply le_n_Sn ]. Qed. Lemma Rsum_abs :  forall (An:nat -> R) (N:nat),    Rabs (sum_f_R0 An N) <= sum_f_R0 (fun l:nat => Rabs (An l)) N. intros. induction N as [| N HrecN]. simpl in |- *. right; reflexivity. do 2 rewrite tech5. apply Rle_trans with (Rabs (sum_f_R0 An N) + Rabs (An (S N))). apply Rabs_triang. do 2 rewrite <- (Rplus_comm (Rabs (An (S N)))). apply Rplus_le_compat_l. apply HrecN. Qed. Lemma sum_cte :  forall (x:R) (N:nat), sum_f_R0 (fun _:nat => x) N = x * INR (S N). intros. induction N as [| N HrecN]. simpl in |- *; ring. rewrite tech5. rewrite HrecN; repeat rewrite S_INR; ring. Qed. Lemma sum_growing :  forall (An Bn:nat -> R) (N:nat),    (forall n:nat, An n <= Bn n) -> sum_f_R0 An N <= sum_f_R0 Bn N. intros. induction N as [| N HrecN]. simpl in |- *; apply H. do 2 rewrite tech5. apply Rle_trans with (sum_f_R0 An N + Bn (S N)). apply Rplus_le_compat_l; apply H. do 2 rewrite <- (Rplus_comm (Bn (S N))). apply Rplus_le_compat_l; apply HrecN. Qed. Lemma Rabs_triang_gen :  forall (An:nat -> R) (N:nat),    Rabs (sum_f_R0 An N) <= sum_f_R0 (fun i:nat => Rabs (An i)) N. intros. induction N as [| N HrecN]. simpl in |- *. right; reflexivity. do 2 rewrite tech5. apply Rle_trans with (Rabs (sum_f_R0 An N) + Rabs (An (S N))). apply Rabs_triang. do 2 rewrite <- (Rplus_comm (Rabs (An (S N)))). apply Rplus_le_compat_l; apply HrecN. Qed. Lemma cond_pos_sum :  forall (An:nat -> R) (N:nat),    (forall n:nat, 0 <= An n) -> 0 <= sum_f_R0 An N. intros. induction N as [| N HrecN]. simpl in |- *; apply H. rewrite tech5. apply Rplus_le_le_0_compat. apply HrecN. apply H. Qed. Definition Cauchy_crit_series (An:nat -> R) : Prop :=   Cauchy_crit (fun N:nat => sum_f_R0 An N). Lemma cauchy_abs :  forall An:nat -> R,    Cauchy_crit_series (fun i:nat => Rabs (An i)) -> Cauchy_crit_series An. unfold Cauchy_crit_series in |- *; unfold Cauchy_crit in |- *. intros. elim (H eps H0); intros. exists x. intros. cut  (R_dist (sum_f_R0 An n) (sum_f_R0 An m) <=   R_dist (sum_f_R0 (fun i:nat => Rabs (An i)) n)     (sum_f_R0 (fun i:nat => Rabs (An i)) m)). intro. apply Rle_lt_trans with  (R_dist (sum_f_R0 (fun i:nat => Rabs (An i)) n)     (sum_f_R0 (fun i:nat => Rabs (An i)) m)). assumption. apply H1; assumption. assert (H4:= lt_eq_lt_dec n m). elim H4; intro. elim a; intro. rewrite (tech2 An n m); [ idtac | assumption ]. rewrite (tech2 (fun i:nat => Rabs (An i)) n m); [ idtac | assumption ]. unfold R_dist in |- *. unfold Rminus in |- *. do 2 rewrite Ropp_plus_distr. do 2 rewrite <- Rplus_assoc. do 2 rewrite Rplus_opp_r. do 2 rewrite Rplus_0_l. do 2 rewrite Rabs_Ropp. rewrite  (Rabs_right (sum_f_R0 (fun i:nat => Rabs (An (S n + i)%nat)) (m - S n)))  . set (Bn:= fun i:nat => An (S n + i)%nat). replace (fun i:nat => Rabs (An (S n + i)%nat)) with  (fun i:nat => Rabs (Bn i)). apply Rabs_triang_gen. unfold Bn in |- *; reflexivity. apply Rle_ge. apply cond_pos_sum. intro; apply Rabs_pos. rewrite b. unfold R_dist in |- *. unfold Rminus in |- *; do 2 rewrite Rplus_opp_r. rewrite Rabs_R0; right; reflexivity. rewrite (tech2 An m n); [ idtac | assumption ]. rewrite (tech2 (fun i:nat => Rabs (An i)) m n); [ idtac | assumption ]. unfold R_dist in |- *. unfold Rminus in |- *. do 2 rewrite Rplus_assoc. rewrite (Rplus_comm (sum_f_R0 An m)). rewrite (Rplus_comm (sum_f_R0 (fun i:nat => Rabs (An i)) m)). do 2 rewrite Rplus_assoc. do 2 rewrite Rplus_opp_l. do 2 rewrite Rplus_0_r. rewrite  (Rabs_right (sum_f_R0 (fun i:nat => Rabs (An (S m + i)%nat)) (n - S m)))  . set (Bn:= fun i:nat => An (S m + i)%nat). replace (fun i:nat => Rabs (An (S m + i)%nat)) with  (fun i:nat => Rabs (Bn i)). apply Rabs_triang_gen. unfold Bn in |- *; reflexivity. apply Rle_ge. apply cond_pos_sum. intro; apply Rabs_pos. Qed. Lemma cv_cauchy_1 :  forall An:nat -> R,    sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l) ->    Cauchy_crit_series An. intros. elim X; intros. unfold Un_cv in p. unfold Cauchy_crit_series in |- *; unfold Cauchy_crit in |- *. intros. cut (0 < eps / 2). intro. elim (p (eps / 2) H0); intros. exists x0. intros. apply Rle_lt_trans with (R_dist (sum_f_R0 An n) x + R_dist (sum_f_R0 An m) x). unfold R_dist in |- *. replace (sum_f_R0 An n - sum_f_R0 An m) with  (sum_f_R0 An n - x + - (sum_f_R0 An m - x)); [ idtac | ring ]. rewrite <- (Rabs_Ropp (sum_f_R0 An m - x)). apply Rabs_triang. apply Rlt_le_trans with (eps / 2 + eps / 2). apply Rplus_lt_compat. apply H1; assumption. apply H1; assumption. right; symmetry in |- *; apply double_var. unfold Rdiv in |- *; apply Rmult_lt_0_compat;  [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. Qed. Lemma cv_cauchy_2 :  forall An:nat -> R,    Cauchy_crit_series An ->    sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l). intros. apply R_complete. unfold Cauchy_crit_series in H. exact H. Qed. Lemma sum_eq_R0 :  forall (An:nat -> R) (N:nat),    (forall n:nat, (n <= N)%nat -> An n = 0) -> sum_f_R0 An N = 0. intros; induction N as [| N HrecN]. simpl in |- *; apply H; apply le_n. rewrite tech5; rewrite HrecN;  [ rewrite Rplus_0_l; apply H; apply le_n  | intros; apply H; apply le_trans with N; [ assumption | apply le_n_Sn ] ]. Qed. Definition SP (fn:nat -> R -> R) (N:nat) (x:R) : R :=   sum_f_R0 (fun k:nat => fn k x) N. Lemma sum_incr :  forall (An:nat -> R) (N:nat) (l:R),    Un_cv (fun n:nat => sum_f_R0 An n) l ->    (forall n:nat, 0 <= An n) -> sum_f_R0 An N <= l. intros; case (total_order_T (sum_f_R0 An N) l); intro. elim s; intro. left; apply a. right; apply b. cut (Un_growing (fun n:nat => sum_f_R0 An n)). intro; set (l1:= sum_f_R0 An N). fold l1 in r. unfold Un_cv in H; cut (0 < l1 - l). intro; elim (H _ H2); intros. set (N0:= max x N); cut (N0 >= x)%nat. intro; assert (H5:= H3 N0 H4). cut (l1 <= sum_f_R0 An N0). intro; unfold R_dist in H5; rewrite Rabs_right in H5. cut (sum_f_R0 An N0 < l1). intro; elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H7 H6)). apply Rplus_lt_reg_r with (- l). do 2 rewrite (Rplus_comm (- l)). apply H5. apply Rle_ge; apply Rplus_le_reg_l with l. rewrite Rplus_0_r; replace (l + (sum_f_R0 An N0 - l)) with (sum_f_R0 An N0);  [ idtac | ring ]; apply Rle_trans with l1. left; apply r. apply H6. unfold l1 in |- *; apply Rge_le;  apply (growing_prop (fun k:nat => sum_f_R0 An k)). apply H1. unfold ge, N0 in |- *; apply le_max_r. unfold ge, N0 in |- *; apply le_max_l. apply Rplus_lt_reg_r with l; rewrite Rplus_0_r;  replace (l + (l1 - l)) with l1; [ apply r | ring ]. unfold Un_growing in |- *; intro; simpl in |- *;  pattern (sum_f_R0 An n) at 1 in |- *; rewrite <- Rplus_0_r;  apply Rplus_le_compat_l; apply H0. Qed. Lemma sum_cv_maj :  forall (An:nat -> R) (fn:nat -> R -> R) (x l1 l2:R),    Un_cv (fun n:nat => SP fn n x) l1 ->    Un_cv (fun n:nat => sum_f_R0 An n) l2 ->    (forall n:nat, Rabs (fn n x) <= An n) -> Rabs l1 <= l2. intros; case (total_order_T (Rabs l1) l2); intro. elim s; intro. left; apply a. right; apply b. cut (forall n0:nat, Rabs (SP fn n0 x) <= sum_f_R0 An n0). intro; cut (0 < (Rabs l1 - l2) / 2). intro; unfold Un_cv in H, H0. elim (H _ H3); intros Na H4. elim (H0 _ H3); intros Nb H5. set (N:= max Na Nb). unfold R_dist in H4, H5. cut (Rabs (sum_f_R0 An N - l2) < (Rabs l1 - l2) / 2). intro; cut (Rabs (Rabs l1 - Rabs (SP fn N x)) < (Rabs l1 - l2) / 2). intro; cut (sum_f_R0 An N < (Rabs l1 + l2) / 2). intro; cut ((Rabs l1 + l2) / 2 < Rabs (SP fn N x)). intro; cut (sum_f_R0 An N < Rabs (SP fn N x)). intro; assert (H11:= H2 N). elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H11 H10)). apply Rlt_trans with ((Rabs l1 + l2) / 2); assumption. case (Rcase_abs (Rabs l1 - Rabs (SP fn N x))); intro. apply Rlt_trans with (Rabs l1). apply Rmult_lt_reg_l with 2. prove_sup0. unfold Rdiv in |- *; rewrite (Rmult_comm 2); rewrite Rmult_assoc;  rewrite <- Rinv_l_sym. rewrite Rmult_1_r; rewrite double; apply Rplus_lt_compat_l; apply r. discrR. apply (Rminus_lt _ _ r0). rewrite (Rabs_right _ r0) in H7. apply Rplus_lt_reg_r with ((Rabs l1 - l2) / 2 - Rabs (SP fn N x)). replace ((Rabs l1 - l2) / 2 - Rabs (SP fn N x) + (Rabs l1 + l2) / 2) with  (Rabs l1 - Rabs (SP fn N x)). unfold Rminus in |- *; rewrite Rplus_assoc; rewrite Rplus_opp_l;  rewrite Rplus_0_r; apply H7. unfold Rdiv in |- *; rewrite Rmult_plus_distr_r;  rewrite <- (Rmult_comm (/ 2)); rewrite Rmult_minus_distr_l;  repeat rewrite (Rmult_comm (/ 2)); pattern (Rabs l1) at 1 in |- *;  rewrite double_var; unfold Rdiv in |- *; ring. case (Rcase_abs (sum_f_R0 An N - l2)); intro. apply Rlt_trans with l2. apply (Rminus_lt _ _ r0). apply Rmult_lt_reg_l with 2. prove_sup0. rewrite (double l2); unfold Rdiv in |- *; rewrite (Rmult_comm 2);  rewrite Rmult_assoc; rewrite <- Rinv_l_sym. rewrite Rmult_1_r; rewrite (Rplus_comm (Rabs l1)); apply Rplus_lt_compat_l;  apply r. discrR. rewrite (Rabs_right _ r0) in H6; apply Rplus_lt_reg_r with (- l2). replace (- l2 + (Rabs l1 + l2) / 2) with ((Rabs l1 - l2) / 2). rewrite Rplus_comm; apply H6. unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2));  rewrite Rmult_minus_distr_l; rewrite Rmult_plus_distr_r;  pattern l2 at 2 in |- *; rewrite double_var;  repeat rewrite (Rmult_comm (/ 2)); rewrite Ropp_plus_distr;  unfold Rdiv in |- *; ring. apply Rle_lt_trans with (Rabs (SP fn N x - l1)). rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr'; apply Rabs_triang_inv2. apply H4; unfold ge, N in |- *; apply le_max_l. apply H5; unfold ge, N in |- *; apply le_max_r. unfold Rdiv in |- *; apply Rmult_lt_0_compat. apply Rplus_lt_reg_r with l2. rewrite Rplus_0_r; replace (l2 + (Rabs l1 - l2)) with (Rabs l1);  [ apply r | ring ]. apply Rinv_0_lt_compat; prove_sup0. intros; induction n0 as [| n0 Hrecn0]. unfold SP in |- *; simpl in |- *; apply H1. unfold SP in |- *; simpl in |- *. apply Rle_trans with  (Rabs (sum_f_R0 (fun k:nat => fn k x) n0) + Rabs (fn (S n0) x)). apply Rabs_triang. apply Rle_trans with (sum_f_R0 An n0 + Rabs (fn (S n0) x)). do 2 rewrite <- (Rplus_comm (Rabs (fn (S n0) x))). apply Rplus_le_compat_l; apply Hrecn0. apply Rplus_le_compat_l; apply H1. Qed.```
Index