proposition: Lemma finite_cv_radius_zip_compat_l : forall (An Bn : Rseq) (r : nonnegreal), finite_cv_radius An r -> (forall x, Rabs x < r -> Cv_radius_weak Bn x) -> 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 ; assumption. apply HBn ; rewrite Rabs_right ; try apply Rle_ge ; apply r'2_encad. assumption. reflexivity. intros r' r'_lb Hf ; apply (proj2 HAn (r' ^ 2)), Cv_radius_weak_zip_r1 with Bn. 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