proposition: Lemma RiemannInt_P17 : forall (f:R -> R) (a b:R) (pr1:Riemann_integrable f a b) (pr2:Riemann_integrable (fun x:R => Rabs (f x)) a b), a <= b -> Rabs (RiemannInt pr1) <= RiemannInt pr2.
proof: Proof. intro f; intros; unfold RiemannInt; case (RiemannInt_exists pr1 RinvN RinvN_cv) as (x0,HUn_cv0); case (RiemannInt_exists pr2 RinvN RinvN_cv) as (x,HUn_cv); set (phi1 := phi_sequence RinvN pr1) in HUn_cv0; set (phi2 := fun N:nat => mkStepFun (StepFun_P32 (phi1 N))); apply Rle_cv_lim with (fun N:nat => Rabs (RiemannInt_SF (phi1 N))) (fun N:nat => RiemannInt_SF (phi2 N)). { intro; unfold phi2; apply StepFun_P34; assumption. } { apply (continuity_seq Rabs (fun N:nat => RiemannInt_SF (phi1 N)) x0); try assumption. apply Rcontinuity_abs. } set (phi3 := phi_sequence RinvN pr2); assert (H0 : exists psi3 : nat -> StepFun a b, (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (Rabs (f t) - phi3 n t) <= psi3 n t) /\ Rabs (RiemannInt_SF (psi3 n)) < RinvN n)). { split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr2 n)); intro; apply (proj2_sig (phi_sequence_prop RinvN pr2 n)). } assert (H1 : exists psi2 : nat -> StepFun a b, (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (Rabs (f t) - phi2 n t) <= psi2 n t) /\ Rabs (RiemannInt_SF (psi2 n)) < RinvN n)). { assert (H1 : exists psi2 : nat -> StepFun a b, (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t - phi1 n t) <= psi2 n t) /\ Rabs (RiemannInt_SF (psi2 n)) < RinvN n)). { split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr1 n)); intro; apply (proj2_sig (phi_sequence_prop RinvN pr1 n)). } elim H1; clear H1; intros psi2 H1; split with psi2; intros; elim (H1 n); clear H1; intros; split; try assumption. intros; unfold phi2; simpl; apply Rle_trans with (Rabs (f t - phi1 n t)). { apply Rabs_triang_inv2. } apply H1; assumption. } elim H0; clear H0; intros psi3 H0; elim H1; clear H1; intros psi2 H1; apply RiemannInt_P11 with (fun x:R => Rabs (f x)) RinvN phi3 psi3 psi2; try assumption; apply RinvN_cv. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra