proposition: Lemma RiemannInt_P18 : forall (f g:R -> R) (a b:R) (pr1:Riemann_integrable f a b) (pr2:Riemann_integrable g a b), a <= b -> (forall x:R, a < x < b -> f x = g x) -> 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); eapply UL_sequence. { apply HUn_cv0. } set (phi1 := fun N:nat => phi_sequence RinvN pr1 N); change (Un_cv (fun N:nat => RiemannInt_SF (phi1 N)) x); assert (H1 : exists psi1 : nat -> StepFun a b, (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t - phi1 n t) <= psi1 n t) /\ Rabs (RiemannInt_SF (psi1 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 psi1 H1; set (phi2 := fun N:nat => phi_sequence RinvN pr2 N). set (phi2_aux := fun (N:nat) (x:R) => match Req_dec_T x a with | left _ => f a | right _ => match Req_dec_T x b with | left _ => f b | right _ => phi2 N x end end). cut (forall N:nat, IsStepFun (phi2_aux N) a b). { intro; set (phi2_m := fun N:nat => mkStepFun (X N)). assert (H2 : exists psi2 : nat -> StepFun a b, (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (g t - phi2 n t) <= psi2 n t) /\ Rabs (RiemannInt_SF (psi2 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)). } elim H2; clear H2; intros psi2 H2; apply RiemannInt_P11 with f RinvN phi2_m psi2 psi1; try assumption. - apply RinvN_cv. - intro; elim (H2 n); intros; split; try assumption. intros; unfold phi2_m; simpl; unfold phi2_aux; destruct (Req_dec_T t a) as [Heqa|Hneqa]; destruct (Req_dec_T t b) as [Heqb|Hneqb]. + rewrite Heqa; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply Rle_trans with (Rabs (g t - phi2 n t)). { apply Rabs_pos. } pattern a at 3; rewrite <- Heqa; apply H3; assumption. + rewrite Heqa; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply Rle_trans with (Rabs (g t - phi2 n t)). { apply Rabs_pos. } pattern a at 3; rewrite <- Heqa; apply H3; assumption. + rewrite Heqb; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply Rle_trans with (Rabs (g t - phi2 n t)). { apply Rabs_pos. } pattern b at 3; rewrite <- Heqb; apply H3; assumption. + replace (f t) with (g t). { apply H3; assumption. } symmetry ; apply H0; elim H5; clear H5; intros. assert (H7 : Rmin a b = a). { unfold Rmin; destruct (Rle_dec a b) as [Heqab|Hneqab]; [ reflexivity | elim Hneqab; assumption ]. } assert (H8 : Rmax a b = b). { unfold Rmax; destruct (Rle_dec a b) as [Heqab|Hneqab]; [ reflexivity | elim Hneqab; assumption ]. } rewrite H7 in H5; rewrite H8 in H6; split. { elim H5; intro; [ assumption | elim Hneqa; symmetry ; assumption ]. } elim H6; intro; [ assumption | elim Hneqb; assumption ]. - cut (forall N:nat, RiemannInt_SF (phi2_m N) = RiemannInt_SF (phi2 N)). { intro; unfold Un_cv; intros; elim (HUn_cv _ H4); intros; exists x1; intros; rewrite (H3 n); apply H5; assumption. } intro; apply Rle_antisym. { apply StepFun_P37; try assumption. intros; unfold phi2_m; simpl; unfold phi2_aux; destruct (Req_dec_T x1 a) as [Heqa|Hneqa]; destruct (Req_dec_T x1 b) as [Heqb|Hneqb]. + elim H3; intros; rewrite Heqa in H4; elim (Rlt_irrefl _ H4). + elim H3; intros; rewrite Heqa in H4; elim (Rlt_irrefl _ H4). + elim H3; intros; rewrite Heqb in H5; elim (Rlt_irrefl _ H5). + right; reflexivity. } apply StepFun_P37; try assumption. intros; unfold phi2_m; simpl; unfold phi2_aux; destruct (Req_dec_T x1 a) as [ -> |Hneqa]. { elim H3; intros; elim (Rlt_irrefl _ H4). } destruct (Req_dec_T x1 b) as [ -> |Hneqb]. { elim H3; intros; elim (Rlt_irrefl _ H5). } right; reflexivity. } intro; assert (H2 := pre (phi2 N)); unfold IsStepFun in H2; unfold is_subdivision in H2; elim H2; clear H2; intros l [lf H2]; split with l; split with lf; unfold adapted_couple in H2; decompose [and] H2; clear H2; unfold adapted_couple; repeat split; try assumption. intros; assert (H9 := H8 i H2); unfold constant_D_eq, open_interval in H9; unfold constant_D_eq, open_interval; intros; rewrite <- (H9 x1 H7); assert (H10 : a <= pos_Rl l i). { replace a with (Rmin a b). { rewrite <- H5; elim (RList_P6 l); intros; apply H10. - assumption. - apply Nat.le_0_l. - apply Nat.lt_trans with (pred (length l)); [ assumption | apply Nat.lt_pred_l ]. intro; rewrite H12 in H6; discriminate. } unfold Rmin; decide (Rle_dec a b) with H; reflexivity. } assert (H11 : pos_Rl l (S i) <= b). { replace b with (Rmax a b). { rewrite <- H4; elim (RList_P6 l); intros; apply H11. - assumption. - apply Nat.le_succ_l; assumption. - apply Nat.lt_pred_l; intro; rewrite H13 in H6; discriminate. } unfold Rmax; decide (Rle_dec a b) with H; reflexivity. } elim H7; clear H7; intros; unfold phi2_aux; destruct (Req_dec_T x1 a) as [Heq|Hneq]; destruct (Req_dec_T x1 b) as [Heq'|Hneq']. - rewrite Heq' in H12; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H11 H12)). - rewrite Heq in H7; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H10 H7)). - rewrite Heq' in H12; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H11 H12)). - reflexivity. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra