# 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.

Lemma Rseq_eq_refl : ∀ Un, Un == Un.

Proof.

intros Un n; reflexivity.

Qed.

Lemma Rseq_eq_sym : ∀ Un Vn, Un == Vn → Vn == Un.

Proof.

intros Un Vn Heq n.

symmetry; apply Heq.

Qed.

Lemma Rseq_eq_trans : ∀ Un Vn Wn, Un == Vn → Vn == Wn → Un == 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.

Proof.

intros Un n; reflexivity.

Qed.

Lemma Rseq_eq_sym : ∀ Un Vn, Un == Vn → Vn == Un.

Proof.

intros Un Vn Heq n.

symmetry; apply Heq.

Qed.

Lemma Rseq_eq_trans : ∀ Un Vn Wn, Un == Vn → Vn == Wn → Un == 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.

Lemma Rseq_opp_invol : ∀ Un, - - Un == Un.

Proof.

intros Un n ; unfold Rseq_opp ; rewrite Ropp_involutive ;

reflexivity.

Qed.

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 == Vn → Rseq_cv_pos_infty Un → Rseq_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 == Vn → Rseq_cv_neg_infty Un → Rseq_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.

∀ 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 == Vn → Rseq_cv_pos_infty Un → Rseq_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 == Vn → Rseq_cv_neg_infty Un → Rseq_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.

Lemma Rseq_big_O_eq_compat :

∀ Un Vn Wn Xn, Un == Wn → Vn == 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 == Wn → Vn == 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 == Wn → Vn == Xn →

Un ¬ Vn → Wn ¬ 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.

∀ Un Vn Wn Xn, Un == Wn → Vn == 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 == Wn → Vn == 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 == Wn → Vn == Xn →

Un ¬ Vn → Wn ¬ 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.

Lemma even_odd_boundedness : ∀ (An : nat → R) (M1 M2 : R),

Rseq_bound (fun n ⇒ An (2 × n)%nat) M1 →

Rseq_bound (fun n ⇒ An (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.

Section Rseq_partial.

Variable Un : nat → R.

Lemma Rseq_partial_bound_max : ∀ N, ∃ M, ∀ n, (n ≤ N)%nat → Un 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)%nat → m ≤ 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)%nat → Rabs (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.

Definition Rseq_asymptotic P :=

∀ (Q : Rseq → Prop) Un,

(∀ Vn, Q Vn → P Vn) → Rseq_eventually Q Un → P Un.

Definition Rseq_asymptotic2 P :=

∀ (Q : Rseq → Rseq → Prop) Un Vn,

(∀ Wn Xn, Q Wn Xn → P Wn Xn) → Rseq_eventually2 Q Un Vn → P Un Vn.

∀ (Q : Rseq → Prop) Un,

(∀ Vn, Q Vn → P Vn) → Rseq_eventually Q Un → P Un.

Definition Rseq_asymptotic2 P :=

∀ (Q : Rseq → Rseq → Prop) Un Vn,

(∀ Wn Xn, Q Wn Xn → P Wn Xn) → Rseq_eventually2 Q Un Vn → P Un Vn.

Lemma Rseq_cv_asymptotic : ∀ l, Rseq_asymptotic (fun Un ⇒ Rseq_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)%nat → Un n = Vn n) → Rseq_cv Un l → Rseq_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.

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)%nat → Un n = Vn n) → Rseq_cv Un l → Rseq_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.

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.

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.