Require Export Reals.
Require Export Rsequence_def.
Require Export Rsequence_base_facts.
Require Export Rsequence_cv_facts.
Require Export Rsequence_rel_facts.
Require Export Rsequence_usual_facts.
Require Import Fourier.
Open Scope R_scope.
Open Scope Rseq_scope.

Lemma Rseq_growing_constructive_limit : ∀ (Un : nat → R), Rseq_growing Un → (∃ l, Rseq_cv Un l) → {l | Rseq_cv Un l}.
Proof.
intros Un Hg Hl.
assert (has_ub Un).
  destruct Hl as [l Hl]; ∃ l.
  intros x Hx; destruct Hx as [n Hn]; rewrite Hn.
  apply growing_ineq; assumption.
apply growing_cv; assumption.
Qed.

Lemma Rseq_cv_not_infty : ∀ (Un : nat → R), ¬ ((∃ l, Rseq_cv Un l) ∧ Rseq_cv_pos_infty Un).
Proof.
intros Un Hf.
destruct Hf as [[l Hl] Hinf].
unfold Rseq_cv in Hl.
unfold Rseq_cv_pos_infty in Hinf.
destruct (Hinf (l+1)%R) as [ N HN].
destruct (Hl 1) as [N0 HN0].
auto with ×.
apply Rlt_irrefl with (Un (Max.max N N0)).
apply Rlt_trans with (l+1)%R.
replace (Un (Max.max N N0)) with (l+(Un (Max.max N N0)-l))%R by ring.
apply Rplus_lt_compat_l.
apply Rle_lt_trans with (Rabs (Un (Max.max N N0) - l)).
apply RRle_abs.
apply HN0.
apply Max.le_max_r.
apply HN.
apply Max.le_max_l.
Qed.

Lemma Rseq_growing_trans : ∀ an, Rseq_growing an → ∀ y x:nat,
  (x ≤ y)%nat → (an x ≤ an y)%R.
Proof.
induction y.
 intros x Hxy; rewrite (le_n_O_eq x Hxy); intuition.

 intros x Hxy; destruct (Compare.le_decide _ _ Hxy) as [Hyx|Hyx].
  apply Rle_trans with (an y).
   apply IHy.
   apply gt_S_le.
   apply Hyx.

   apply H.

  subst; apply Rle_refl.
Qed.

Lemma Rseq_strictly_growing_trans : ∀ an, Rseq_strictly_growing an → ∀ y x:nat,
  (x < y)%nat → (an x < an y)%R.
Proof.
induction y.
 intros x Hx0. inversion Hx0.

 intros x Hxy.
 destruct (Compare.le_decide _ _ Hxy) as [Hyx|Hyx].
  apply Rlt_trans with (an y).
   apply IHy.
   apply gt_S_le.
   apply Hyx.

   apply H.

  rewrite <- Hyx. apply H.
Qed.

Lemma Rseq_cv_shift_compat : ∀ Un l, Rseq_cv (Rseq_shift Un) l → Rseq_cv Un l.
Proof.
intros Un l H eps epspos.
destruct (H eps epspos) as [N Hu].
∃ (S N); intros n nSN.
destruct n; [inversion nSN | ].
replace (Un (S n)) with (Rseq_shift Un n) by reflexivity.
intuition.
Qed.

Lemma Rseq_cv_pos_infty_shift_compat : ∀ Un, Rseq_cv_pos_infty (Rseq_shift Un) → Rseq_cv_pos_infty Un.
Proof.
intros Un H M.
destruct (H M) as [N Hu].
∃ (S N); intros n nSN.
destruct n; [inversion nSN | ].
replace (Un (S n)) with (Rseq_shift Un n) by reflexivity.
intuition.
Qed.

Lemma Rseq_cv_neg_infty_shift_compat : ∀ Un, Rseq_cv_neg_infty (Rseq_shift Un) → Rseq_cv_neg_infty Un.
Proof.
intros Un H M.
destruct (H M) as [N Hu].
∃ (S N); intros n nSN.
destruct n; [inversion nSN | ].
replace (Un (S n)) with (Rseq_shift Un n) by reflexivity.
intuition.
Qed.

