proposition: Lemma Cseq_Rseq_Rseq_equiv : Cseq_cv Un lu <-> (Rseq_cv (fun n => Cre (Un n)) (Cre lu) /\ Rseq_cv (fun n => Cim (Un n)) (Cim lu)).
proof: Proof. split ; intro H. split ; intros eps eps_pos. destruct (H _ eps_pos) as [N HN] ; exists N ; intros n Hn. unfold R_dist ; rewrite Cre_minus_compat. assert (Hrew := Cadd_conj (Un n - lu)). assert (HN_conj : forall n : nat, (n >= N)%nat -> Cnorm (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 lra ; apply Rlt_le_trans with (/2 * (2 * eps))%R. apply Rmult_lt_compat_l ; [lra |] ; 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] ; exists N ; intros n Hn. unfold R_dist ; rewrite Cim_minus_compat. assert (Hrew := Cminus_conj (Un n - lu)). assert (HN_conj : forall n : nat, (n >= N)%nat -> Cnorm (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 lra ; apply Rlt_le_trans with (/2 * (2 * eps))%R. apply Rmult_lt_compat_l ; [lra |] ; 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 lra ; destruct (Hre _ eps_2_pos) as (N1, HN1) ; destruct (Him _ eps_2_pos) as (N2, HN2) ; exists (Nat.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 Nat.le_trans with (Nat.max N1 N2)%nat. apply Nat.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 Nat.le_trans with (Nat.max N1 N2)%nat. apply Nat.le_max_l. assumption. right ; field. Qed.
imports: MyReals PeanoNat Rsequence_def Rsequence_facts Rsequence_base_facts Lia Lra Complex Csequence_def