# Library Coqtail.Complex.Csequence_facts

Require Import MyReals.
Require Import Max.
Require Import Rsequence_def.
Require Import Rsequence_facts.
Require Import Rsequence_base_facts.
Require Import Fourier.
Require Import Complex.
Require Import Csequence_def.

Open Scope C_scope.
Open Scope Cseq_scope.

Section Cseq_partial.

Variable Un : Cseq.

Lemma Cseq_partial_bound : N, M, n,
(n N)%natCnorm (Un n) M.
Proof.
intros N.
destruct (Rseq_partial_bound_max (fun nCnorm (Un n)) N) as (M, HM) ;
M ; apply HM.
Qed.

End Cseq_partial.

# Asymptotic properties.

Section Cseq_asymptotic.

Definition Cseq_asymptotic P :=
(Q : CseqProp) Un,
( Vn, Q VnP Vn) → Cseq_eventually Q UnP Un.

Definition Cseq_asymptotic2 P :=
(Q : CseqCseqProp) Un Vn,
( Wn Xn, Q Wn XnP Wn Xn) → Cseq_eventually2 Q Un VnP Un Vn.

Convergence is asymptotic.
Lemma Cseq_cv_asymptotic : l, Cseq_asymptotic (fun UnCseq_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.

End Cseq_asymptotic.

# Convergence compatibilities

Section Cseq_cv_R_to_C.

Variable Un : Cseq.
Variable lu : C.

Lemma Cseq_Rseq_Rseq_equiv : Cseq_cv Un lu
(Rseq_cv (fun nCre (Un n)) (Cre lu) Rseq_cv (fun nCim (Un n)) (Cim lu)).
Proof.
split ; intro H.
split ; intros eps eps_pos.
destruct (H _ eps_pos) as [N HN] ; N ; intros n Hn.
unfold R_dist ; rewrite Cre_minus_compat.
assert (Hrew := Cadd_conj (Un n - lu)).
assert (HN_conj : n : nat, (n N)%natCnorm (Cconj (Un n - lu)) < eps).
intros ; rewrite Cnorm_conj_compat ; apply HN ; assumption.
apply Rle_lt_trans with (Rabs (2 / 2 × Cre (Un n - lu))).
right ; apply Rabs_eq_compat ; field.
replace (2 / 2 × Cre (Un n - lu))%R with (/2 × (2 × Cre (Un n - lu)))%R by field.
replace (2 × Cre (Un n - lu))%R with (Cre (Un n - lu + Cconj (Un n - lu)))%R.
rewrite Rabs_mult ; rewrite Rabs_right by fourier ; apply Rlt_le_trans with
(/2 × (2 × eps))%R.
apply Rmult_lt_compat_l ; [fourier |] ; apply Rle_lt_trans with
(Rabs (Cre (Un n - lu)) + Rabs (Cre (Cconj (Un n - lu))))%R.
rewrite <- Cre_add_compat ; apply Rabs_triang.
apply Rle_lt_trans with (Cnorm (Un n - lu) + Rabs (Cre (Cconj (Un n - lu))))%R.
apply Rplus_le_compat_r ; apply Cre_le_Cnorm.
apply Rle_lt_trans with (Cnorm (Un n - lu) + Cnorm (Cconj (Un n - lu)))%R.
apply Rplus_le_compat_l ; apply Cre_le_Cnorm.
apply Rlt_trans with (eps + Cnorm (Cconj (Un n - lu)))%R.
apply Rplus_lt_compat_r ; apply HN ; assumption.
replace (2 × eps)%R with (eps + eps)%R by field ; apply Rplus_lt_compat_l ;
apply HN_conj ; assumption.
right ; field.
rewrite Hrew ; simpl ; replace ((0 + 0) × 0)%R with 0%R.
rewrite Rminus_0_r ; reflexivity.
field.
destruct (H _ eps_pos) as [N HN] ; N ; intros n Hn.
unfold R_dist ; rewrite Cim_minus_compat.
assert (Hrew := Cminus_conj (Un n - lu)).
assert (HN_conj : n : nat, (n N)%natCnorm (Cconj (Un n - lu)) < eps).
intros ; rewrite Cnorm_conj_compat ; apply HN ; assumption.
apply Rle_lt_trans with (Rabs (2 / 2 × Cim (Un n - lu))).
right ; apply Rabs_eq_compat ; field.
replace (2 / 2 × Cim (Un n - lu))%R with (/2 × (2 × Cim (Un n - lu)))%R by field.
replace (2 × Cim (Un n - lu))%R with (Cim (Un n - lu - Cconj (Un n - lu)))%R.
rewrite Rabs_mult ; rewrite Rabs_right by fourier ; apply Rlt_le_trans with
(/2 × (2 × eps))%R.
apply Rmult_lt_compat_l ; [fourier |] ; apply Rle_lt_trans with
(Rabs (Cim (Un n - lu)) + Rabs (- Cim (Cconj (Un n - lu))))%R.
rewrite <- Cim_minus_compat ; unfold Rminus ; apply Rabs_triang.
apply Rle_lt_trans with (Cnorm (Un n - lu) + Rabs (Cim (Cconj (Un n - lu))))%R.
rewrite Rabs_Ropp ; apply Rplus_le_compat_r ; apply Cim_le_Cnorm.
apply Rle_lt_trans with (Cnorm (Un n - lu) + Cnorm (Cconj (Un n - lu)))%R.
apply Rplus_le_compat_l ; apply Cim_le_Cnorm.
apply Rlt_trans with (eps + Cnorm (Cconj (Un n - lu)))%R.
apply Rplus_lt_compat_r ; apply HN ; assumption.
replace (2 × eps)%R with (eps + eps)%R by field ; apply Rplus_lt_compat_l ;
apply HN_conj ; assumption.
right ; field.
rewrite Hrew ; simpl ; replace ((0 + 0) × 0)%R with 0%R.
rewrite Rplus_0_r ; reflexivity.
field.
destruct H as [Hre Him] ; intros eps eps_pos ;
assert (eps_2_pos : 0 < eps/2) by fourier ; destruct (Hre _ eps_2_pos) as (N1, HN1) ;
destruct (Him _ eps_2_pos) as (N2, HN2) ; (max N1 N2) ; intros n Hn.
apply Rle_lt_trans with (Rabs (Cre (Un n - lu)) + Rabs (Cim (Un n - lu)))%R.
apply Cnorm_le_Cre_Cim.
unfold R_dist in × ; apply Rlt_trans with (Rabs (Cre (Un n - lu)) + eps/2)%R.
apply Rplus_lt_compat_l ; rewrite <- Cim_minus_compat ; apply HN2.
apply le_trans with (max N1 N2)%nat.
apply le_max_r.
assumption.
apply Rlt_le_trans with (eps/2 + eps/2)%R.
apply Rplus_lt_compat_r ; rewrite <- Cre_minus_compat ; apply HN1.
apply le_trans with (max N1 N2)%nat.
apply le_max_l.
assumption.
right ; field.
Qed.

Lemma Cauchy_equiv : Cauchy_crit Un
(Rseries.Cauchy_crit (fun nCre (Un n)) Rseries.Cauchy_crit (fun nCim (Un n)))%R.
Proof.
split.
intro Un_cauchy ; split ; intros eps eps_pos ;
destruct (Un_cauchy eps eps_pos) as [N HN] ;
N ; intros m n m_lb n_lb.
apply Rle_lt_trans with (Cnorm (Cre (Un m - Un n))%C)%R ;
[right |].
unfold R_dist ; rewrite Cnorm_IRC_Rabs ; apply Rabs_eq_compat ;
apply Cre_minus_compat.
rewrite Cnorm_IRC_Rabs ; apply Rle_lt_trans with (Cnorm (Un m - Un n))%R ;
[apply Cre_le_Cnorm | apply HN] ; assumption.
apply Rle_lt_trans with (Cnorm (Cim (Un m - Un n))%C)%R ;
[right |].
unfold R_dist ; rewrite Cnorm_IRC_Rabs ; apply Rabs_eq_compat ;
apply Cim_minus_compat.
rewrite Cnorm_IRC_Rabs ; apply Rle_lt_trans with (Cnorm (Un m - Un n))%R ;
[apply Cim_le_Cnorm | apply HN] ; assumption.
intros [Cre_cauchy Cim_cauchy] ; intros eps eps_pos ;
assert (eps_2_pos : 0 < eps / 2) by fourier ;
destruct (Cre_cauchy (eps / 2)%R eps_2_pos) as [N1 HN1] ;
destruct (Cim_cauchy (eps / 2)%R eps_2_pos) as [N2 HN2] ;
unfold R_dist in × ; (max N1 N2) ; intros m n m_ub n_ub.
apply Rle_lt_trans with (Rabs (Cre (Un m - Un n)) + Rabs (Cim (Un m - Un n)))%R ;
[apply Cnorm_le_Cre_Cim | apply Rlt_le_trans with (eps / 2 + eps / 2)%R ;
[| right ; field]].
apply Rlt_trans with (Rabs (Cre (Un m - Un n)) + eps / 2)%R.
apply Rplus_lt_compat_l ; rewrite <- Cim_minus_compat ; apply HN2 ;
apply le_trans with (max N1 N2) ; [apply le_max_r | assumption |
apply le_max_r | assumption].
apply Rplus_lt_compat_r.
rewrite <- Cre_minus_compat ; apply HN1 ;
apply le_trans with (max N1 N2) ; [apply le_max_l | assumption |
apply le_max_l | assumption].
Qed.

End Cseq_cv_R_to_C.

Section Cseq_cv_simpl.

Variable Un Vn : Cseq.
Variable lu lv : C.
Hypothesis Hu : Cseq_cv Un lu.
Hypothesis Hv : Cseq_cv Vn lv.

Lemma Cseq_cv_bound : M, 0 < M Cseq_bound Un M.
Proof.
destruct (Hu 1%R) as [N HN]; [fourier|].
destruct (Cseq_partial_bound Un N) as [M HM].
(Rmax (1 + (Cnorm lu)) M).
split.
eapply Rlt_le_trans; [|apply RmaxLess1].
apply Rplus_lt_le_0_compat; [fourier|apply Cnorm_pos].
intros n.
destruct (le_ge_dec n N) as [He|He].
eapply Rle_trans; [apply HM; assumption|apply RmaxLess2].
eapply Rle_trans; [|apply RmaxLess1].
replace (Un n) with ((Un n - lu) + lu)%C by field.
eapply Rle_trans; [apply Cnorm_triang|].
apply Rplus_le_compat.
left; apply HN; assumption.
apply Rle_refl.
Qed.

Lemma Cseq_cv_eq_compat : l,
( n, Un n = Vn n) → Cseq_cv Un lCseq_cv Vn l.
Proof.
intros l H Hl eps Heps.
destruct (Hl eps Heps) as [N HN]; N;
intros n Hn; rewrite <- H; apply HN; apply Hn.
Qed.

Lemma Cseq_cst_cv : (c : C), Cseq_cv (fun _c) c.
intros c eps Heps; O; intros n Hn.
unfold R_dist.
assert (c - c = 0)%C.
ring.
rewrite H.
rewrite Cnorm_C0; apply Heps.
Qed.

Lemma Cseq_cv_cnorm_compat : Rseq_cv (fun kCnorm (Un k)) (Cnorm lu).
Proof.
intros eps Heps ; destruct (Hu eps Heps) as [N HN].
N.
intros n Hn.
unfold R_dist.
apply Rle_lt_trans with (Cnorm (Un n - lu)).
apply Cnorm_triang_rev.
apply HN; apply Hn.
Qed.

Lemma Cseq_cv_add_compat : Cseq_cv (Un + Vn) (lu + lv).
Proof.
intros eps Heps.
destruct (Hu (eps/2)%R) as [Nu HNu]; [fourier|].
destruct (Hv (eps/2)%R) as [Nv HNv]; [fourier|].
(Max.max Nu Nv).
intros n Hn.
replace (Un n + Vn n - (lu + lv))%C
with ((Un n - lu) + (Vn n - lv))%C by field.
eapply Rle_lt_trans; [apply Cnorm_triang|].
replace eps with (eps/2 + eps/2)%R by field.
apply Rplus_lt_compat.
apply (HNu n); eapply le_trans; [apply Max.le_max_l|eexact Hn].
apply (HNv n); eapply le_trans; [apply Max.le_max_r|eexact Hn].
Qed.

Lemma Cseq_cv_opp_compat : Cseq_cv (- Un) (- lu).
Proof.
intros eps Heps.
destruct (Hu eps) as [Nu HNu]; [assumption|].
Nu; intros n Hn.
unfold R_dist; unfold Cseq_opp.
replace (- Un n - - lu)%C with (- (Un n - lu))%C by field.
rewrite Cnorm_opp.
apply HNu; exact Hn.
Qed.

End Cseq_cv_simpl.

Section Cseq_cv.

Variable Un Vn : natC.
Variable lu lv : C.
Hypothesis Hu : Cseq_cv Un lu.
Hypothesis Hv : Cseq_cv Vn lv.

Lemma Cseq_cv_minus_compat : Cseq_cv (Un - Vn) (lu - lv).
Proof.
apply Cseq_cv_eq_compat with (Un + (-Vn)).
reflexivity.
apply Hu.
apply Cseq_cv_opp_compat.
apply Hv.
Qed.

Lemma Cseq_cv_mult_compat : Cseq_cv (Un × Vn) (lu × lv).
Proof.
intros eps Heps.
destruct Cseq_cv_bound with Un lu%C as [Mb [HMb Hb]] ; [assumption |].
pose (eps1 := (eps / 2 / (Rmax 1 (Cnorm lv)))%R).
pose (eps2 := (eps / 2 / Mb)%R).
assert (Heps1 : eps1 > 0).
unfold eps1; repeat apply Rmult_gt_0_compat; try fourier.
apply Rinv_0_lt_compat; eapply Rlt_le_trans; [apply Rlt_0_1|apply RmaxLess1].
assert (Heps2 : eps2 > 0).
unfold eps2; repeat apply Rmult_gt_0_compat; try fourier.
apply Rinv_0_lt_compat; assumption.
destruct (Hu eps1) as [Nu HNu]; [assumption|].
destruct (Hv eps2) as [Nv HNv]; [assumption|].
(Max.max Nu Nv); intros n Hn.
unfold R_dist; unfold Cseq_mult.
replace (Un n × Vn n - lu × lv)%C
with ((Un n × Vn n - Un n × lv) + (Un n × lv - lu × lv))%C by field.
eapply Rle_lt_trans; [apply Cnorm_triang|].
replace eps with (eps / 2 + eps / 2)%R by field.
apply Rplus_lt_compat.
rewrite <- Cmult_minus_distr_l ; rewrite Cnorm_Cmult.
eapply Rle_lt_trans.
apply Rmult_le_compat_r; [apply Cnorm_pos|].
apply Hb.
replace (eps / 2)%R with (Mb × (eps / 2 / Mb))%R
by (field; apply Rgt_not_eq; assumption).
apply Rmult_lt_compat_l; [assumption|].
apply HNv; eapply le_trans; [apply Max.le_max_r|eexact Hn].
unfold Cminus ; rewrite <- Copp_mult_distr_l_reverse.
rewrite Cnorm_Cmult.
destruct (Ceq_dec lv C0) as [Hlv|Hlv].
rewrite Hlv ; rewrite Cnorm_C0 ; rewrite Rmult_0_r; fourier.
eapply Rlt_le_trans.
apply Rmult_lt_compat_r; [apply Cnorm_pos_lt; assumption|].
apply HNu; eapply le_trans; [apply Max.le_max_l|eexact Hn].
unfold eps1.
unfold Rdiv; rewrite Rmult_assoc; rewrite <- Rmult_1_r.
apply Rmult_le_compat_l; [fourier|].
assert (Hmax : Rmax 1 (Cnorm lv) > 0%R).
eapply Rlt_le_trans with 1%R; [fourier|apply RmaxLess1].
pattern 1%R at 2; rewrite <- (Rinv_l (Rmax 1 (Cnorm lv))).
apply Rmult_le_compat_l.
left; apply Rinv_0_lt_compat; assumption.
apply RmaxLess2.
apply Rgt_not_eq; assumption.
Qed.

Lemma Cseq_cv_inv_compat : lu 0 → Cseq_cv (/ Un) (/ lu).
Proof.
intros H eps Heps.
destruct (Hu (Cnorm lu / 2))%R as [Ninf Hinf].
apply Rmult_lt_0_compat; [apply Cnorm_pos_lt|fourier]; assumption.
destruct (Hu (/2 × Cnorm lu × Cnorm lu × eps))%R as [N HN].
repeat apply Rmult_lt_0_compat; (apply Cnorm_pos_lt || fourier); assumption.
(Max.max Ninf N).
intros n Hn.
unfold R_dist; unfold Cseq_inv.
assert (Habs : Cnorm lu / 2 Cnorm (Un n)).
replace (Cnorm lu / 2)%R with
(Cnorm lu - Cnorm lu / 2)%R by field.
assert (Hr : Cnorm (Un n - lu) < Cnorm lu / 2).
apply Hinf; eapply le_trans; [apply Max.le_max_l|eexact Hn].
rewrite Cnorm_minus_sym in Hr.
assert (Temp := Cnorm_triang_rev_r (lu - Un n) lu).
replace (Cnorm (Un n)) with (Cnorm (- Un n)) by (apply Cnorm_opp) ;
replace (- Un n)%C with (lu - Un n - lu)%C by field.
fourier.
assert (Hpos : Un n 0).
case (Ceq_or_neq_C0 (Un n)) ; intro HUn.
apply False_ind ; elim (Rlt_irrefl 0).
apply Rlt_le_trans with (Cnorm lu / 2)%R.
unfold Rdiv ; rewrite Rmult_comm ; replace (/2)%R with (Rabs (/2)) by
(apply Rabs_right ; fourier) ; rewrite <- Cnorm_mult ; apply Cnorm_pos_lt ;
apply Cnorm_gt_not_eq ; rewrite Cnorm_mult ; apply Rmult_lt_0_compat.
rewrite Rabs_right ; fourier.
apply Cnorm_pos_lt ; assumption.
apply Rle_trans with (Cnorm (Un n)) ; [assumption | rewrite HUn ;
rewrite Cnorm_C0 ; right ; trivial].
assumption.
replace (/ Un n - / lu)%C with
(/ lu × / Un n × (lu - Un n))%C by (field; tauto).
repeat (rewrite Cnorm_Cmult).
repeat rewrite Cnorm_inv; try assumption.
rewrite Cnorm_minus_sym.
eapply Rlt_le_trans.
apply Rmult_lt_compat_l.
apply Rmult_lt_0_compat; apply Rinv_0_lt_compat;
apply Cnorm_pos_lt; assumption.
apply HN; eapply le_trans; [apply Max.le_max_r|eexact Hn].
replace (/ Cnorm lu × / Cnorm (Un n) × (/2 × Cnorm lu × Cnorm lu × eps))%R
with (/ Cnorm (Un n) × (/2 × Cnorm lu) × eps)%R by (field; split ;
apply Cnorm_no_R0 ; assumption).
rewrite <- Rmult_1_l.
apply Rmult_le_compat_r; auto with real.
eapply Rle_trans.
apply Rmult_le_compat_r.
replace 0%R with (0 × 0)%R by field.
apply Rmult_le_compat; auto with real; apply Cnorm_pos.
destruct Habs as [Habs|Habs].
left; apply Rinv_lt_contravar; [|eassumption].
repeat apply Rmult_lt_0_compat; auto with real; apply Cnorm_pos_lt; assumption.
rewrite Habs; right; reflexivity.
right; field.
apply Cnorm_no_R0; assumption.
Qed.

End Cseq_cv.

Compatibility with Cre and Cim
Lemma Cseq_cv_re_compat : Un l, Cseq_cv Un l
Rseq_cv (fun n : natCre (Un n)) (Cre l).
Proof.
intros Un l HC e epos.
destruct (HC e epos) as [N HN]; N.
intros n Hn.
pose proof HN n Hn.
unfold R_dist.
rewrite Cre_minus_compat.
eapply Rle_lt_trans.
apply Cre_le_Cnorm.
auto.
Qed.

Lemma Cseq_cv_im_compat : Un l, Cseq_cv Un l
Rseq_cv (fun n : natCim (Un n)) (Cim l).
Proof.
intros Un l HC e epos.
destruct (HC e epos) as [N HN]; N.
intros n Hn.
pose proof HN n Hn.
unfold R_dist.
rewrite Cim_minus_compat.
eapply Rle_lt_trans.
apply Cim_le_Cnorm.
auto.
Qed.

Lemma Cseq_cv_re_im_compat : Un l,
Rseq_cv (fun nCre (Un n)) (Cre l) →
Rseq_cv (fun nCim (Un n)) (Cim l) →
Cseq_cv Un l.
Proof.
intros Un l Hre Him e epos.
pose (e / 2)%R as e'.
assert (e'pos : e' > 0) by (unfold e'; fourier).
destruct (Hre e' e'pos) as [Nre HNre].
destruct (Him e' e'pos) as [Nim HNim].
(max Nre Nim).
intros n Hn.
replace e with (e' + e')%R by (unfold e'; field).
eapply Rle_lt_trans.
apply Cnorm_le_Cre_Cim.
apply Rplus_lt_compat.
rewrite <- Cre_minus_compat.
apply HNre.
eapply le_trans.
apply le_max_l.
apply Hn.
rewrite <- Cim_minus_compat.
apply HNim.
eapply le_trans.
apply le_max_r.
apply Hn.
Qed.

Limit uniquess
Lemma Cseq_cv_unique : Un lu1 lu2, Cseq_cv Un lu1Cseq_cv Un lu2lu1 = lu2.
Proof.
intros Un l1 l2 Hl1 Hl2.
rewrite <- Cproj_right with l1.
rewrite <- Cproj_right with l2.
cut (Cre l1 = Cre l2 Cim l1 = Cim l2).
intros [H I]; rewrite H; rewrite I; trivial.
split.
apply Rseq_cv_unique with (fun nCre (Un n));
apply Cseq_cv_re_compat; assumption.
apply Rseq_cv_unique with (fun nCim (Un n));
apply Cseq_cv_im_compat; assumption.
Qed.

Section Cseq_cv_bonus.

Variable Un Vn : natC.
Variable lu lv : C.
Hypothesis Hu : Cseq_cv Un lu.
Hypothesis Hv : Cseq_cv Vn lv.

Lemma Cseq_cv_div_compat : lv 0 → Cseq_cv (Un /Vn) (lu/lv).
Proof.
intro Hlu ; unfold Cseq_div, Rdiv.
apply Cseq_cv_eq_compat with (Un *(/Vn)).
reflexivity.
apply Cseq_cv_mult_compat.
assumption.
apply Cseq_cv_inv_compat ; assumption.
Qed.

End Cseq_cv_bonus.