proposition: Lemma RiemannInt_P2 : forall (f:R -> R) (a b:R) (un:nat -> posreal) (vn wn:nat -> StepFun a b), Un_cv un 0 -> a <= b -> (forall n:nat, (forall t:R, Rmin a b <= t <= Rmax a b -> Rabs (f t - vn n t) <= wn n t) /\ Rabs (RiemannInt_SF (wn n)) < un n) -> { l:R | Un_cv (fun N:nat => RiemannInt_SF (vn N)) l }.
proof: Proof. intros; apply R_complete; unfold Un_cv in H; unfold Cauchy_crit; intros; assert (H3 : 0 < eps / 2) by lra. elim (H _ H3); intros N0 H4; exists N0; intros; unfold Rdist; unfold Rdist in H4; elim (H1 n); elim (H1 m); intros; replace (RiemannInt_SF (vn n) - RiemannInt_SF (vn m)) with (RiemannInt_SF (vn n) + -1 * RiemannInt_SF (vn m)); [ idtac | ring ]; rewrite <- StepFun_P30; apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P32 (mkStepFun (StepFun_P28 (-1) (vn n) (vn m)))))). { apply StepFun_P34; assumption. } apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P28 1 (wn n) (wn m)))). { apply StepFun_P37; try assumption. intros; simpl; apply Rle_trans with (Rabs (vn n x - f x) + Rabs (f x - vn m x)). { replace (vn n x + -1 * vn m x) with (vn n x - f x + (f x - vn m x)); [ apply Rabs_triang | ring ]. } assert (H12 : Rmin a b = a). { unfold Rmin; decide (Rle_dec a b) with H0; reflexivity. } assert (H13 : Rmax a b = b). { unfold Rmax; decide (Rle_dec a b) with H0; reflexivity. } rewrite <- H12 in H11; rewrite <- H13 in H11 at 2; rewrite Rmult_1_l; apply Rplus_le_compat. { rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H9. elim H11; intros; split; left; assumption. } apply H7. elim H11; intros; split; left; assumption. } rewrite StepFun_P30; rewrite Rmult_1_l; apply Rlt_trans with (un n + un m). { apply Rle_lt_trans with (Rabs (RiemannInt_SF (wn n)) + Rabs (RiemannInt_SF (wn m))). { apply Rplus_le_compat; apply RRle_abs. } apply Rplus_lt_compat; assumption. } apply Rle_lt_trans with (Rabs (un n) + Rabs (un m)). { apply Rplus_le_compat; apply RRle_abs. } replace (pos (un n)) with (un n - 0); [ idtac | ring ]; replace (pos (un m)) with (un m - 0); [ idtac | ring ]; rewrite <-(Rplus_half_diag eps); apply Rplus_lt_compat; apply H4; assumption. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra