# Library Coqtail.Reals.Rsequence.Rsequence_subsequence

Require Import Reals.
Require Import Rsequence_def.
Require Import Rsequence_facts.

Require Import Fourier.
Open Scope Rseq_scope.
Open Scope nat_scope.
Definition is_extractor (phi : natnat) := n, phi n < phi (S n).

Definition extractor := {phi | is_extractor phi}.

Definition extracted {X : Type} (phi : extractor) (Un : natX) n := Un ((proj1_sig phi) n).

Notation "Un ⋅ phi" := (extracted phi Un) (at level 40, left associativity) : Rseq_scope.

Definition subsequence {X : Type} (Un Vn : natX) :=
{phi | n, Un n = (Vn phi) n}.

Properties on nat -> nat sequences

Lemma nat_seq_growing_trans : an : natnat, ( x, an x an (S x)) →
y x, x yan x an y.
Proof.
induction y.
intros x Hx0; rewrite (le_n_O_eq x Hx0).
apply le_refl.

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

apply H.

subst; apply le_refl.
Qed.

Lemma nat_seq_strict_growing_trans : an, ( x, an x < an (S x)) →
y x, x < yan x < an y.
Proof.
induction y.
intros x Hx0. inversion Hx0.

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

rewrite <- Hyx.
apply H.
Qed.

Lemma nat_seq_growing_trans_converse : an, ( x, an x < an (S x)) →
x y, an x an yx y.
Proof.
intros an H x y Hxy.
destruct (le_le_S_dec x y).
assumption.

pose proof (nat_seq_strict_growing_trans an H x y).
intuition.
Qed.

Properties on extractors
Lemma Rsubseq_n_le_extractor_n : phi n, is_extractor phin phi n.
Proof.
intros phi n Hphi.
induction n.
apply le_O_n.

eapply le_trans with (S (phi n)).
apply (le_n_S _ _ IHn).
apply Hphi.
Qed.

Convergence compatible with subsequence
Lemma Rseq_subseq_cv_compat : Un Vn l, subsequence Un VnRseq_cv Vn lRseq_cv Un l.
Proof.
intros Un Vn l Hsub Hcv eps Heps.
destruct (Hcv eps Heps) as [N HN].
N; intros n Hn.
destruct Hsub as [phi Hphi].
unfold extracted in *; simpl in Hphi.
rewrite Hphi.
apply HN.
apply le_trans with n.
apply Hn.
apply Rsubseq_n_le_extractor_n; destruct phi; auto.
Qed.

Divergence compatible with subsequence
Lemma Rseq_subseq_cv_pos_infty_compat :
Un Vn, subsequence Un Vn
Rseq_cv_pos_infty VnRseq_cv_pos_infty Un.
Proof.
intros Un Vn Hsub Hdv M.
destruct (Hdv M) as [N HN].
N; intros n Hn.
destruct Hsub as [phi Hphi].
rewrite Hphi.
apply HN.
apply le_trans with n.
apply Hn.
apply Rsubseq_n_le_extractor_n; destruct phi; auto.
Qed.

An extractor defines a partition of N
Lemma Rseq_extractor_partition : phi, is_extractor phi
n, phi 0 n p, phi p n < phi (S p).
Proof.
intros phi ephi.
induction n.
0.
split.
assumption.
apply (Rsubseq_n_le_extractor_n _ 1 ephi).

destruct (le_le_S_dec (phi 0) n).
intros _.
destruct (IHn l) as [p [Hpn Hnsp]].
destruct (Compare.le_decide _ _ Hnsp).
p.
split; [constructor|]; assumption.

(S p).
rewrite e.
intuition.

intro l'; rewrite (le_antisym _ _ l l').
0.
split.
constructor.
apply ephi.
Qed.

Composition of extractors

Lemma extractor_comp : phi1 phi2,
is_extractor phi1is_extractor phi2is_extractor (fun nphi1 (phi2 n)).
Proof.
intros phi1 phi2 H1 H2 n.
apply nat_seq_strict_growing_trans; trivial.
Qed.

Common extractors
Definition Rseq_iter_S k := plus k.

Lemma extractor_S : is_extractor S.
Proof.
intro n.
constructor.
Qed.

Lemma extractor_Rseq_iter_S : k, is_extractor (Rseq_iter_S k).
Proof.
intros k n.
unfold Rseq_iter_S.
apply plus_lt_compat_l; constructor.
Qed.

Lemma is_extractor_mult_2 : is_extractor (mult 2).
Proof.
intros n; omega.
Qed.

Definition extractor_mult_2 := existT _ (mult 2) is_extractor_mult_2.

Rseq_zip can be inversed thanks to extractors

Lemma Rseq_zip_extract_evens : Un Vn,
Rseq_zip Un Vn extractor_mult_2 == Un.
Proof.
intros Un Vn n ; unfold Rseq_zip, extracted, extractor_mult_2 ;
simpl ; case (n_modulo_2 (n + (n + 0))) ; intros [p Hp].
f_equal ; omega.
apply False_ind ; omega.
Qed.

Convergence of subsequence implies convergence of the growing sequence
Open Scope R_scope.

Lemma Rseq_subseq_growing_cv_compat :
Un Vn l, subsequence Un VnRseq_cv Un lRseq_growing VnRseq_cv Vn l.
Proof.
intros un vn l [phi ephi] uncv vngrow eps epspos.
destruct phi as [phi Hphi]; unfold extracted in *; simpl in ×.
assert (spliteps : (eps / 3 > 0)%R) by fourier.
destruct (uncv (eps / 3) spliteps) as [Nu Hu].
(phi Nu).
intros n nNu.
destruct (Rseq_extractor_partition phi Hphi n) as [N Hpart].
apply le_trans with (phi Nu).
apply nat_seq_growing_trans.
intros x.
apply lt_le_weak.
apply Hphi.

apply le_O_n.

exact nNu.

assert (HNuN : (Nu N)%nat).
destruct (le_le_S_dec Nu N) as [goal|Hinv].
exact goal.

destruct Hpart as [HNn HnSN].
pose proof (nat_seq_growing_trans phi (fun xlt_le_weak _ _ (Hphi _)) Nu (S N) Hinv).
pose proof (le_trans _ _ _ H nNu).
pose proof (lt_le_trans _ _ _ HnSN H).
intuition.

pose proof (Hu N HNuN) as Hun.
pose proof (Hu (S N) (le_S _ _ HNuN)) as Husn.
rewrite ephi in Hun.
rewrite ephi in Husn.
assert (vn (phi N) vn n vn (phi (S N)))%R.
split; apply (Rseq_growing_trans _ vngrow); intuition.
rewrite R_dist_sym in Husn.
replace eps with (eps / 3 + eps / 3 + eps / 3) by field.
eapply Rle_lt_trans.
apply (R_dist_tri _ _ (vn (phi (S N)))).
apply Rplus_lt_compat.
eapply R_dist_bounded_in_segment.
apply H.
eapply Rle_lt_trans.
apply (R_dist_tri _ _ l).
apply Rplus_lt_compat.
apply Hun.
apply Husn.
rewrite R_dist_sym .
apply Husn.
Qed.

u(2n) → l and u growing implies u → l

Corollary Rseq_even_growing_compat : un l, Rseq_growing un
Rseq_cv (fun iun (2×i)%nat) lRseq_cv un l.
Proof.
intros.
apply Rseq_subseq_growing_cv_compat with (fun i : natun (2 × i)%nat).
assert (Hex : is_extractor (mult 2)).
intros n; omega.
pose (phi := exist _ (mult 2) Hex).
phi; reflexivity.
assumption.
assumption.
Qed.

Section Landau.

Variables Un Vn : natR.

Subsequence and big-O.
Lemma Rseq_big_O_subseq_compat :
phi, Un = O (Vn)(Un phi) = O(Vn phi).
Proof.
intros phi Heq.
destruct Heq as [N [HN [N0 HN0]]].
N; split.
assumption.
N0; intros n Hn.
apply HN0.
apply le_trans with n.
assumption.
apply Rsubseq_n_le_extractor_n; destruct phi; assumption.
Qed.

Subsequence and little-O.
Lemma Rseq_little_O_subseq_compat :
phi, Un = o (Vn)(Un phi) = o(Vn phi).
Proof.
intros [phi Hphi] Heq.
intros eps Heps.
destruct (Heq eps Heps) as [N HN].
N.
intros n Hn; unfold Rseq_minus.
apply HN.
apply le_trans with (phi N).
apply Rsubseq_n_le_extractor_n; assumption.
apply nat_seq_growing_trans; auto with ×.
Qed.

Subsequence and equivalence.
Lemma Rseq_equiv_subseq_compat :
phi, Un ¬ Vn(Un phi) ¬ (Vn phi).
Proof.
intros [phi Hphi] Heq.
intros eps Heps.
destruct (Heq eps Heps) as [N HN].
N.
intros n Hn; unfold Rseq_minus.
apply HN.
apply le_trans with (phi N).
apply Rsubseq_n_le_extractor_n; assumption.
apply nat_seq_growing_trans;auto with ×.
Qed.

End Landau.