# Library Coqtail.Reals.Rsequence.Rsequence_base_facts

Require Import Rsequence_def.
Require Import Morphisms Setoid.
Require Import Fourier.

Open Scope R_scope.
Open Scope Rseq_scope.

# Extensional equality is an equivalence relation.

Lemma Rseq_eq_refl : Un, Un == Un.
Proof.
intros Un n; reflexivity.
Qed.

Lemma Rseq_eq_sym : Un Vn, Un == VnVn == Un.
Proof.
intros Un Vn Heq n.
symmetry; apply Heq.
Qed.

Lemma Rseq_eq_trans : Un Vn Wn, Un == VnVn == WnUn == Wn.
Proof.
intros Un Vn Wn Heq1 Heq2 n.
transitivity (Vn n); [apply Heq1|apply Heq2].
Qed.

Instance Rseq_eq_Equivalence : Equivalence Rseq_eq.
Proof.
split.
exact Rseq_eq_refl.
exact Rseq_eq_sym.
exact Rseq_eq_trans.
Qed.

# Rseq_opp is involutive.

Lemma Rseq_opp_invol : Un, - - Un == Un.
Proof.
intros Un n ; unfold Rseq_opp ; rewrite Ropp_involutive ;
reflexivity.
Qed.

# Compatibility of extensional equality with convergence.

Lemma Rseq_cv_eq_compat :
Un Vn l, Un == Vn
(Rseq_cv Un l Rseq_cv Vn l).
Proof.
intros Un Vn l Heq ; split ; intros Hcv eps Heps ;
destruct (Hcv eps Heps) as [N HN] ;
N; intros n Hn ;
[rewrite <- Heq | rewrite Heq] ;
apply HN; assumption.
Qed.

Lemma Rseq_cv_pos_infty_eq_compat :
Un Vn, Un == VnRseq_cv_pos_infty UnRseq_cv_pos_infty Vn.
Proof.
intros Un Vn Heq Hdiv.
intros m.
destruct (Hdiv m) as [N HN].
N; intros n Hn.
rewrite <- (Heq n).
apply HN; assumption.
Qed.

Lemma Rseq_cv_neg_infty_eq_compat :
Un Vn, Un == VnRseq_cv_neg_infty UnRseq_cv_neg_infty Vn.
Proof.
intros Un Vn Heq Hdiv.
intros m.
destruct (Hdiv m) as [N HN].
N; intros n Hn.
rewrite <- (Heq n).
apply HN; assumption.
Qed.

# Compatibility of extensional equality with Laudau relations.

Lemma Rseq_big_O_eq_compat :
Un Vn Wn Xn, Un == WnVn == Xn
Un = O(Vn)Wn = O(Xn).
Proof.
intros Un Vn Wn Xn Huw Hvx Huv.
destruct Huv as [M [HM [N HN]]].
M; split.
assumption.
N; intros n Hn.
rewrite <- Huw; rewrite <- Hvx.
apply HN; assumption.
Qed.

Lemma Rseq_little_O_eq_compat :
Un Vn Wn Xn, Un == WnVn == Xn
Un = o(Vn)Wn = o(Xn).
Proof.
intros Un Vn Wn Xn Huw Hvx Huv.
intros eps Heps.
destruct (Huv eps Heps) as [N HN].
N; intros n Hn.
rewrite <- Huw; rewrite <- Hvx.
apply HN; assumption.
Qed.

Lemma Rseq_equiv_eq_compat :
Un Vn Wn Xn, Un == WnVn == Xn
Un ¬ VnWn ¬ Xn.
Proof.
intros Un Vn Wn Xn Huw Hvx Huv.
intros eps Heps.
destruct(Huv eps Heps) as [N HN].
N; intros n Hn.
unfold Rseq_minus.
rewrite <- Huw; rewrite <- Hvx.
apply HN; apply Hn.
Qed.

## Boundedness and subsequences

Lemma even_odd_boundedness : (An : natR) (M1 M2 : R),
Rseq_bound (fun nAn (2 × n)%nat) M1
Rseq_bound (fun nAn (S (2 × n))) M2
Rseq_bound An (Rmax M1 M2).
Proof.
intros An M1 M2 HM1 HM2 n ; destruct (n_modulo_2 n) as [n_even | n_odd].
destruct n_even as [p Hp] ; rewrite Hp ; apply Rle_trans with M1 ; [apply HM1 | apply RmaxLess1].
destruct n_odd as [p Hp] ; rewrite Hp ; apply Rle_trans with M2 ; [apply HM2 | apply RmaxLess2].
Qed.

## Partial sequences.

Section Rseq_partial.

Variable Un : natR.

Lemma Rseq_partial_bound_max : N, M, n, (n N)%natUn n M.
Proof.
induction N.
(Un 0).
intros n Hn; inversion Hn as [H|H]; apply Rle_refl.
destruct IHN as [M IHN].
(Rmax M (Un (S N))).
intros n Hn.
destruct (le_lt_eq_dec n (S N)) as [He|He]; try assumption.
eapply Rle_trans; [apply IHN|apply RmaxLess1].
apply lt_n_Sm_le; assumption.
rewrite He; apply RmaxLess2.
Qed.

Lemma Rseq_partial_bound_min : N, m, n, (n N)%natm Un n.
Proof.
induction N.
(Un 0).
intros n Hn; inversion Hn as [H|H]; apply Rle_refl.
destruct IHN as [m IHN].
(Rmin m (Un (S N))).
intros n Hn.
destruct (le_lt_eq_dec n (S N)) as [He|He]; try assumption.
eapply Rle_trans; [apply Rmin_l|apply IHN].
apply lt_n_Sm_le; assumption.
rewrite He; apply Rmin_r.
Qed.

