proposition: Lemma Cv_radius_weak_zip_l : forall An Bn (r : nonnegreal), Cv_radius_weak An r -> Cv_radius_weak Bn r -> Cv_radius_weak (Rseq_zip An Bn) (Rsqrt r).
proof: Proof. intros An Bn r [BAn HAn] [BBn HBn] ; exists (Rmax BAn (BBn * Rabs (Rsqrt r))) ; intros x [i Hi] ; subst. unfold gt_abs_pser, gt_pser, Rseq_abs, Rseq_zip, Rseq_mult. case (n_modulo_2 i) ; intros [p Hp] ; rewrite Hp. rewrite Rsqrt_pow_even ; transitivity BAn ; [apply HAn ; exists p ; reflexivity | apply RmaxLess1]. rewrite <- tech_pow_Rmult, Rsqrt_pow_even ; transitivity (Rabs (Bn p * r ^ p) * Rabs (Rsqrt r)). right ; rewrite <- Rabs_mult ; apply Rabs_eq_compat ; ring. transitivity (BBn * Rabs (Rsqrt r)). apply Rmult_le_compat_r ; [apply Rabs_pos | apply HBn ; exists p ; reflexivity]. apply RmaxLess2. Qed.
imports: Reals Rpser_def Rpser_def_simpl Rinterval Rsequence_def Rsequence_base_facts Rsequence_subsequence Rsequence_rewrite_facts Rsequence_cv_facts Rsequence_facts Rsequence_bound_facts Rsequence_sums_facts Rpow_facts PeanoNat Lra MyRIneq MyNat MyNNR