proposition: Lemma RiemannInt_P8 : forall (f:R -> R) (a b:R) (pr1:Riemann_integrable f a b) (pr2:Riemann_integrable f b a), RiemannInt pr1 = - RiemannInt pr2.
proof: Proof. intro f; intros; eapply UL_sequence. { unfold RiemannInt; destruct (RiemannInt_exists pr1 RinvN RinvN_cv) as (?,HUn); apply HUn. } unfold RiemannInt; destruct (RiemannInt_exists pr2 RinvN RinvN_cv) as (?,HUn); intros; cut (exists psi1 : nat -> StepFun a b, (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t - phi_sequence RinvN pr1 n t) <= psi1 n t) /\ Rabs (RiemannInt_SF (psi1 n)) < RinvN n)). 2:{ split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr1 n)); intro; apply (proj2_sig (phi_sequence_prop RinvN pr1 n)). } cut (exists psi2 : nat -> StepFun b a, (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t - phi_sequence RinvN pr2 n t) <= psi2 n t) /\ Rabs (RiemannInt_SF (psi2 n)) < RinvN n)). 2:{ split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr2 n)); intro; rewrite Rmin_comm; rewrite RmaxSym; apply (proj2_sig (phi_sequence_prop RinvN pr2 n)). } intros; elim H; clear H; intros psi2 H; elim H0; clear H0; intros psi1 H0; assert (H1 := RinvN_cv); unfold Un_cv; intros; assert (H3 : 0 < eps / 3). { unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. } unfold Un_cv in H1; elim (H1 _ H3); clear H1; intros N0 H1; unfold Rdist in H1; simpl in H1; assert (H4 : forall n:nat, (n >= N0)%nat -> RinvN n < eps / 3). { intros; assert (H5 := H1 _ H4); replace (pos (RinvN n)) with (Rabs (/ (INR n + 1) - 0)); [ assumption | unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; apply Rabs_right; left; apply (cond_pos (RinvN n)) ]. } clear H1; destruct (HUn _ H3) as (N1,H1); exists (max N0 N1); intros; unfold Rdist; apply Rle_lt_trans with (Rabs (RiemannInt_SF (phi_sequence RinvN pr1 n) + RiemannInt_SF (phi_sequence RinvN pr2 n)) + Rabs (RiemannInt_SF (phi_sequence RinvN pr2 n) - x)). { rewrite <- (Rabs_Ropp (RiemannInt_SF (phi_sequence RinvN pr2 n) - x)); replace (RiemannInt_SF (phi_sequence RinvN pr1 n) - - x) with (RiemannInt_SF (phi_sequence RinvN pr1 n) + RiemannInt_SF (phi_sequence RinvN pr2 n) + - (RiemannInt_SF (phi_sequence RinvN pr2 n) - x)); [ apply Rabs_triang | ring ]. } replace eps with (2 * (eps / 3) + eps / 3) by lra. apply Rplus_lt_compat. 2:{ unfold Rdist in H1; apply H1; unfold ge; apply Nat.le_trans with (max N0 N1); [ apply Nat.le_max_r | assumption ]. } rewrite (StepFun_P39 (phi_sequence RinvN pr2 n)); replace (RiemannInt_SF (phi_sequence RinvN pr1 n) + - RiemannInt_SF (mkStepFun (StepFun_P6 (pre (phi_sequence RinvN pr2 n))))) with (RiemannInt_SF (phi_sequence RinvN pr1 n) + -1 * RiemannInt_SF (mkStepFun (StepFun_P6 (pre (phi_sequence RinvN pr2 n))))); [ idtac | ring ]; rewrite <- StepFun_P30. destruct (Rle_dec a b) as [Hle|Hnle]. { apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P32 (mkStepFun (StepFun_P28 (-1) (phi_sequence RinvN pr1 n) (mkStepFun (StepFun_P6 (pre (phi_sequence RinvN pr2 n))))))))). { apply StepFun_P34; assumption. } apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P28 1 (psi1 n) (mkStepFun (StepFun_P6 (pre (psi2 n))))))). { apply StepFun_P37; try assumption. intros; simpl; rewrite Rmult_1_l; apply Rle_trans with (Rabs (phi_sequence RinvN pr1 n x0 - f x0) + Rabs (f x0 - phi_sequence RinvN pr2 n x0)). { replace (phi_sequence RinvN pr1 n x0 + -1 * phi_sequence RinvN pr2 n x0) with (phi_sequence RinvN pr1 n x0 - f x0 + (f x0 - phi_sequence RinvN pr2 n x0)); [ apply Rabs_triang | ring ]. } assert (H7 : Rmin a b = a). { unfold Rmin; decide (Rle_dec a b) with Hle; reflexivity. } assert (H8 : Rmax a b = b). { unfold Rmax; decide (Rle_dec a b) with Hle; reflexivity. } apply Rplus_le_compat. { elim (H0 n); intros; rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H9; rewrite H7; rewrite H8. elim H6; intros; split; left; assumption. } elim (H n); intros; apply H9; rewrite H7; rewrite H8. elim H6; intros; split; left; assumption. } rewrite StepFun_P30; rewrite Rmult_1_l; rewrite <-Rplus_diag; apply Rplus_lt_compat. { elim (H0 n); intros; apply Rle_lt_trans with (Rabs (RiemannInt_SF (psi1 n))); [ apply RRle_abs | apply Rlt_trans with (pos (RinvN n)); [ assumption | apply H4; unfold ge; apply Nat.le_trans with (max N0 N1); [ apply Nat.le_max_l | assumption ] ] ]. } elim (H n); intros; rewrite <- (Ropp_involutive (RiemannInt_SF (mkStepFun (StepFun_P6 (pre (psi2 n)))))) ; rewrite <- StepFun_P39; apply Rle_lt_trans with (Rabs (RiemannInt_SF (psi2 n))); [ rewrite <- Rabs_Ropp; apply RRle_abs | apply Rlt_trans with (pos (RinvN n)); [ assumption | apply H4; unfold ge; apply Nat.le_trans with (max N0 N1); [ apply Nat.le_max_l | assumption ] ] ]. } assert (Hyp : b <= a). { auto with real. } rewrite StepFun_P39; rewrite Rabs_Ropp; apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P32 (mkStepFun (StepFun_P6 (StepFun_P28 (-1) (phi_sequence RinvN pr1 n) (mkStepFun (StepFun_P6 (pre (phi_sequence RinvN pr2 n)))))))))). { apply StepFun_P34; assumption. } apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P28 1 (mkStepFun (StepFun_P6 (pre (psi1 n)))) (psi2 n)))). { apply StepFun_P37; try assumption. intros; simpl; rewrite Rmult_1_l; apply Rle_trans with (Rabs (phi_sequence RinvN pr1 n x0 - f x0) + Rabs (f x0 - phi_sequence RinvN pr2 n x0)). { replace (phi_sequence RinvN pr1 n x0 + -1 * phi_sequence RinvN pr2 n x0) with (phi_sequence RinvN pr1 n x0 - f x0 + (f x0 - phi_sequence RinvN pr2 n x0)); [ apply Rabs_triang | ring ]. } assert (H7 : Rmin a b = b). { unfold Rmin; decide (Rle_dec a b) with Hnle; reflexivity. } assert (H8 : Rmax a b = a). { unfold Rmax; decide (Rle_dec a b) with Hnle; reflexivity. } apply Rplus_le_compat. { elim (H0 n); intros; rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H9; rewrite H7; rewrite H8. elim H6; intros; split; left; assumption. } elim (H n); intros; apply H9; rewrite H7; rewrite H8; elim H6; intros; split; left; assumption. } rewrite StepFun_P30; rewrite Rmult_1_l; rewrite <-Rplus_diag; apply Rplus_lt_compat. { elim (H0 n); intros; rewrite <- (Ropp_involutive (RiemannInt_SF (mkStepFun (StepFun_P6 (pre (psi1 n)))))) ; rewrite <- StepFun_P39; apply Rle_lt_trans with (Rabs (RiemannInt_SF (psi1 n))); [ rewrite <- Rabs_Ropp; apply RRle_abs | apply Rlt_trans with (pos (RinvN n)); [ assumption | apply H4; unfold ge; apply Nat.le_trans with (max N0 N1); [ apply Nat.le_max_l | assumption ] ] ]. } elim (H n); intros; apply Rle_lt_trans with (Rabs (RiemannInt_SF (psi2 n))); [ apply RRle_abs | apply Rlt_trans with (pos (RinvN n)); [ assumption | apply H4; unfold ge; apply Nat.le_trans with (max N0 N1); [ apply Nat.le_max_l | assumption ] ] ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra