proposition: Lemma Cv_radius_weak_prod_compat: forall (An Bn : Rseq) (r1 r2 : R), Cv_radius_weak An r1 -> Cv_radius_weak Bn r2 -> forall r, Rabs r < Rmin (Rabs r1) (Rabs r2) -> Cv_radius_weak (An # Bn) r.
proof: Proof. intros An Bn r1 r2 rAn rBn r Hr. apply Cv_radius_weak_ext with (An_deriv (fun n => if eq_nat_dec n 0 then 0 else (Rseq_div (An # Bn) (Rseq_shift INR)) (pred n))). unfold An_deriv, Rseq_shift, Rseq_mult, Rseq_div, Rdiv ; intro n ; simpl. rewrite <- Rmult_assoc, Rmult_comm, <- Rmult_assoc, Rinv_l, Rmult_1_l. reflexivity. apply Rgt_not_eq ; unfold Rgt ; replace (match n with | 0%nat => 1 | S _ => INR n + 1 end) with (INR (S n)) by auto ; apply lt_0_INR ; lia. apply Cv_radius_weak_derivable_compat with (Rmin (Rabs r1) (Rabs r2)). destruct (Cv_radius_weak_prod_prelim An Bn r1 r2 rAn rBn) as [B HB] ; exists (B * Rabs (Rmin (Rabs r1) (Rabs r2))) ; intros x [i Hi] ; subst ; unfold gt_abs_pser, Rseq_abs, gt_pser, Rseq_mult ; destruct i as [| j]. simpl ; rewrite Rmult_1_r, Rabs_R0 ; apply Rle_trans with ((gt_abs_pser ((An # Bn) / Rseq_shift INR)) (Rmin (Rabs r1) (Rabs r2)) O * Rabs (Rmin (Rabs r1) (Rabs r2))). apply Rmult_le_pos ; [unfold gt_abs_pser, Rseq_abs|] ; apply Rabs_pos. apply Rmult_le_compat_r ; [apply Rabs_pos | apply HB ; exists O ; reflexivity]. simpl. rewrite (Rmult_comm (Rmin (Rabs r1) (Rabs r2))), <- Rmult_assoc, Rabs_mult, (Rabs_pos_eq (Rmin (Rabs r1) (Rabs r2))). apply Rmult_le_compat_r. apply MyRIneq.Rmin_pos ; apply Rabs_pos. apply HB ; exists j ; reflexivity. apply MyRIneq.Rmin_pos ; apply Rabs_pos. rewrite (Rabs_pos_eq (Rmin (Rabs r1) (Rabs r2))) ; [assumption | apply MyRIneq.Rmin_pos ; apply Rabs_pos]. Qed.
imports: Reals Fourier Lra Rpow_facts Rinterval Rextensionality Rsequence_facts Rsequence_sums_facts Rsequence_rewrite_facts RFsequence RFsequence_facts Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_cv_facts Rpser_sums MyINR