# Library Coqtail.Reals.Rseries.Rseries_pos_facts

Require Import Rsequence Rsequence_stdlib.
Require Import Rseries_def Rseries_base_facts.

Local Open Scope Rseq_scope.

# Properties about positive term series

Lemma Rser_pos_growing: Un,
( n, 0 Un n) → Rseq_growing (Rseq_sum Un).
Proof.
intros Un Un_pos n ; transitivity (Rseq_sum Un n + 0)%R.
rewrite Rplus_0_r ; reflexivity.
apply Rplus_le_compat_l ; trivial.
Qed.

Lemma Rser_pos_strictly_growing: Un,
( n, 0 < Un n) → Rseq_strictly_growing (Rseq_sum Un).
Proof.
intros Un Un_pos n ; apply Rle_lt_trans with (Rseq_sum Un n + 0)%R.
rewrite Rplus_0_r ; reflexivity.
apply Rplus_lt_compat_l ; trivial.
Qed.

Positive term series convergence caracterization

Lemma Rser_pos_bound_cv : Un M,
( n, 0 Un n) → Rser_bound_max Un M{ l | Rser_cv Un l }.
Proof.
intros Un M Un_pos Hb ; destruct ub_to_lub with (Rseq_sum Un) as [l Hl].
eapply Rseq_bound_max_has_ub ; eassumption.
l ; try apply tech10; apply Un_cv_crit_lub ; [apply Rser_pos_growing |] ; assumption.
Qed.

Properties using classical logic

Section Classical_facts.

Variables Un Vn : natR.
Hypothesis Un_pos : n, 0 Un n.
Hypothesis NNPP : p : Prop, ¬ ¬ pp.
Hypothesis classic: P : Prop, P ¬ P.

Positive series are either convergent or go to infinity

Lemma Rser_pos_cv_dec : ( l, Rser_cv Un l) (Rser_cv_pos_infty Un).
Proof.
destruct (classic ( l, Rser_cv Un l)) as [yes | no].
left ; exact yes.
right ; apply Rseq_unbounded_growing.
apply NNPP.
apply Rser_pos_growing ; assumption.
intros [M HM] ; apply no ; destruct (Rser_pos_bound_cv _ _ Un_pos HM) as [l Hl] ;
l ; assumption.
Qed.

End Classical_facts.

If a gt-positive series converges on an extractor, then it converges

Lemma Rser_cv_growing_subseq_compat: (An : Rseq) (phi : extractor) l,
( n, 0 An n) → Rseq_cv ((Rseq_sum An) phi)%Rseq lRser_cv An l.
Proof.
intros An phi l A_pos Hcv ;
apply Rseq_subseq_growing_cv_compat with ((Rseq_sum An) phi).
phi ; trivial.
assumption.
intro ; transitivity (Rseq_sum An n + 0)%R.
rewrite Rplus_0_r ; reflexivity.
simpl ; apply Rplus_le_compat_l ; trivial.
Qed.

If a gt-positive series converges on even or odd integers, then it converges

Lemma Rser_cv_growing_even_compat: An l,
( n, 0 An n) → Rseq_cv (fun n ⇒ (Rseq_sum An (2×n))) l
Rser_cv An l.
Proof.
intros An l An_pos Hcv ; assert (Hex : is_extractor (mult 2)) by (intro n ; omega) ;
apply Rser_cv_growing_subseq_compat with (exist _ _ Hex) ; assumption.
Qed.

Lemma Rser_cv_growing_odd_compat: An l,
( n, 0 An n) → Rseq_cv (fun n ⇒ (Rseq_sum An (S (2×n)))) l
Rser_cv An l.
Proof.
intros An l An_pos Hcv ; assert (Hex : is_extractor (fun nS (2 × n))) by (intro n ; omega) ;
apply Rser_cv_growing_subseq_compat with (exist _ _ Hex) ; assumption.
Qed.