Lemma Rseq_partial_bound : N, M, n, (n N)%natRabs (Un n) M.
Proof.
intros N.
destruct (Rseq_partial_bound_max N) as [M HM].
destruct (Rseq_partial_bound_min N) as [m Hm].
(Rmax (Rabs m) (Rabs M)).
intros n Hn.
apply RmaxAbs; [apply Hm|apply HM]; assumption.
Qed.

End Rseq_partial.

## Asymptotic properties.

Definition Rseq_asymptotic P :=
(Q : RseqProp) Un,
( Vn, Q VnP Vn) → Rseq_eventually Q UnP Un.

Definition Rseq_asymptotic2 P :=
(Q : RseqRseqProp) Un Vn,
( Wn Xn, Q Wn XnP Wn Xn) → Rseq_eventually2 Q Un VnP Un Vn.

# Convergence is asymptotic.

Lemma Rseq_cv_asymptotic : l, Rseq_asymptotic (fun UnRseq_cv Un l).
Proof.
intros l Q Un HQ He eps Heps.
destruct He as [Ne HNe].
edestruct HQ as [N HN]; [eexact HNe|eexact Heps|].
(Ne + N)%nat; intros n Hn.
assert (Hn0 : n0, (n = Ne + n0)%nat).
induction Hn.
N; reflexivity.
destruct IHHn as [n0 H]; (S n0).
rewrite <- plus_Snm_nSm; simpl; rewrite H; reflexivity.
destruct Hn0 as [n0 Hn0].
rewrite Hn0; apply HN; omega.
Qed.

Lemma Rseq_cv_asymptotic_eq_compat : Un Vn l,
( N, n : nat, (N n)%natUn n = Vn n) → Rseq_cv Un lRseq_cv Vn l.
Proof.
intros Un Vn l [N HN] Hu eps Heps.
destruct (Hu eps Heps) as [N' HN'].
(N+N')%nat.
intros n Hn; unfold R_dist.
replace (Vn n -l)%R with ((Vn n - Un n) + (Un n -l))%R by ring.
apply Rle_lt_trans with (Rabs (Vn n - Un n)+ Rabs(Un n -l))%R.
apply Rabs_triang.
rewrite HN at 1.
unfold Rminus at 1.
rewrite Rplus_opp_r, Rabs_R0, Rplus_0_l.
apply HN'.
intuition.
intuition.
Qed.

Lemma Rseq_cv_pos_infty_asymptotic : Rseq_asymptotic Rseq_cv_pos_infty.
Proof.
intros Q Un HQ He M.
destruct He as [Ne HNe].
edestruct HQ as [N HN]; [eexact HNe|].
(Ne + N)%nat; intros n Hn.
assert (Hn0 : n0, (n = Ne + n0)%nat).
induction Hn.
N; reflexivity.
destruct IHHn as [n0 H]; (S n0).
rewrite <- plus_Snm_nSm; simpl; rewrite H; reflexivity.
destruct Hn0 as [n0 Hn0].
rewrite Hn0; apply HN; omega.
Qed.

Lemma Rseq_cv_neg_infty_asymptotic : Rseq_asymptotic Rseq_cv_neg_infty.
Proof.
intros Q Un HQ He M.
destruct He as [Ne HNe].
edestruct HQ as [N HN]; [eexact HNe|].
(Ne + N)%nat; intros n Hn.
assert (Hn0 : n0, (n = Ne + n0)%nat).
induction Hn.
N; reflexivity.
destruct IHHn as [n0 H]; (S n0).
rewrite <- plus_Snm_nSm; simpl; rewrite H; reflexivity.
destruct Hn0 as [n0 Hn0].
rewrite Hn0; apply HN; omega.
Qed.

# Landau relations are asymptotic.

Lemma Rseq_big_O_asymptotic : Rseq_asymptotic2 Rseq_big_O.
Proof.
intros Q Un Vn HQ He.
destruct He as [Ne HNe].
edestruct HQ as [M [HM [N HN]]]; [eexact HNe|].
M; split.
assumption.
(Ne + N)%nat; intros n Hn.
assert (Hn0 : n0, (n = Ne + n0)%nat).
induction Hn.
N; reflexivity.
destruct IHHn as [n0 H]; (S n0).
rewrite <- plus_Snm_nSm; simpl; rewrite H; reflexivity.
destruct Hn0 as [n0 Hn0].
rewrite Hn0; apply HN; omega.
Qed.

Lemma Rseq_little_O_asymptotic : Rseq_asymptotic2 Rseq_little_O.
Proof.
intros Q Un Vn HQ He.
destruct He as [Ne HNe].
intros eps Heps.
edestruct HQ as [N HN]; [eexact HNe|apply Heps|].
(Ne + N)%nat; intros n Hn.
assert (Hn0 : n0, (n = Ne + n0)%nat).
induction Hn.
N; reflexivity.
destruct IHHn as [n0 H]; (S n0).
rewrite <- plus_Snm_nSm; simpl; rewrite H; reflexivity.
destruct Hn0 as [n0 Hn0].
rewrite Hn0; apply HN; omega.
Qed.

Lemma Rseq_equiv_asymptotic : Rseq_asymptotic2 Rseq_equiv.
Proof.
intros Q Un Vn HQ He.
destruct He as [Ne HNe].
intros eps Heps.
edestruct HQ as [N HN]; [eexact HNe|apply Heps|].
(Ne + N)%nat; intros n Hn.
assert (Hn0 : n0, (n = Ne + n0)%nat).
induction Hn.
N; reflexivity.
destruct IHHn as [n0 H]; (S n0).
rewrite <- plus_Snm_nSm; simpl; rewrite H; reflexivity.
destruct Hn0 as [n0 Hn0].
unfold Rseq_minus in HN.
rewrite Hn0; apply HN; omega.
Qed.