proposition: Lemma lb_Cauchy:forall alpha, Rseries.Cauchy_crit (lb alpha).
proof: Proof. intros alpha. intros eps H_eps_pos. set (N:=Zabs_nat (up (2 / eps))). exists N. intros m n Hn Hm. unfold Rfunctions.R_dist. apply Raxioms.Rlt_trans with (Qminus (ub alpha N)(lb alpha N)). set (u_N:=ub alpha N); set (l_N:=lb alpha N); set (l_n:=lb alpha n);set (l_m:=lb alpha m). apply Rbasic_fun.Rabs_def1. repeat rewrite <- Q_to_Rminus; apply Q_to_Rlt. apply Qlt_Zero_Qminus. stepr (Qplus (Qminus u_N l_m)(Qminus l_n l_N)); try ring. apply Qlt_le_reg_pos. apply Qlt_Qminus_Zero; subst u_N l_m; apply lb_lt_ub. apply Qle_Qminus_Zero; subst l_N l_n; apply lb_nondecreasing; auto. apply RIneq.Ropp_lt_cancel; rewrite RIneq.Ropp_involutive; rewrite RIneq.Ropp_minus_distr. repeat rewrite <- Q_to_Rminus; apply Q_to_Rlt. apply Qlt_Zero_Qminus. stepr (Qplus(Qminus u_N l_n)(Qminus l_m l_N)); try ring. apply Qlt_le_reg_pos. apply Qlt_Qminus_Zero; subst u_N l_n; apply lb_lt_ub. apply Qle_Qminus_Zero; subst l_N l_m; apply lb_nondecreasing; auto. apply RIneq.Rle_lt_trans with (Qdiv (Z_to_Q (Z_of_nat 2)) (Qplus (Z_to_Q (Z_of_nat N)) (Z_to_Q (Z_of_nat 1)))). apply Q_to_Rle; apply thesis_5_7_9. assert (H_N_plus_one_pos:(0 < Rdefinitions.IZR N +1)%R); [ apply RIneq.Rle_lt_trans with (Rdefinitions.IZR N); rewrite <- INR_IZR_INZ; auto with real| ]. assert (H_N_plus_one_nonzero:(Rdefinitions.IZR N +1<>0)%R); auto with real. elim (Raxioms.archimed (2/eps)); intros H_N _. rewrite <- (Z_of_nat_Zabs_nat_pos (up(2/eps))) in H_N. rewrite Q_to_Rdiv. rewrite Q_to_Rplus. repeat rewrite Z_to_Q_to_R_IZR. assert (2/eps-1<(Rdefinitions.IZR N))%R. apply Raxioms.Rlt_trans with (2/eps)%R; auto. apply RIneq.Rminus_lt. stepl (Ropp (Rdefinitions.IZR 1%nat)). simpl. apply RIneq.Ropp_lt_gt_0_contravar. apply Fourier_util.Rlt_zero_1. simpl; ring. simpl. apply Rmult_lt_reg_l with ((Rdefinitions.IZR N + 1)*(Rinv eps))%R. apply Fourier_util.Rlt_mult_inv_pos; auto. stepl (2/eps)%R. stepr (Rdefinitions.IZR N+1)%R. apply Rplus_lt_reg_r with (Ropp 1). stepl (2/eps -1)%R; try ring. stepr (Rdefinitions.IZR N)%R; auto; try ring. field; auto with real. field; auto with real. natq_S N; natq_zero; apply Z_to_Q_not_eq; apply inj_neq; discriminate. apply le_O_IZR. apply RIneq.Rlt_le. apply Raxioms.Rlt_trans with (2 / eps)%R; auto; unfold Rdiv; apply Fourier_util.Rlt_mult_inv_pos; auto; apply DiscrR.Rlt_R0_R2. Qed.
imports: digits ub rep Rseries Rdefinitions RIneq Rcomplete QArithSternBrocot(R_addenda) Fourier_solvable_ineqs