proposition: Lemma finite_cv_radius_zip_compat_r : forall (An Bn : Rseq) (r : nonnegreal), (forall x, Rabs x < r -> Cv_radius_weak An x) -> finite_cv_radius Bn r -> finite_cv_radius (Rseq_zip An Bn) (Rsqrt r).
proof: Proof. intros An Bn r HAn HBn ; split. intros r' [r'_lb r'_ub] ; rewrite <- (Rsqrt_sqr r' (nnr_sqr r')). assert (r'2_encad : 0 <= nnr_sqr r' < r). split ; [apply cond_nonneg |]. simpl ; fold (r' ^ 2) ; rewrite <- Rsqr_Rsqrt ; apply pow_lt_compat ; auto. apply Cv_radius_weak_zip_l. apply HAn ; rewrite Rabs_right ; try apply Rle_ge ; apply r'2_encad. apply HBn ; assumption. assumption. reflexivity. intros r' r'_lb Hf ; apply (proj2 HBn (r' ^ 2)), Cv_radius_weak_zip_r2 with An. rewrite <- Rsqr_Rsqrt ; apply pow_lt_compat. apply Rsqrt_positivity. assumption. auto. assumption. 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