proposition: Lemma RiemannInt_P12 : forall (f g:R -> R) (a b l:R) (pr1:Riemann_integrable f a b) (pr2:Riemann_integrable g a b) (pr3:Riemann_integrable (fun x:R => f x + l * g x) a b), a <= b -> RiemannInt pr3 = RiemannInt pr1 + l * RiemannInt pr2.
proof: Proof. intro f; intros; case (Req_dec l 0); intro. { pattern l at 2; rewrite H0; rewrite Rmult_0_l; rewrite Rplus_0_r; unfold RiemannInt; destruct (RiemannInt_exists pr3 RinvN RinvN_cv) as (?,HUn_cv); destruct (RiemannInt_exists pr1 RinvN RinvN_cv) as (?,HUn_cv0); intros. eapply UL_sequence; [ apply HUn_cv | set (psi1 := fun n:nat => proj1_sig (phi_sequence_prop RinvN pr1 n)); set (psi2 := fun n:nat => proj1_sig (phi_sequence_prop RinvN pr3 n)); apply RiemannInt_P11 with f RinvN (phi_sequence RinvN pr1) psi1 psi2; [ apply RinvN_cv | intro; apply (proj2_sig (phi_sequence_prop RinvN pr1 n)) | intro; assert (H1 : (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t + l * g t - phi_sequence RinvN pr3 n t) <= psi2 n t) /\ Rabs (RiemannInt_SF (psi2 n)) < RinvN n); [ apply (proj2_sig (phi_sequence_prop RinvN pr3 n)) | elim H1; intros; split; try assumption; intros; replace (f t) with (f t + l * g t); [ apply H2; assumption | rewrite H0; ring ] ] | assumption ] ]. } eapply UL_sequence. { unfold RiemannInt; destruct (RiemannInt_exists pr3 RinvN RinvN_cv) as (?,HUn_cv); intros; apply HUn_cv. } unfold Un_cv; 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); unfold Un_cv; intros; assert (H2 : 0 < eps / 5). { unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. } elim (HUn_cv0 _ H2); clear HUn_cv0; intros N0 H3; assert (H4 := RinvN_cv); unfold Un_cv in H4; elim (H4 _ H2); clear H4 H2; intros N1 H4; assert (H5 : 0 < eps / (5 * Rabs l)). { unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; [ prove_sup0 | apply Rabs_pos_lt; assumption ] ]. } elim (HUn_cv _ H5); clear HUn_cv; intros N2 H6; assert (H7 := RinvN_cv); unfold Un_cv in H7; elim (H7 _ H5); clear H7 H5; intros N3 H5; unfold Rdist in H3, H4, H5, H6; set (N := max (max N0 N1) (max N2 N3)). assert (H7 : forall n:nat, (n >= N1)%nat -> RinvN n < eps / 5). { intros; replace (pos (RinvN n)) with (Rabs (RinvN n - 0)); [ unfold RinvN; apply H4; assumption | unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; apply Rabs_right; left; apply (cond_pos (RinvN n)) ]. } clear H4; assert (H4 := H7); clear H7; assert (H7 : forall n:nat, (n >= N3)%nat -> RinvN n < eps / (5 * Rabs l)). { intros; replace (pos (RinvN n)) with (Rabs (RinvN n - 0)); [ unfold RinvN; apply H5; assumption | unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; apply Rabs_right; left; apply (cond_pos (RinvN n)) ]. } clear H5; assert (H5 := H7); clear H7; exists N; intros; unfold Rdist. apply Rle_lt_trans with (Rabs (RiemannInt_SF (phi_sequence RinvN pr3 n) - (RiemannInt_SF (phi_sequence RinvN pr1 n) + l * RiemannInt_SF (phi_sequence RinvN pr2 n))) + Rabs (RiemannInt_SF (phi_sequence RinvN pr1 n) - x0) + Rabs l * Rabs (RiemannInt_SF (phi_sequence RinvN pr2 n) - x)). { apply Rle_trans with (Rabs (RiemannInt_SF (phi_sequence RinvN pr3 n) - (RiemannInt_SF (phi_sequence RinvN pr1 n) + l * RiemannInt_SF (phi_sequence RinvN pr2 n))) + Rabs (RiemannInt_SF (phi_sequence RinvN pr1 n) - x0 + l * (RiemannInt_SF (phi_sequence RinvN pr2 n) - x))). { replace (RiemannInt_SF (phi_sequence RinvN pr3 n) - (x0 + l * x)) with (RiemannInt_SF (phi_sequence RinvN pr3 n) - (RiemannInt_SF (phi_sequence RinvN pr1 n) + l * RiemannInt_SF (phi_sequence RinvN pr2 n)) + (RiemannInt_SF (phi_sequence RinvN pr1 n) - x0 + l * (RiemannInt_SF (phi_sequence RinvN pr2 n) - x))); [ apply Rabs_triang | ring ]. } rewrite Rplus_assoc; apply Rplus_le_compat_l; rewrite <- Rabs_mult; replace (RiemannInt_SF (phi_sequence RinvN pr1 n) - x0 + l * (RiemannInt_SF (phi_sequence RinvN pr2 n) - x)) with (RiemannInt_SF (phi_sequence RinvN pr1 n) - x0 + l * (RiemannInt_SF (phi_sequence RinvN pr2 n) - x)); [ apply Rabs_triang | ring ]. } replace eps with (3 * (eps / 5) + eps / 5 + eps / 5) by lra. apply Rplus_lt_compat. 2:{ apply Rmult_lt_reg_l with (/ Rabs l). { apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption. } rewrite <- Rmult_assoc; rewrite Rinv_l. 2:apply Rabs_no_R0; assumption. rewrite Rmult_1_l; replace (/ Rabs l * (eps / 5)) with (eps / (5 * Rabs l)). { apply H6; unfold ge; apply Nat.le_trans with (max N2 N3); [ apply Nat.le_max_l | apply Nat.le_trans with N; [ unfold N; apply Nat.le_max_r | assumption ] ]. } unfold Rdiv; rewrite Rinv_mult; ring. } apply Rplus_lt_compat. 2:apply H3;Lia.lia. assert (H7 : 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)). { split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr1 n)); intro; apply (proj2_sig (phi_sequence_prop RinvN pr1 n0)). } assert (H8 : exists psi2 : nat -> StepFun a b, (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (g t - phi_sequence RinvN pr2 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 n0)). } assert (H9 : exists psi3 : nat -> StepFun a b, (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t + l * g t - phi_sequence RinvN pr3 n t) <= psi3 n t) /\ Rabs (RiemannInt_SF (psi3 n)) < RinvN n)). { split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr3 n)); intro; apply (proj2_sig (phi_sequence_prop RinvN pr3 n0)). } elim H7; clear H7; intros psi1 H7; elim H8; clear H8; intros psi2 H8; elim H9; clear H9; intros psi3 H9; replace (RiemannInt_SF (phi_sequence RinvN pr3 n) - (RiemannInt_SF (phi_sequence RinvN pr1 n) + l * RiemannInt_SF (phi_sequence RinvN pr2 n))) with (RiemannInt_SF (phi_sequence RinvN pr3 n) + -1 * (RiemannInt_SF (phi_sequence RinvN pr1 n) + l * RiemannInt_SF (phi_sequence RinvN pr2 n))); [ idtac | ring ]; do 2 rewrite <- StepFun_P30; assert (H10 : Rmin a b = a). { unfold Rmin; decide (Rle_dec a b) with H; reflexivity. } assert (H11 : Rmax a b = b). { unfold Rmax; decide (Rle_dec a b) with H; reflexivity. } rewrite H10 in H7; rewrite H10 in H8; rewrite H10 in H9; rewrite H11 in H7; rewrite H11 in H8; rewrite H11 in H9; apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P32 (mkStepFun (StepFun_P28 (-1) (phi_sequence RinvN pr3 n) (mkStepFun (StepFun_P28 l (phi_sequence RinvN pr1 n) (phi_sequence RinvN pr2 n)))))))). { apply StepFun_P34; assumption. } apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P28 1 (psi3 n) (mkStepFun (StepFun_P28 (Rabs l) (psi1 n) (psi2 n)))))). { apply StepFun_P37; try assumption. intros; simpl; rewrite Rmult_1_l. apply Rle_trans with (Rabs (phi_sequence RinvN pr3 n x1 - (f x1 + l * g x1)) + Rabs (f x1 + l * g x1 + -1 * (phi_sequence RinvN pr1 n x1 + l * phi_sequence RinvN pr2 n x1))). { replace (phi_sequence RinvN pr3 n x1 + -1 * (phi_sequence RinvN pr1 n x1 + l * phi_sequence RinvN pr2 n x1)) with (phi_sequence RinvN pr3 n x1 - (f x1 + l * g x1) + (f x1 + l * g x1 + -1 * (phi_sequence RinvN pr1 n x1 + l * phi_sequence RinvN pr2 n x1))); [ apply Rabs_triang | ring ]. } rewrite Rplus_assoc; apply Rplus_le_compat. { elim (H9 n); intros; rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H13. elim H12; intros; split; left; assumption. } apply Rle_trans with (Rabs (f x1 - phi_sequence RinvN pr1 n x1) + Rabs l * Rabs (g x1 - phi_sequence RinvN pr2 n x1)). { rewrite <- Rabs_mult; replace (f x1 + (l * g x1 + -1 * (phi_sequence RinvN pr1 n x1 + l * phi_sequence RinvN pr2 n x1))) with (f x1 - phi_sequence RinvN pr1 n x1 + l * (g x1 - phi_sequence RinvN pr2 n x1)); [ apply Rabs_triang | ring ]. } apply Rplus_le_compat. { elim (H7 n); intros; apply H13. elim H12; intros; split; left; assumption. } apply Rmult_le_compat_l; [ apply Rabs_pos | elim (H8 n); intros; apply H13; elim H12; intros; split; left; assumption ]. } do 2 rewrite StepFun_P30; rewrite Rmult_1_l; replace (3 * (eps / 5)) with (eps / 5 + (eps / 5 + eps / 5)) by ring. repeat apply Rplus_lt_compat. - apply Rlt_trans with (pos (RinvN n)); [ apply Rle_lt_trans with (Rabs (RiemannInt_SF (psi3 n))); [ apply RRle_abs | elim (H9 n); intros; assumption ] | apply H4; unfold ge; apply Nat.le_trans with N; [ apply Nat.le_trans with (max N0 N1); [ apply Nat.le_max_r | unfold N; apply Nat.le_max_l ] | assumption ] ]. - apply Rlt_trans with (pos (RinvN n)); [ apply Rle_lt_trans with (Rabs (RiemannInt_SF (psi1 n))); [ apply RRle_abs | elim (H7 n); intros; assumption ] | apply H4; unfold ge; apply Nat.le_trans with N; [ apply Nat.le_trans with (max N0 N1); [ apply Nat.le_max_r | unfold N; apply Nat.le_max_l ] | assumption ] ]. - apply Rmult_lt_reg_l with (/ Rabs l). { apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption. } rewrite <- Rmult_assoc; rewrite Rinv_l. { rewrite Rmult_1_l; replace (/ Rabs l * (eps / 5)) with (eps / (5 * Rabs l)). { apply Rlt_trans with (pos (RinvN n)); [ apply Rle_lt_trans with (Rabs (RiemannInt_SF (psi2 n))); [ apply RRle_abs | elim (H8 n); intros; assumption ] | apply H5; unfold ge; apply Nat.le_trans with N; [ apply Nat.le_trans with (max N2 N3); [ apply Nat.le_max_r | unfold N; apply Nat.le_max_r ] | assumption ] ]. } unfold Rdiv; rewrite Rinv_mult; ring. } apply Rabs_no_R0; assumption. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra