proposition: Lemma RiemannInt_P3 : forall (f:R -> R) (a b:R) (un:nat -> posreal) (vn wn:nat -> StepFun a b), Un_cv un 0 -> (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; destruct (Rle_dec a b) as [Hle|Hnle]. { apply RiemannInt_P2 with f un wn; assumption. } assert (H1 : b <= a); auto with real. set (vn' := fun n:nat => mkStepFun (StepFun_P6 (pre (vn n)))); set (wn' := fun n:nat => mkStepFun (StepFun_P6 (pre (wn n)))); assert (H2 : forall n:nat, (forall t:R, Rmin b a <= t <= Rmax b a -> Rabs (f t - vn' n t) <= wn' n t) /\ Rabs (RiemannInt_SF (wn' n)) < un n). { intro; elim (H0 n); intros; split. { intros t (H4,H5); apply (H2 t); split; [ apply Rle_trans with (Rmin b a); try assumption; right; unfold Rmin | apply Rle_trans with (Rmax b a); try assumption; right; unfold Rmax ]; decide (Rle_dec a b) with Hnle; decide (Rle_dec b a) with H1; reflexivity. } generalize H3; unfold RiemannInt_SF; destruct (Rle_dec a b) as [Hleab|Hnleab]; destruct (Rle_dec b a) as [Hle'|Hnle']; unfold wn'; intros; (replace (Int_SF (subdivision_val (mkStepFun (StepFun_P6 (pre (wn n))))) (subdivision (mkStepFun (StepFun_P6 (pre (wn n)))))) with (Int_SF (subdivision_val (wn n)) (subdivision (wn n))); [ idtac | apply StepFun_P17 with (fe (wn n)) a b; [ apply StepFun_P1 | apply StepFun_P2; apply (StepFun_P1 (mkStepFun (StepFun_P6 (pre (wn n))))) ] ]). - apply H4. - rewrite Rabs_Ropp; apply H4. - rewrite Rabs_Ropp in H4; apply H4. - apply H4. } assert (H3 := RiemannInt_P2 _ _ _ _ H H1 H2); elim H3; intros x p; exists (- x); unfold Un_cv; unfold Un_cv in p; intros; elim (p _ H4); intros; exists x0; intros; generalize (H5 _ H6); unfold Rdist, RiemannInt_SF; destruct (Rle_dec b a) as [Hle'|Hnle']; destruct (Rle_dec a b) as [Hle''|Hnle'']; intros. 1,3,4: lra. unfold vn' in H7; replace (Int_SF (subdivision_val (vn n)) (subdivision (vn n))) with (Int_SF (subdivision_val (mkStepFun (StepFun_P6 (pre (vn n))))) (subdivision (mkStepFun (StepFun_P6 (pre (vn n)))))); [ unfold Rminus; rewrite Ropp_involutive; rewrite <- Rabs_Ropp; rewrite Ropp_plus_distr; rewrite Ropp_involutive; apply H7 | symmetry ; apply StepFun_P17 with (fe (vn n)) a b; [ apply StepFun_P1 | apply StepFun_P2; apply (StepFun_P1 (mkStepFun (StepFun_P6 (pre (vn n))))) ] ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra