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 : nat → nat) := ∀ n, phi n < phi (S n).
Definition extractor := {phi | is_extractor phi}.
Definition extracted {X : Type} (phi : extractor) (Un : nat → X) 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 : nat → X) :=
{phi | ∀ n, Un n = (Vn • phi) n}.
Properties on nat -> nat sequences
Lemma nat_seq_growing_trans : ∀ an : nat → nat, (∀ x, an x ≤ an (S x)) →
∀ y x, x ≤ y → an 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 < y → an 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 y → x ≤ 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 phi → n ≤ 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.
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 Vn → Rseq_cv Vn l → Rseq_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.
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 Vn → Rseq_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.
∀ Un Vn, subsequence Un Vn →
Rseq_cv_pos_infty Vn → Rseq_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.
∀ 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 phi1 → is_extractor phi2 → is_extractor (fun n ⇒ phi1 (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.
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 Vn → Rseq_cv Un l → Rseq_growing Vn → Rseq_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 x ⇒ lt_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.
Lemma Rseq_subseq_growing_cv_compat :
∀ Un Vn l, subsequence Un Vn → Rseq_cv Un l → Rseq_growing Vn → Rseq_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 x ⇒ lt_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 i ⇒ un (2×i)%nat) l → Rseq_cv un l.
Proof.
intros.
apply Rseq_subseq_growing_cv_compat with (fun i : nat ⇒ un (2 × i)%nat).
assert (Hex : is_extractor (mult 2)).
intros n; omega.
pose (phi := exist _ (mult 2) Hex).
∃ phi; reflexivity.
assumption.
assumption.
Qed.
Link with Landau's relations
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.
∀ 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.
∀ 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.
∀ 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.