Lemma Rseq_cv_shift_compat_reciprocal : ∀ Un l, Rseq_cv Un l → Rseq_cv (Rseq_shift Un) l.
Proof.
intros Un l H eps epspos.
destruct (H eps epspos) as [N Hu].
∃ N; intros n nSN.
unfold Rseq_shift.
apply Hu.
intuition.
Qed.

Lemma Rseq_cv_pos_infty_shift_compat_reciprocal : ∀ Un, Rseq_cv_pos_infty Un → Rseq_cv_pos_infty (Rseq_shift Un).
Proof.
intros Un H M.
destruct (H M) as [N Hu].
∃ N; intros n nSN.
unfold Rseq_shift.
apply Hu.
intuition.
Qed.

Lemma Rseq_cv_neg_infty_shift_compat_reciprocal : ∀ Un, Rseq_cv_neg_infty Un → Rseq_cv_neg_infty (Rseq_shift Un).
Proof.
intros Un H M.
destruct (H M) as [N Hu].
∃ N; intros n nSN.
unfold Rseq_shift.
apply Hu.
intuition.
Qed.

Lemma Rseq_cv_shifts_compat : ∀ N Un l, Rseq_cv (Rseq_shifts Un N) l → Rseq_cv Un l.
Proof.
intros N Un l H eps eps_pos.
destruct (H eps eps_pos) as [M HM].
∃ (N + M)%nat; intros n nSN.
assert (Hrew: (n = N + (n - N))%nat) by omega.
rewrite Hrew ; apply HM ; omega.
Qed.

Lemma Rseq_cv_shifts_compat_reciprocal : ∀ N Un l,
  Rseq_cv Un l → Rseq_cv (Rseq_shifts Un N) l.
Proof.
intros N Un l H eps eps_pos.
destruct (H eps eps_pos) as [M HM].
∃ (M - N)%nat; intros n nSN.
apply HM ; intuition.
Qed.

Lemma Rseq_cv_pos_infty_shifts_compat : ∀ Un N,
  Rseq_cv_pos_infty (Rseq_shifts Un N) → Rseq_cv_pos_infty Un.
Proof.
intros Un N H M.
destruct (H M) as [P HP].
∃ (N + P)%nat; intros n nSN.
assert (Hrew: (n = N + (n - N))%nat) by omega.
rewrite Hrew ; apply HP ; omega.
Qed.

Section Classical_facts.

Variables Un : nat → R.
Hypothesis NNPP : ∀ p : Prop, ¬ ¬ p → p.

Lemma Rseq_unbounded_growing :
    Rseq_growing Un → (¬ ∃ M, Rseq_bound_max Un M) → Rseq_cv_pos_infty Un.
Proof.
intros Hgr Hnmaj m.
apply NNPP; intro Hf; apply Hnmaj.
∃ m; intro n.
apply NNPP.
intro Hff.
apply Hf.
apply Rnot_le_lt in Hff.
∃ n.
intros p Hp.
apply Rlt_le_trans with (Un n); [ apply Hff | apply Rge_le].
apply growing_prop.
apply Hgr.
apply Hp.
Qed.

Lemma Rseq_unbounded_decreasing :
    Rseq_decreasing Un → (¬ ∃ M, Rseq_bound_min Un M) → Rseq_cv_neg_infty Un.
Proof.
intros Hgr Hnmin m.
apply NNPP; intro Hf; apply Hnmin.
∃ m; intro n.
apply NNPP.
intro Hff.
apply Hf.
apply Rnot_le_lt in Hff.
∃ n.
intros p Hp.
apply Rle_lt_trans with (Un n).
apply decreasing_prop.
apply Hgr.
apply Hp.
apply Hff.
Qed.

End Classical_facts.

Close Scope Rseq_scope.