proposition: Lemma RiemannInt_P10 : forall (f g:R -> R) (a b l:R), Riemann_integrable f a b -> Riemann_integrable g a b -> Riemann_integrable (fun x:R => f x + l * g x) a b.
proof: Proof. unfold Riemann_integrable; intros f g; intros; destruct (Req_dec_T l 0) as [Heq|Hneq]. { elim (X eps); intros x p; split with x; elim p; intros x0 p0; split with x0; elim p0; intros; split; try assumption; rewrite Heq; intros; rewrite Rmult_0_l; rewrite Rplus_0_r; apply H; assumption. } assert (H : 0 < eps / 2). { unfold Rdiv; apply Rmult_lt_0_compat; [ apply (cond_pos eps) | apply Rinv_0_lt_compat; prove_sup0 ]. } assert (H0 : 0 < eps / (2 * Rabs l)). { unfold Rdiv; apply Rmult_lt_0_compat; [ apply (cond_pos eps) | apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; [ prove_sup0 | apply Rabs_pos_lt; assumption ] ]. } elim (X (mkposreal _ H)); intros x p; elim (X0 (mkposreal _ H0)); intros x0 p0; split with (mkStepFun (StepFun_P28 l x x0)); elim p0; elim p; intros x1 p1 x2 p2. split with (mkStepFun (StepFun_P28 (Rabs l) x1 x2)); elim p1; elim p2; clear p1 p2 p0 p X X0; intros; split. { intros; simpl; apply Rle_trans with (Rabs (f t - x t) + Rabs (l * (g t - x0 t))). { replace (f t + l * g t - (x t + l * x0 t)) with (f t - x t + l * (g t - x0 t)); [ apply Rabs_triang | ring ]. } apply Rplus_le_compat; [ apply H3; assumption | rewrite Rabs_mult; apply Rmult_le_compat_l; [ apply Rabs_pos | apply H1; assumption ] ]. } rewrite StepFun_P30; apply Rle_lt_trans with (Rabs (RiemannInt_SF x1) + Rabs (Rabs l * RiemannInt_SF x2)). { apply Rabs_triang. } rewrite <-(Rplus_half_diag eps); apply Rplus_lt_compat. { apply H4. } rewrite Rabs_mult; rewrite Rabs_Rabsolu; 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 / 2)) with (eps / (2 * Rabs l)); [ apply H2 | unfold Rdiv; rewrite Rinv_mult; ring ] | apply Rabs_no_R0; assumption ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra