proposition: Lemma Alt_CVU : forall (f : nat -> R -> R) g h c r, (forall x, Boule c r x ->Un_decreasing (fun n => f n x)) -> (forall x, Boule c r x -> Un_cv (fun n => f n x) 0) -> (forall x, Boule c r x -> Un_cv (sum_f_R0 (tg_alt (fun i => f i x))) (g x)) -> (forall x n, Boule c r x -> f n x <= h n) -> (Un_cv h 0) -> CVU (fun N x => sum_f_R0 (tg_alt (fun i => f i x)) N) g c r.
proof: Proof. intros f g h c r decr to0 to_g bound bound0 eps ep. assert (ep' : 0 <eps/2) by lra. destruct (bound0 _ ep) as [N Pn]; exists N. intros n y nN dy. rewrite <- Rabs_Ropp, Ropp_minus_distr; apply Rle_lt_trans with (f n y). { solve[apply (Alt_first_term_bound (fun i => f i y) (g y) n n); auto]. } apply Rle_lt_trans with (h n). { apply bound; assumption. } clear - nN Pn. generalize (Pn _ nN); unfold Rdist; rewrite Rminus_0_r; intros t. apply Rabs_def2 in t; tauto. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia