Library Coqtail.Subseq.Subseq


Require Export Reals.
Require Export Max.
Open Local Scope R_scope.

Definition strictly_increasing (f : natnat) := n: nat, (f n < f (S n)) %nat.

Definition of a sub-sequence
Definition sub_seq (An : natR) (f : natnat) (pr : strictly_increasing f) :=
    fun nAn (f n).

Lemma sincr_ge_id (f : natnat) : strictly_increasing f n : nat, (n f n )%nat.
Proof.
induction n.
omega.
apply le_trans with (S (f n)).
apply le_n_S.
apply IHn.
apply lt_le_S.
apply (H n).
Qed.

A sub-sequence of a convergent sequence converges to the same limit
Lemma Rsubseq_cv : (An : natR) (f : natnat) (pr : strictly_increasing f) (l : R),
    Un_cv An lUn_cv (sub_seq An f pr) l.
Proof.
unfold Un_cv.
intros An f pr l Hcv eps Heps.
destruct (Hcv eps Heps) as (N, HN).
N.
intros n Hn.
apply HN.
apply le_trans with n.
apply Hn.
apply sincr_ge_id.
apply pr.
Qed.

Lemma odd_or_even : n : nat, p : nat, (n = 2×p n = S (2×p)) %nat.
Proof.
intros.
induction n.
0%nat.
left.
trivial.
destruct IHn.
case H; intro.
x.
right.
rewrite H0.
reflexivity.
(S x).
left.
rewrite H0.
omega.
Qed.

a seqence converges if its odd and even subsequences converges to the same limit
Lemma even_odd_cv : (An : natR) (l : R),
    Un_cv (fun nAn ((2×n) %nat)) lUn_cv (fun nAn (S (2×n) %nat)) l
        Un_cv An l.
Proof.
unfold Un_cv.
intros An l Hcve Hcvo eps Heps.
destruct (Hcve eps Heps) as (Ne, He).
destruct (Hcvo eps Heps) as (No, Ho).
(max (2×Ne) (S (2×No))).
intros n Hn.
destruct (odd_or_even n) as (p, Hp).
destruct Hp.
rewrite H.
apply He.
apply le_double.
rewrite <- H.
apply le_trans with (max (2 × Ne) (S (2 × No) )).
apply le_max_l.
apply Hn.
rewrite H.
apply Ho.
apply le_double.
apply le_S_n.
rewrite <- H.
apply le_trans with (max (2 × Ne) (S (2 × No))).
apply le_max_r.
apply Hn.
Qed.

Lemma sub_seq_ub_compat : (An : natR) (f : natnat) (pr : strictly_increasing f),
    has_ub Anhas_ub (sub_seq An f pr).
Proof.
intros An f pr Hub.
destruct Hub as (m, Hm).
m.
intros x Hx.
destruct Hx as (n, Hn).
rewrite Hn.
apply Hm.
(f n).
reflexivity.
Qed.

Lemma sub_seq_lb_compat : (An : natR) (f : natnat) (pr : strictly_increasing f),
    has_lb Anhas_lb (sub_seq An f pr).
Proof.
intros An f pr Hlb.
destruct Hlb as (m, Hm).
m.
intros x Hx.
destruct Hx as (n, Hn).
rewrite Hn.
apply Hm.
(f n).
reflexivity.
Qed.