proposition: Lemma sum_cv_maj : forall (An : nat -> R) (fn : nat -> C -> C) (z l1 : C) (l2 : R), Cseq_cv (fun n : nat => CFpartial_sum (fun n => fn n z) n) l1 -> Rseq_cv (fun n : nat => sum_f_R0 An n) l2 -> (forall n : nat, Cnorm (fn n z) <= An n) -> Cnorm l1 <= l2.
proof: Proof. intros An fn z l1 l2 fn_cv An_cv fn_bd. destruct (Rle_lt_dec (Cnorm l1) l2) as [H | Hf]. assumption. pose (eps := ((Cnorm l1 - l2) / 4)%R) ; assert (eps_pos : 0 < eps). unfold eps, Rdiv ; apply Rlt_mult_inv_pos ; lra. destruct (fn_cv _ eps_pos) as [Nfn Hfn] ; destruct (An_cv _ eps_pos) as [NAn HAn]. pose (N := max Nfn NAn). assert (Main : Cnorm l1 - eps < l2 + eps). apply Rlt_trans with (Cnorm (CFpartial_sum (fun n : nat => fn n z) N)). apply Rlt_minus_exchange ; apply Rle_lt_trans with (Cnorm (CFpartial_sum (fun n : nat => fn n z) N - l1)) ; [apply Cnorm_triang_rev_r | apply Hfn ; apply Nat.le_max_l]. apply Rle_lt_trans with (Rabs (sum_f_R0 An N)). apply Rle_trans with (sum_f_R0 (fun n => Cnorm (fn n z)) N). unfold CFpartial_sum ; apply sum_f_C0_triang. clear - fn_bd ; induction N. simpl ; rewrite Rabs_right ; [| apply Rle_ge ; apply Rle_trans with (Cnorm (fn O z)) ; [apply Cnorm_pos |] ] ; apply fn_bd. simpl ; rewrite Rabs_right. apply Rle_trans with (Rplus (sum_f_R0 An N) (Cnorm (fn (S N) z))) ; [apply Rplus_le_compat_r ; rewrite <- Rabs_right ; [apply IHN |] | apply Rplus_le_compat_l ; apply fn_bd]. apply Rle_ge ; apply cond_pos_sum. intro n ; apply Rle_trans with (Cnorm (fn n z)) ; [apply Cnorm_pos | apply fn_bd]. rewrite <- tech5 ; apply Rle_ge ; apply cond_pos_sum. intro n ; apply Rle_trans with (Cnorm (fn n z)) ; [apply Cnorm_pos | apply fn_bd]. apply Rlt_plus_exchange. apply Rle_lt_trans with (R_dist (sum_f_R0 An N) l2). apply Rle_trans with (Rminus (Rabs (sum_f_R0 An N)) (Rabs l2)). replace (Rabs l2) with l2. right ; reflexivity. symmetry ; apply Rabs_right. apply Rle_ge ; apply Rseq_limit_comparison with (fun _ => R0) (fun n : nat => sum_f_R0 An n). intros n ; apply cond_pos_sum ; intro n' ; apply Rle_trans with (Cnorm (fn n' z)) ; [apply Cnorm_pos | apply fn_bd]. intros ; exists O ; intros ; simpl ; unfold R_dist . rewrite Rminus_0_r. change R0 with (IZR 0). rewrite Rabs_R0 ; assumption. assumption. unfold R_dist ; apply Rabs_triang_inv. apply HAn ; apply Nat.le_max_r. assert (Cnorm l1 < Cnorm l1). apply Rlt_trans with (l2 + 2 * eps)%R. lra. unfold eps. apply Rle_lt_trans with ((Cnorm l1 + l2) / 2)%R. right ; field. rewrite Rplus_comm ; apply (middle_is_in_the_middle _ _ Hf). elim (Rlt_irrefl _ H). Qed.
imports: Rsequence_def Rinterval Ranalysis_def Rsequence_cv_facts Rsequence_tactics MyRIneq Cfunctions Csequence Csequence_facts CFsequence Cnorm Cprop_base Ctacfield Lia Lra PeanoNat Cmet Canalysis_def Canalysis_deriv