proposition: Lemma RiemannInt_P15 : forall (a b c:R) (pr:Riemann_integrable (fct_cte c) a b), RiemannInt pr = c * (b - a).
proof: Proof. intros; unfold RiemannInt; destruct (RiemannInt_exists pr RinvN RinvN_cv) as (?,HUn_cv); intros; eapply UL_sequence. { apply HUn_cv. } set (phi1 := fun N:nat => phi_sequence RinvN pr N); change (Un_cv (fun N:nat => RiemannInt_SF (phi1 N)) (c * (b - a))); set (f := fct_cte c); 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 - phi_sequence RinvN pr n t) <= psi1 n t) /\ Rabs (RiemannInt_SF (psi1 n)) < RinvN n)). { split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr n)); intro; apply (proj2_sig (phi_sequence_prop RinvN pr n)). } elim H1; clear H1; intros psi1 H1; set (phi2 := fun n:nat => mkStepFun (StepFun_P4 a b c)); set (psi2 := fun n:nat => mkStepFun (StepFun_P4 a b 0)); apply RiemannInt_P11 with f RinvN phi2 psi2 psi1. - apply RinvN_cv. - intro; split. { intros; unfold f; simpl; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; unfold fct_cte; right; reflexivity. } unfold psi2; rewrite StepFun_P18; rewrite Rmult_0_l; rewrite Rabs_R0; apply (cond_pos (RinvN n)). - assumption. - unfold Un_cv; intros; split with 0%nat; intros; unfold Rdist; unfold phi2; rewrite StepFun_P18; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply H. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra