proposition: Lemma AltSeries_small : forall x (p : positive), Str_alt_decr x -> Qabs (snd (CRstreams.iterate (X * Q * Q) (fun y : X * Q * Q => let (z, r0) := f (fst y) in (z, r0, r0 + snd y)) p (x, 0))) <= Qabs (snd (f x)).
proof: Proof. intros. destruct (Qlt_le_dec (snd (f x)) 0). - apply (Pos.peano_case (fun p => Qabs (snd (CRstreams.iterate (X * Q * Q) (fun y : X * Q * Q => let (z, r0) := f (fst y) in (z, r0, r0 + snd y)) p (x, 0))) <= Qabs (snd (f x)))). + simpl. destruct (f x). unfold snd. rewrite Qplus_0_r. apply Qle_refl. + assert (0 <= snd (f (f x))) as sndPos. { specialize (H xH) as [_ H]. unfold Str_pth in H. simpl in H. rewrite <- (Qmult_0_l (-snd (f x))) in H. setoid_replace (snd (f (f x)) * snd (f x))%Q with (-snd (f (f x)) * -snd (f x))%Q in H. apply Qmult_le_r in H. apply (Qopp_le_compat _ 0) in H. rewrite Qopp_involutive in H. exact H. apply (Qplus_lt_l _ _ (snd (f x))). ring_simplify. exact q. unfold equiv, Q_eq. simpl. ring. } intro n. rewrite <- Pos.add_1_l, SumStream_assoc, iterate_one. setoid_replace (snd (let (z, r0) := f (fst (x, 0)) in (z, r0, r0 + snd (x, 0)))) with (snd (f x)) by (simpl; destruct (f x); apply Qplus_0_r). rewrite Qabs_neg, Qabs_neg. apply Qopp_le_compat. rewrite <- (Qplus_0_r (snd (f x))) at 1. apply Qplus_le_r. apply AltSeries_small_pos. exact (Str_alt_decr_tl x _ H). exact sndPos. apply Qlt_le_weak, q. apply (Qle_trans _ (snd (f x) + snd (f (f x)))). apply Qplus_le_r. apply AltSeries_small_pos. exact (Str_alt_decr_tl x 1 H). exact sndPos. specialize (H xH) as [H _]. unfold Str_pth in H. simpl in H. rewrite (Qabs_pos _ sndPos) in H. rewrite Qabs_neg in H. apply (Qplus_le_r _ _ (snd (f x))) in H. rewrite Qplus_opp_r in H. exact H. apply Qlt_le_weak, q. - pose proof (AltSeries_small_pos x p H q). rewrite (Qabs_pos (snd (f x)) q). rewrite Qabs_pos. apply H0. apply H0. Qed.
imports: Coq.setoid_ring.ArithRing Coq.Bool.Bool Coq.QArith.Qpower Coq.QArith.Qabs CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRArith CoRN.model.metric2.Qmetric CoRN.reals.fast.LazyNat CoRN.reals.fast.CRstreams CoRN.metric2.Limit CoRN.model.totalorder.QposMinMax CoRN.classes.Qclasses MathClasses.interfaces.abstract_algebra