products/sources/formale sprachen/Coq/theories/Reals/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: undo020.fake   Sprache: Coq

Original von: Coq©
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import Rfunctions.
Require Import SeqSeries.
Require Import Ranalysis_reg.
Require Import Rbase.
Require Import RiemannInt_SF.
Require Import Max.
Local Open Scope R_scope.

Set Implicit Arguments.

(********************************************)
(**           Riemann's Integral            *)
(********************************************)

Definition Riemann_integrable (f:R -> R) (a b:R) : Type :=
  forall eps:posreal,
    { phi:StepFun a b &
      { psi:StepFun a b |
        (forall t:R,
          Rmin a b <= t <= Rmax a b -> Rabs (f t - phi t) <= psi t) /\
        Rabs (RiemannInt_SF psi) < eps } }.

Definition phi_sequence (un:nat -> posreal) (f:R -> R)
  (a b:R) (pr:Riemann_integrable f a b) (n:nat) :=
  projT1 (pr (un n)).

Lemma phi_sequence_prop :
  forall (un:nat -> posreal) (f:R -> R) (a b:R) (pr:Riemann_integrable f a b)
    (N:nat),
    { psi:StepFun a b |
      (forall t:R,
        Rmin a b <= t <= Rmax a b ->
        Rabs (f t - phi_sequence un pr N t) <= psi t) /\
      Rabs (RiemannInt_SF psi) < un N }.
Proof.
  intros; apply (projT2 (pr (un N))).
Qed.

Lemma RiemannInt_P1 :
  forall (f:R -> R) (a b:R),
    Riemann_integrable f a b -> Riemann_integrable f b a.
Proof.
  unfold Riemann_integrable; intros; elim (X eps); clear X; intros.
  elim p; clear p; intros x0 p; exists (mkStepFun (StepFun_P6 (pre x)));
      exists (mkStepFun (StepFun_P6 (pre x0)));
        elim p; clear p; intros; split.
  intros; apply (H t); elim H1; clear H1; intros; split;
    [ apply Rle_trans with (Rmin b a); try assumption; right;
      unfold Rmin
      | apply Rle_trans with (Rmax b a); try assumption; right;
        unfold Rmax ];
    (case (Rle_dec a b); case (Rle_dec b a); intros;
      try reflexivity || apply Rle_antisym;
        [ assumption | assumption | auto with real | auto with real ]).
  generalize H0; unfold RiemannInt_SF; case (Rle_dec a b);
    case (Rle_dec b a); intros;
      (replace
        (Int_SF (subdivision_val (mkStepFun (StepFun_P6 (pre x0))))
          (subdivision (mkStepFun (StepFun_P6 (pre x0))))) with
        (Int_SF (subdivision_val x0) (subdivision x0));
        [ idtac
          | apply StepFun_P17 with (fe x0) a b;
            [ apply StepFun_P1
              | apply StepFun_P2;
                apply (StepFun_P1 (mkStepFun (StepFun_P6 (pre x0)))) ] ]).
  apply H1.
  rewrite Rabs_Ropp; apply H1.
  rewrite Rabs_Ropp in H1; apply H1.
  apply H1.
Qed.

Lemma RiemannInt_P2 :
  forall (f:R -> R) (a b:R) (un:nat -> posreal) (vn wn:nat -> StepFun a b),
    Un_cv un 0 ->
    a <= b ->
    (forall n:nat,
      (forall t:R, Rmin a b <= t <= Rmax a b -> Rabs (f t - vn n t) <= wn n t) /\
      Rabs (RiemannInt_SF (wn n)) < un n) ->
    { l:R | Un_cv (fun N:nat => RiemannInt_SF (vn N)) l }.
Proof.
  intros; apply R_complete; unfold Un_cv in H; unfold Cauchy_crit;
    intros; assert (H3 : 0 < eps / 2).
  unfold Rdiv; apply Rmult_lt_0_compat;
    [ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
  elim (H _ H3); intros N0 H4; exists N0; intros; unfold R_dist;
    unfold R_dist in H4; elim (H1 n); elim (H1 m); intros;
      replace (RiemannInt_SF (vn n) - RiemannInt_SF (vn m)) with
      (RiemannInt_SF (vn n) + -1 * RiemannInt_SF (vn m));
      [ idtac | ring ]; rewrite <- StepFun_P30;
        apply Rle_lt_trans with
          (RiemannInt_SF
            (mkStepFun (StepFun_P32 (mkStepFun (StepFun_P28 (-1) (vn n) (vn m)))))).
  apply StepFun_P34; assumption.
  apply Rle_lt_trans with
    (RiemannInt_SF (mkStepFun (StepFun_P28 1 (wn n) (wn m)))).
  apply StepFun_P37; try assumption.
  intros; simpl;
    apply Rle_trans with (Rabs (vn n x - f x) + Rabs (f x - vn m x)).
  replace (vn n x + -1 * vn m x) with (vn n x - f x + (f x - vn m x));
  [ apply Rabs_triang | ring ].
  assert (H12 : Rmin a b = a).
  unfold Rmin; decide (Rle_dec a b) with H0; reflexivity.
  assert (H13 : Rmax a b = b).
  unfold Rmax; decide (Rle_dec a b) with H0; reflexivity.
  rewrite <- H12 in H11; rewrite <- H13 in H11 at 2;
    rewrite Rmult_1_l; apply Rplus_le_compat.
  rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H9.
  elim H11; intros; split; left; assumption.
  apply H7.
  elim H11; intros; split; left; assumption.
  rewrite StepFun_P30; rewrite Rmult_1_l; apply Rlt_trans with (un n + un m).
  apply Rle_lt_trans with
    (Rabs (RiemannInt_SF (wn n)) + Rabs (RiemannInt_SF (wn m))).
  apply Rplus_le_compat; apply RRle_abs.
  apply Rplus_lt_compat; assumption.
  apply Rle_lt_trans with (Rabs (un n) + Rabs (un m)).
  apply Rplus_le_compat; apply RRle_abs.
  replace (pos (un n)) with (un n - 0); [ idtac | ring ];
  replace (pos (un m)) with (un m - 0); [ idtac | ring ];
  rewrite (double_var eps); apply Rplus_lt_compat; apply H4;
    assumption.
Qed.

Lemma RiemannInt_P3 :
  forall (f:R -> R) (a b:R) (un:nat -> posreal) (vn wn:nat -> StepFun a b),
    Un_cv un 0 ->
    (forall n:nat,
      (forall t:R, Rmin a b <= t <= Rmax a b -> Rabs (f t - vn n t) <= wn n t) /\
      Rabs (RiemannInt_SF (wn n)) < un n) ->
    { l:R | Un_cv (fun N:nat => RiemannInt_SF (vn N)) l }.
Proof.
  intros; destruct (Rle_dec a b) as [Hle|Hnle].
  apply RiemannInt_P2 with f un wn; assumption.
  assert (H1 : b <= a); auto with real.
  set (vn' := fun n:nat => mkStepFun (StepFun_P6 (pre (vn n))));
    set (wn' := fun n:nat => mkStepFun (StepFun_P6 (pre (wn n))));
      assert
        (H2 :
          forall n:nat,
            (forall t:R,
              Rmin b a <= t <= Rmax b a -> Rabs (f t - vn' n t) <= wn' n t) /\
            Rabs (RiemannInt_SF (wn' n)) < un n).
  intro; elim (H0 n); intros; split.
  intros t (H4,H5); apply (H2 t); split;
    [ apply Rle_trans with (Rmin b a); try assumption; right;
      unfold Rmin
      | apply Rle_trans with (Rmax b a); try assumption; right;
        unfold Rmax ];
    decide (Rle_dec a b) with Hnle; decide (Rle_dec b a) with H1; reflexivity.
  generalize H3; unfold RiemannInt_SF; destruct (Rle_dec a b) as [Hleab|Hnleab];
    destruct (Rle_dec b a) as [Hle'|Hnle']; unfold wn'; intros;
      (replace
        (Int_SF (subdivision_val (mkStepFun (StepFun_P6 (pre (wn n)))))
          (subdivision (mkStepFun (StepFun_P6 (pre (wn n)))))) with
        (Int_SF (subdivision_val (wn n)) (subdivision (wn n)));
        [ idtac
          | apply StepFun_P17 with (fe (wn n)) a b;
            [ apply StepFun_P1
              | apply StepFun_P2;
                apply (StepFun_P1 (mkStepFun (StepFun_P6 (pre (wn n))))) ] ]).
  apply H4.
  rewrite Rabs_Ropp; apply H4.
  rewrite Rabs_Ropp in H4; apply H4.
  apply H4.
  assert (H3 := RiemannInt_P2 _ _ _ _ H H1 H2); elim H3; intros x p;
    exists (- x); unfold Un_cv; unfold Un_cv in p;
      intros; elim (p _ H4); intros; exists x0; intros;
        generalize (H5 _ H6); unfold R_dist, RiemannInt_SF;
          destruct (Rle_dec b a) as [Hle'|Hnle']; destruct (Rle_dec a b) as [Hle''|Hnle''];
          intros.
  elim Hnle; assumption.
  unfold vn' in H7;
    replace (Int_SF (subdivision_val (vn n)) (subdivision (vn n))) with
    (Int_SF (subdivision_val (mkStepFun (StepFun_P6 (pre (vn n)))))
      (subdivision (mkStepFun (StepFun_P6 (pre (vn n))))));
    [ unfold Rminus; rewrite Ropp_involutive; rewrite <- Rabs_Ropp;
      rewrite Ropp_plus_distr; rewrite Ropp_involutive;
        apply H7
      | symmetry ; apply StepFun_P17 with (fe (vn n)) a b;
        [ apply StepFun_P1
          | apply StepFun_P2;
            apply (StepFun_P1 (mkStepFun (StepFun_P6 (pre (vn n))))) ] ].
  elim Hnle'; assumption.
  elim Hnle'; assumption.
Qed.

Lemma RiemannInt_exists :
  forall (f:R -> R) (a b:R) (pr:Riemann_integrable f a b)
    (un:nat -> posreal),
    Un_cv un 0 ->
    { l:R | Un_cv (fun N:nat => RiemannInt_SF (phi_sequence un pr N)) l }.
Proof.
  intros f; intros;
    apply RiemannInt_P3 with
      f un (fun n:nat => proj1_sig (phi_sequence_prop un pr n));
      [ apply H | intro; apply (proj2_sig (phi_sequence_prop un pr n)) ].
Qed.

Lemma RiemannInt_P4 :
  forall (f:R -> R) (a b l:R) (pr1 pr2:Riemann_integrable f a b)
    (un vn:nat -> posreal),
    Un_cv un 0 ->
    Un_cv vn 0 ->
    Un_cv (fun N:nat => RiemannInt_SF (phi_sequence un pr1 N)) l ->
    Un_cv (fun N:nat => RiemannInt_SF (phi_sequence vn pr2 N)) l.
Proof.
  unfold Un_cv; unfold R_dist; intros f; intros;
    assert (H3 : 0 < eps / 3).
  unfold Rdiv; apply Rmult_lt_0_compat;
    [ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
  elim (H _ H3); clear H; intros N0 H; elim (H0 _ H3); clear H0; intros N1 H0;
    elim (H1 _ H3); clear H1; intros N2 H1; set (N := max (max N0 N1) N2);
      exists N; intros;
        apply Rle_lt_trans with
          (Rabs
            (RiemannInt_SF (phi_sequence vn pr2 n) -
              RiemannInt_SF (phi_sequence un pr1 n)) +
            Rabs (RiemannInt_SF (phi_sequence un pr1 n) - l)).
  replace (RiemannInt_SF (phi_sequence vn pr2 n) - l) with
  (RiemannInt_SF (phi_sequence vn pr2 n) -
    RiemannInt_SF (phi_sequence un pr1 n) +
    (RiemannInt_SF (phi_sequence un pr1 n) - l)); [ apply Rabs_triang | ring ].
  replace eps with (2 * (eps / 3) + eps / 3).
  apply Rplus_lt_compat.
  elim (phi_sequence_prop vn pr2 n); intros psi_vn H5;
    elim (phi_sequence_prop un pr1 n); intros psi_un H6;
      replace
      (RiemannInt_SF (phi_sequence vn pr2 n) -
        RiemannInt_SF (phi_sequence un pr1 n)) with
      (RiemannInt_SF (phi_sequence vn pr2 n) +
        -1 * RiemannInt_SF (phi_sequence un pr1 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 vn pr2 n)
              (phi_sequence un pr1 n)))))).
  apply StepFun_P34; assumption.
  apply Rle_lt_trans with
    (RiemannInt_SF (mkStepFun (StepFun_P28 1 psi_un psi_vn))).
  apply StepFun_P37; try assumption; intros; simpl; rewrite Rmult_1_l;
    apply Rle_trans with
      (Rabs (phi_sequence vn pr2 n x - f x) +
        Rabs (f x - phi_sequence un pr1 n x)).
  replace (phi_sequence vn pr2 n x + -1 * phi_sequence un pr1 n x) with
  (phi_sequence vn pr2 n x - f x + (f x - phi_sequence un pr1 n x));
  [ apply Rabs_triang | ring ].
  assert (H10 : Rmin a b = a).
  unfold Rmin; decide (Rle_dec a b) with Hle; reflexivity.
  assert (H11 : Rmax a b = b).
  unfold Rmax; decide (Rle_dec a b) with Hle; reflexivity.
  rewrite (Rplus_comm (psi_un x)); apply Rplus_le_compat.
  rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; destruct H5 as (H8,H9); apply H8.
  rewrite H10; rewrite H11; elim H7; intros; split; left; assumption.
  elim H6; intros; apply H8.
  rewrite H10; rewrite H11; elim H7; intros; split; left; assumption.
  rewrite StepFun_P30; rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat.
  apply Rlt_trans with (pos (un n)).
  elim H6; intros; apply Rle_lt_trans with (Rabs (RiemannInt_SF psi_un)).
  apply RRle_abs.
  assumption.
  replace (pos (un n)) with (Rabs (un n - 0));
  [ apply H; unfold ge; apply le_trans with N; try assumption;
    unfold N; apply le_trans with (max N0 N1);
      apply le_max_l
    | unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; apply Rabs_right;
      apply Rle_ge; left; apply (cond_pos (un n)) ].
  apply Rlt_trans with (pos (vn n)).
  elim H5; intros; apply Rle_lt_trans with (Rabs (RiemannInt_SF psi_vn)).
  apply RRle_abs; assumption.
  assumption.
  replace (pos (vn n)) with (Rabs (vn n - 0));
  [ apply H0; unfold ge; apply le_trans with N; try assumption;
    unfold N; apply le_trans with (max N0 N1);
      [ apply le_max_r | apply le_max_l ]
    | unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; apply Rabs_right;
      apply Rle_ge; left; apply (cond_pos (vn n)) ].
  rewrite StepFun_P39; rewrite Rabs_Ropp;
    apply Rle_lt_trans with
      (RiemannInt_SF
        (mkStepFun
          (StepFun_P32
            (mkStepFun
              (StepFun_P6
                (pre
                  (mkStepFun
                    (StepFun_P28 (-1) (phi_sequence vn pr2 n)
                      (phi_sequence un pr1 n))))))))).
  apply StepFun_P34; try auto with real.
  apply Rle_lt_trans with
    (RiemannInt_SF
      (mkStepFun (StepFun_P6 (pre (mkStepFun (StepFun_P28 1 psi_vn psi_un)))))).
  apply StepFun_P37.
  auto with real.
  intros; simpl; rewrite Rmult_1_l;
    apply Rle_trans with
      (Rabs (phi_sequence vn pr2 n x - f x) +
        Rabs (f x - phi_sequence un pr1 n x)).
  replace (phi_sequence vn pr2 n x + -1 * phi_sequence un pr1 n x) with
  (phi_sequence vn pr2 n x - f x + (f x - phi_sequence un pr1 n x));
  [ apply Rabs_triang | ring ].
  assert (H10 : Rmin a b = b).
  unfold Rmin; decide (Rle_dec a b) with Hnle; reflexivity.
  assert (H11 : Rmax a b = a).
  unfold Rmax; decide (Rle_dec a b) with Hnle; reflexivity.
  apply Rplus_le_compat.
  rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; elim H5; intros; apply H8.
  rewrite H10; rewrite H11; elim H7; intros; split; left; assumption.
  elim H6; intros; apply H8.
  rewrite H10; rewrite H11; elim H7; intros; split; left; assumption.
  rewrite <-
    (Ropp_involutive
      (RiemannInt_SF
        (mkStepFun
          (StepFun_P6 (pre (mkStepFun (StepFun_P28 1 psi_vn psi_un)))))))
    ; rewrite <- StepFun_P39; rewrite StepFun_P30; rewrite Rmult_1_l;
      rewrite double; rewrite Ropp_plus_distr; apply Rplus_lt_compat.
  apply Rlt_trans with (pos (vn n)).
  elim H5; intros; apply Rle_lt_trans with (Rabs (RiemannInt_SF psi_vn)).
  rewrite <- Rabs_Ropp; apply RRle_abs.
  assumption.
  replace (pos (vn n)) with (Rabs (vn n - 0));
  [ apply H0; unfold ge; apply le_trans with N; try assumption;
    unfold N; apply le_trans with (max N0 N1);
      [ apply le_max_r | apply le_max_l ]
    | unfold R_dist; unfold Rminus; rewrite Ropp_0;
      rewrite Rplus_0_r; apply Rabs_right; apply Rle_ge;
        left; apply (cond_pos (vn n)) ].
  apply Rlt_trans with (pos (un n)).
  elim H6; intros; apply Rle_lt_trans with (Rabs (RiemannInt_SF psi_un)).
  rewrite <- Rabs_Ropp; apply RRle_abs; assumption.
  assumption.
  replace (pos (un n)) with (Rabs (un n - 0));
  [ apply H; unfold ge; apply le_trans with N; try assumption;
    unfold N; apply le_trans with (max N0 N1);
      apply le_max_l
    | unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; apply Rabs_right;
      apply Rle_ge; left; apply (cond_pos (un n)) ].
  apply H1; unfold ge; apply le_trans with N; try assumption;
    unfold N; apply le_max_r.
  apply Rmult_eq_reg_l with 3;
    [ unfold Rdiv; rewrite Rmult_plus_distr_l;
      do 2 rewrite (Rmult_comm 3); repeat rewrite Rmult_assoc;
        rewrite <- Rinv_l_sym; [ ring | discrR ]
      | discrR ].
Qed.

Lemma RinvN_pos : forall n:nat, 0 < / (INR n + 1).
Proof.
  intro; apply Rinv_0_lt_compat; apply Rplus_le_lt_0_compat;
    [ apply pos_INR | apply Rlt_0_1 ].
Qed.

Definition RinvN (N:nat) : posreal := mkposreal _ (RinvN_pos N).

Lemma RinvN_cv : Un_cv RinvN 0.
Proof.
  unfold Un_cv; intros; assert (H0 := archimed (/ eps)); elim H0;
    clear H0; intros; assert (H2 : (0 <= up (/ eps))%Z).
  apply le_IZR; left; apply Rlt_trans with (/ eps);
    [ apply Rinv_0_lt_compat; assumption | assumption ].
  elim (IZN _ H2); intros; exists x; intros; unfold R_dist;
    simpl; unfold Rminus; rewrite Ropp_0;
      rewrite Rplus_0_r; assert (H5 : 0 < INR n + 1).
  apply Rplus_le_lt_0_compat; [ apply pos_INR | apply Rlt_0_1 ].
  rewrite Rabs_right;
    [ idtac
      | left; change (0 < / (INR n + 1)); apply Rinv_0_lt_compat;
        assumption ]; apply Rle_lt_trans with (/ (INR x + 1)).
  apply Rinv_le_contravar.
  apply Rplus_le_lt_0_compat; [ apply pos_INR | apply Rlt_0_1 ].
  apply Rplus_le_compat_r; apply le_INR; apply H4.
  rewrite <- (Rinv_involutive eps).
  apply Rinv_lt_contravar.
  apply Rmult_lt_0_compat.
  apply Rinv_0_lt_compat; assumption.
  apply Rplus_le_lt_0_compat; [ apply pos_INR | apply Rlt_0_1 ].
  apply Rlt_trans with (INR x);
    [ rewrite INR_IZR_INZ; rewrite <- H3; apply H0
      | pattern (INR x) at 1; rewrite <- Rplus_0_r;
        apply Rplus_lt_compat_l; apply Rlt_0_1 ].
  red; intro; rewrite H6 in H; elim (Rlt_irrefl _ H).
Qed.

Lemma Riemann_integrable_ext :
  forall f g a b, 
    (forall x, Rmin a b <= x <= Rmax a b -> f x = g x) ->
    Riemann_integrable f a b -> Riemann_integrable g a b.
intros f g a b fg rif eps; destruct (rif eps) as [phi [psi [P1 P2]]].
exists phi; exists psi;split;[ | assumption ].
intros t intt; rewrite <- fg;[ | assumption].
apply P1; assumption.
Qed.
(**********)
Definition RiemannInt (f:R -> R) (a b:R) (pr:Riemann_integrable f a b) : R :=
  let (a,_) := RiemannInt_exists pr RinvN RinvN_cv in a.

Lemma RiemannInt_P5 :
  forall (f:R -> R) (a b:R) (pr1 pr2:Riemann_integrable f a b),
    RiemannInt pr1 = RiemannInt pr2.
Proof.
  intros; unfold RiemannInt;
    case (RiemannInt_exists pr1 RinvN RinvN_cv) as (x,HUn);
    case (RiemannInt_exists pr2 RinvN RinvN_cv) as (x0,HUn0);
      eapply UL_sequence;
        [ apply HUn
          | apply RiemannInt_P4 with pr2 RinvN; apply RinvN_cv || assumption ].
Qed.

(***************************************)
(** C°([a,b]) is included in L1([a,b]) *)
(***************************************)

Lemma maxN :
  forall (a b:R) (del:posreal),
    a < b -> { n:nat | a + INR n * del < b /\ b <= a + INR (S n) * del }.
Proof.
  intros; set (I := fun n:nat => a + INR n * del < b);
    assert (H0 :  exists n : nat, I n).
  exists 0%nat; unfold I; rewrite Rmult_0_l; rewrite Rplus_0_r;
    assumption.
  cut (Nbound I).
  intro; assert (H2 := Nzorn H0 H1); elim H2; intros x p; exists x; elim p; intros;
    split.
  apply H3.
  destruct (total_order_T (a + INR (S x) * del) b) as [[Hlt|Heq]|Hgt].
  assert (H5 := H4 (S x) Hlt); elim (le_Sn_n _ H5).
  right; symmetry ; assumption.
  left; apply Hgt.
  assert (H1 : 0 <= (b - a) / del).
  unfold Rdiv; apply Rmult_le_pos;
    [ apply Rge_le; apply Rge_minus; apply Rle_ge; left; apply H
      | left; apply Rinv_0_lt_compat; apply (cond_pos del) ].
  elim (archimed ((b - a) / del)); intros;
    assert (H4 : (0 <= up ((b - a) / del))%Z).
  apply le_IZR; simpl; left; apply Rle_lt_trans with ((b - a) / del);
    assumption.
  assert (H5 := IZN _ H4); elim H5; clear H5; intros N H5;
    unfold Nbound; exists N; intros; unfold I in H6;
      apply INR_le; rewrite H5 in H2; rewrite <- INR_IZR_INZ in H2;
        left; apply Rle_lt_trans with ((b - a) / del); try assumption;
          apply Rmult_le_reg_l with (pos del);
            [ apply (cond_pos del)
              | unfold Rdiv; rewrite <- (Rmult_comm (/ del));
                rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym;
                  [ rewrite Rmult_1_l; rewrite Rmult_comm; apply Rplus_le_reg_l with a;
                    replace (a + (b - a)) with b; [ left; assumption | ring ]
                    | assert (H7 := cond_pos del); red; intro; rewrite H8 in H7;
                      elim (Rlt_irrefl _ H7) ] ].
Qed.

Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) : Rlist :=
  match N with
    | O => cons y nil
    | S p => cons x (SubEquiN p (x + del) y del)
  end.

Definition max_N (a b:R) (del:posreal) (h:a < b) : nat :=
  let (N,_) := maxN del h in N.

Definition SubEqui (a b:R) (del:posreal) (h:a < b) : Rlist :=
  SubEquiN (S (max_N del h)) a b del.

Lemma Heine_cor1 :
  forall (f:R -> R) (a b:R),
    a < b ->
    (forall x:R, a <= x <= b -> continuity_pt f x) ->
    forall eps:posreal,
      { delta:posreal |
        delta <= b - a /\
        (forall x y:R,
          a <= x <= b ->
          a <= y <= b -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps) }.
Proof.
  intro f; intros;
    set
      (E :=
        fun l:R =>
          0 < l <= b - a /\
          (forall x y:R,
            a <= x <= b ->
            a <= y <= b -> Rabs (x - y) < l -> Rabs (f x - f y) < eps));
      assert (H1 : bound E).
  unfold bound; exists (b - a); unfold is_upper_bound; intros;
    unfold E in H1; elim H1; clear H1; intros H1 _; elim H1;
      intros; assumption.
  assert (H2 :  exists x : R, E x).
  assert (H2 := Heine f (fun x:R => a <= x <= b) (compact_P3 a b) H0 eps);
    elim H2; intros; exists (Rmin x (b - a)); unfold E;
      split;
        [ split;
          [ unfold Rmin; case (Rle_dec x (b - a)); intro;
            [ apply (cond_pos x) | apply Rlt_Rminus; assumption ]
            | apply Rmin_r ]
          | intros; apply H3; try assumption; apply Rlt_le_trans with (Rmin x (b - a));
            [ assumption | apply Rmin_l ] ].
  assert (H3 := completeness E H1 H2); elim H3; intros x p; cut (0 < x <= b - a).
  intro; elim H4; clear H4; intros; exists (mkposreal _ H4); split.
  apply H5.
  unfold is_lub in p; elim p; intros; unfold is_upper_bound in H6;
    set (D := Rabs (x0 - y)).
  assert (H11: ((exists y : R, D < y /\ E y) \/ (forall y : R, not (D < y /\ E y)) -> False) -> False).
    clear; intros H; apply H.
    right; intros y0 H0; apply H.
    left; now exists y0.
  apply Rnot_le_lt; intros H30.
  apply H11; clear H11; intros H11.
  revert H30; apply Rlt_not_le.
  destruct H11 as [H11|H12].
  elim H11; intros; elim H12; clear H12; intros; unfold E in H13; elim H13;
    intros; apply H15; assumption.
  assert (H13 : is_upper_bound E D).
  unfold is_upper_bound; intros; assert (H14 := H12 x1);
    apply Rnot_lt_le; contradict H14; now split.
  assert (H14 := H7 _ H13); elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H14 H10)).
  unfold is_lub in p; unfold is_upper_bound in p; elim p; clear p; intros;
    split.
  elim H2; intros; assert (H7 := H4 _ H6); unfold E in H6; elim H6; clear H6;
    intros H6 _; elim H6; intros; apply Rlt_le_trans with x0;
      assumption.
  apply H5; intros; unfold E in H6; elim H6; clear H6; intros H6 _; elim H6;
    intros; assumption.
Qed.

Lemma Heine_cor2 :
  forall (f:R -> R) (a b:R),
    (forall x:R, a <= x <= b -> continuity_pt f x) ->
    forall eps:posreal,
      { delta:posreal |
        forall x y:R,
          a <= x <= b ->
          a <= y <= b -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps }.
Proof.
  intro f; intros; destruct (total_order_T a b) as [[Hlt|Heq]|Hgt].
  assert (H0 := Heine_cor1 Hlt H eps); elim H0; intros x p; exists x;
    elim p; intros; apply H2; assumption.
  exists (mkposreal _ Rlt_0_1); intros; assert (H3 : x = y);
    [ elim H0; elim H1; intros; rewrite Heq in H3, H5;
      apply Rle_antisym; apply Rle_trans with b; assumption
      | rewrite H3; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0;
        apply (cond_pos eps) ].
  exists (mkposreal _ Rlt_0_1); intros; elim H0; intros;
    elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ (Rle_trans _ _ _ H3 H4) Hgt)).
Qed.

Lemma SubEqui_P1 :
  forall (a b:R) (del:posreal) (h:a < b), pos_Rl (SubEqui del h) 0 = a.
Proof.
  intros; unfold SubEqui; case (maxN del h); intros; reflexivity.
Qed.

Lemma SubEqui_P2 :
  forall (a b:R) (del:posreal) (h:a < b),
    pos_Rl (SubEqui del h) (pred (Rlength (SubEqui del h))) = b.
Proof.
  intros; unfold SubEqui; destruct (maxN del h)as (x,_).
    cut
      (forall (x:nat) (a:R) (del:posreal),
        pos_Rl (SubEquiN (S x) a b del)
        (pred (Rlength (SubEquiN (S x) a b del))) = b);
      [ intro; apply H
        | simple induction x0;
          [ intros; reflexivity
            | intros;
              change
                (pos_Rl (SubEquiN (S n) (a0 + del0) b del0)
                  (pred (Rlength (SubEquiN (S n) (a0 + del0) b del0))) = b)
               ; apply H ] ].
Qed.

Lemma SubEqui_P3 :
  forall (N:nat) (a b:R) (del:posreal), Rlength (SubEquiN N a b del) = S N.
Proof.
  simple induction N; intros;
    [ reflexivity | simpl; rewrite H; reflexivity ].
Qed.

Lemma SubEqui_P4 :
  forall (N:nat) (a b:R) (del:posreal) (i:nat),
    (i < S N)%nat -> pos_Rl (SubEquiN (S N) a b del) i = a + INR i * del.
Proof.
  simple induction N;
    [ intros; inversion H; [ simpl; ring | elim (le_Sn_O _ H1) ]
      | intros; induction  i as [| i Hreci];
        [ simpl; ring
          | change
            (pos_Rl (SubEquiN (S n) (a + del) b del) i = a + INR (S i) * del)
           ; rewrite H; [ rewrite S_INR; ring | apply lt_S_n; apply H0 ] ] ].
Qed.

Lemma SubEqui_P5 :
  forall (a b:R) (del:posreal) (h:a < b),
    Rlength (SubEqui del h) = S (S (max_N del h)).
Proof.
  intros; unfold SubEqui; apply SubEqui_P3.
Qed.

Lemma SubEqui_P6 :
  forall (a b:R) (del:posreal) (h:a < b) (i:nat),
    (i < S (max_N del h))%nat -> pos_Rl (SubEqui del h) i = a + INR i * del.
Proof.
  intros; unfold SubEqui; apply SubEqui_P4; assumption.
Qed.

Lemma SubEqui_P7 :
  forall (a b:R) (del:posreal) (h:a < b), ordered_Rlist (SubEqui del h).
Proof.
  intros; unfold ordered_Rlist; intros; rewrite SubEqui_P5 in H;
    simpl in H; inversion H.
  rewrite (SubEqui_P6 del h (i:=(max_N del h))).
  replace (S (max_N del h)) with (pred (Rlength (SubEqui del h))).
  rewrite SubEqui_P2; unfold max_N; case (maxN del h) as (?&?&?); left;
    assumption.
  rewrite SubEqui_P5; reflexivity.
  apply lt_n_Sn.
  repeat rewrite SubEqui_P6.
  3: assumption.
  2: apply le_lt_n_Sm; assumption.
  apply Rplus_le_compat_l; rewrite S_INR; rewrite Rmult_plus_distr_r;
    pattern (INR i * del) at 1; rewrite <- Rplus_0_r;
      apply Rplus_le_compat_l; rewrite Rmult_1_l; left;
        apply (cond_pos del).
Qed.

Lemma SubEqui_P8 :
  forall (a b:R) (del:posreal) (h:a < b) (i:nat),
    (i < Rlength (SubEqui del h))%nat -> a <= pos_Rl (SubEqui del h) i <= b.
Proof.
  intros; split.
  pattern a at 1; rewrite <- (SubEqui_P1 del h); apply RList_P5.
  apply SubEqui_P7.
  elim (RList_P3 (SubEqui del h) (pos_Rl (SubEqui del h) i)); intros; apply H1;
    exists i; split; [ reflexivity | assumption ].
  pattern b at 2; rewrite <- (SubEqui_P2 del h); apply RList_P7;
    [ apply SubEqui_P7
      | elim (RList_P3 (SubEqui del h) (pos_Rl (SubEqui del h) i)); intros;
        apply H1; exists i; split; [ reflexivity | assumption ] ].
Qed.

Lemma SubEqui_P9 :
  forall (a b:R) (del:posreal) (f:R -> R) (h:a < b),
    { g:StepFun a b |
      g b = f b /\
      (forall i:nat,
        (i < pred (Rlength (SubEqui del h)))%nat ->
        constant_D_eq g
        (co_interval (pos_Rl (SubEqui del h) i)
          (pos_Rl (SubEqui del h) (S i)))
        (f (pos_Rl (SubEqui del h) i))) }.
Proof.
  intros; apply StepFun_P38;
    [ apply SubEqui_P7 | apply SubEqui_P1 | apply SubEqui_P2 ].
Qed.

Lemma RiemannInt_P6 :
  forall (f:R -> R) (a b:R),
    a < b ->
    (forall x:R, a <= x <= b -> continuity_pt f x) -> Riemann_integrable f a b.
Proof.
  intros; unfold Riemann_integrable; intro;
    assert (H1 : 0 < eps / (2 * (b - a))).
  unfold Rdiv; apply Rmult_lt_0_compat;
    [ apply (cond_pos eps)
      | apply Rinv_0_lt_compat; apply Rmult_lt_0_compat;
        [ prove_sup0 | apply Rlt_Rminus; assumption ] ].
  assert (H2 : Rmin a b = a).
  apply Rlt_le in H.
  unfold Rmin; decide (Rle_dec a b) with H; reflexivity.
  assert (H3 : Rmax a b = b).
  apply Rlt_le in H.
  unfold Rmax; decide (Rle_dec a b) with H; reflexivity.
  elim (Heine_cor2 H0 (mkposreal _ H1)); intros del H4;
    elim (SubEqui_P9 del f H); intros phi [H5 H6]; split with phi;
      split with (mkStepFun (StepFun_P4 a b (eps / (2 * (b - a)))));
        split.
  2: rewrite StepFun_P18; unfold Rdiv; rewrite Rinv_mult_distr.
  2: do 2 rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
  2: rewrite Rmult_1_r; rewrite Rabs_right.
  2: apply Rmult_lt_reg_l with 2.
  2: prove_sup0.
  2: rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
    rewrite <- Rinv_r_sym.
  2: rewrite Rmult_1_l; pattern (pos eps) at 1; rewrite <- Rplus_0_r;
    rewrite double; apply Rplus_lt_compat_l; apply (cond_pos eps).
  2: discrR.
  2: apply Rle_ge; left; apply Rmult_lt_0_compat.
  2: apply (cond_pos eps).
  2: apply Rinv_0_lt_compat; prove_sup0.
  2: apply Rminus_eq_contra; red; intro; clear H6; rewrite H7 in H;
    elim (Rlt_irrefl _ H).
  2: discrR.
  2: apply Rminus_eq_contra; red; intro; clear H6; rewrite H7 in H;
    elim (Rlt_irrefl _ H).
  intros; rewrite H2 in H7; rewrite H3 in H7; simpl;
    unfold fct_cte;
      cut
        (forall t:R,
          a <= t <= b ->
          t = b \/
          (exists i : nat,
            (i < pred (Rlength (SubEqui del H)))%nat /\
            co_interval (pos_Rl (SubEqui del H) i) (pos_Rl (SubEqui del H) (S i))
            t)).
  intro; elim (H8 _ H7); intro.
  rewrite H9; rewrite H5; unfold Rminus; rewrite Rplus_opp_r;
    rewrite Rabs_R0; left; assumption.
  elim H9; clear H9; intros I [H9 H10]; assert (H11 := H6 I H9 t H10);
    rewrite H11; left; apply H4.
  assumption.
  apply SubEqui_P8; apply lt_trans with (pred (Rlength (SubEqui del H))).
  assumption.
  apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H12 in H9;
    elim (lt_n_O _ H9).
  unfold co_interval in H10; elim H10; clear H10; intros; rewrite Rabs_right.
  rewrite SubEqui_P5 in H9; simpl in H9; inversion H9.
  apply Rplus_lt_reg_l with (pos_Rl (SubEqui del H) (max_N del H)).
  replace
  (pos_Rl (SubEqui del H) (max_N del H) +
    (t - pos_Rl (SubEqui del H) (max_N del H))) with t;
  [ idtac | ring ]; apply Rlt_le_trans with b.
  rewrite H14 in H12;
    assert (H13 : S (max_N del H) = pred (Rlength (SubEqui del H))).
  rewrite SubEqui_P5; reflexivity.
  rewrite H13 in H12; rewrite SubEqui_P2 in H12; apply H12.
  rewrite SubEqui_P6.
  2: apply lt_n_Sn.
  unfold max_N; destruct (maxN del H) as (?&?&H13);
    replace (a + INR x * del + del) with (a + INR (S x) * del);
      [ assumption | rewrite S_INR; ring ].
  apply Rplus_lt_reg_l with (pos_Rl (SubEqui del H) I);
    replace (pos_Rl (SubEqui del H) I + (t - pos_Rl (SubEqui del H) I)) with t;
    [ idtac | ring ];
    replace (pos_Rl (SubEqui del H) I + del) with (pos_Rl (SubEqui del H) (S I)).
  assumption.
  repeat rewrite SubEqui_P6.
  rewrite S_INR; ring.
  assumption.
  apply le_lt_n_Sm; assumption.
  apply Rge_minus; apply Rle_ge; assumption.
  intros; clear H0 H1 H4 phi H5 H6 t H7; case (Req_dec t0 b); intro.
  left; assumption.
  right; set (I := fun j:nat => a + INR j * del <= t0);
    assert (H1 :  exists n : nat, I n).
  exists 0%nat; unfold I; rewrite Rmult_0_l; rewrite Rplus_0_r; elim H8;
    intros; assumption.
  assert (H4 : Nbound I).
  unfold Nbound; exists (S (max_N del H)); intros; unfold max_N;
    destruct (maxN del H) as (?&_&H5);
      apply INR_le; apply Rmult_le_reg_l with (pos del).
  apply (cond_pos del).
  apply Rplus_le_reg_l with a; do 2 rewrite (Rmult_comm del);
    apply Rle_trans with t0; unfold I in H4; try assumption;
      apply Rle_trans with b; try assumption; elim H8; intros;
        assumption.
  elim (Nzorn H1 H4); intros N [H5 H6]; assert (H7 : (N < S (max_N del H))%nat).
  unfold max_N; case (maxN del H) as (?&?&?); apply INR_lt;
    apply Rmult_lt_reg_l with (pos del).
  apply (cond_pos del).
  apply Rplus_lt_reg_l with a; do 2 rewrite (Rmult_comm del);
    apply Rle_lt_trans with t0; unfold I in H5; try assumption;
      apply Rlt_le_trans with b; try assumption;
        elim H8; intros.
  elim H11; intro.
  assumption.
  elim H0; assumption.
  exists N; split.
  rewrite SubEqui_P5; simpl; assumption.
  unfold co_interval; split.
  rewrite SubEqui_P6.
  apply H5.
  assumption.
  inversion H7.
  replace (S (max_N del H)) with (pred (Rlength (SubEqui del H))).
  rewrite (SubEqui_P2 del H); elim H8; intros.
  elim H11; intro.
  assumption.
  elim H0; assumption.
  rewrite SubEqui_P5; reflexivity.
  rewrite SubEqui_P6.
  destruct (Rle_dec (a + INR (S N) * del) t0) as [Hle|Hnle].
  assert (H11 := H6 (S N) Hle); elim (le_Sn_n _ H11).
  auto with real.
  apply le_lt_n_Sm; assumption.
Qed.

Lemma RiemannInt_P7 : forall (f:R -> R) (a:R), Riemann_integrable f a a.
Proof.
  unfold Riemann_integrable; intro f; intros;
    split with (mkStepFun (StepFun_P4 a a (f a)));
      split with (mkStepFun (StepFun_P4 a a 0)); split.
  intros; simpl; unfold fct_cte; replace t with a.
  unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; right;
    reflexivity.
  generalize H; unfold Rmin, Rmax; decide (Rle_dec a a) with (Rle_refl a).
    intros (?,?); apply Rle_antisym; assumption.
  rewrite StepFun_P18; rewrite Rmult_0_l; rewrite Rabs_R0; apply (cond_pos eps).
Qed.

Lemma continuity_implies_RiemannInt :
  forall (f:R -> R) (a b:R),
    a <= b ->
    (forall x:R, a <= x <= b -> continuity_pt f x) -> Riemann_integrable f a b.
Proof.
  intros; destruct (total_order_T a b) as [[Hlt| -> ]|Hgt];
      [ apply RiemannInt_P6; assumption | apply RiemannInt_P7
      | elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgt)) ].
Qed.

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.
  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)).
  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)).
  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 R_dist 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 R_dist;
      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).
  apply Rplus_lt_compat.
  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 double; 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 le_trans with (max N0 N1);
            [ apply 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 le_trans with (max N0 N1);
                  [ apply 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 double; 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 le_trans with (max N0 N1);
                  [ apply 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 le_trans with (max N0 N1);
            [ apply le_max_l | assumption ] ] ].
  unfold R_dist in H1; apply H1; unfold ge;
    apply le_trans with (max N0 N1); [ apply le_max_r | assumption ].
  apply Rmult_eq_reg_l with 3;
    [ unfold Rdiv; rewrite Rmult_plus_distr_l;
      do 2 rewrite (Rmult_comm 3); repeat rewrite Rmult_assoc;
        rewrite <- Rinv_l_sym; [ ring | discrR ]
      | discrR ].
  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)).
  split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr1 n)); intro;
    apply (proj2_sig (phi_sequence_prop RinvN pr1 n)).
Qed.

Lemma RiemannInt_P9 :
  forall (f:R -> R) (a:R) (pr:Riemann_integrable f a a), RiemannInt pr = 0.
Proof.
  intros; assert (H := RiemannInt_P8 pr pr); apply Rmult_eq_reg_l with 2;
    [ rewrite Rmult_0_r; rewrite double; pattern (RiemannInt pr) at 2;
      rewrite H; apply Rplus_opp_r
      | discrR ].
Qed.

(* L1([a,b]) is a vectorial space *)
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.
  unfold Riemann_integrable; intros f g; intros; destruct (Req_EM_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 (double_var 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_sym;
    [ rewrite Rmult_1_l;
      replace (/ Rabs l * (eps / 2)) with (eps / (2 * Rabs l));
      [ apply H2
        | unfold Rdiv; rewrite Rinv_mult_distr;
          [ ring | discrR | apply Rabs_no_R0; assumption ] ]
      | apply Rabs_no_R0; assumption ].
Qed.

Lemma RiemannInt_P11 :
  forall (f:R -> R) (a b l:R) (un:nat -> posreal)
    (phi1 phi2 psi1 psi2:nat -> StepFun a b),
    Un_cv un 0 ->
    (forall n:nat,
      (forall t:R,
        Rmin a b <= t <= Rmax a b -> Rabs (f t - phi1 n t) <= psi1 n t) /\
      Rabs (RiemannInt_SF (psi1 n)) < un n) ->
    (forall n:nat,
      (forall t:R,
        Rmin a b <= t <= Rmax a b -> Rabs (f t - phi2 n t) <= psi2 n t) /\
      Rabs (RiemannInt_SF (psi2 n)) < un n) ->
    Un_cv (fun N:nat => RiemannInt_SF (phi1 N)) l ->
    Un_cv (fun N:nat => RiemannInt_SF (phi2 N)) l.
Proof.
  unfold Un_cv; intro f; intros; intros.
  case (Rle_dec a b); intro Hyp.
  assert (H4 : 0 < eps / 3).
  unfold Rdiv; apply Rmult_lt_0_compat;
    [ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
  elim (H _ H4); clear H; intros N0 H.
  elim (H2 _ H4); clear H2; intros N1 H2.
  set (N := max N0 N1); exists N; intros; unfold R_dist.
  apply Rle_lt_trans with
    (Rabs (RiemannInt_SF (phi2 n) - RiemannInt_SF (phi1 n)) +
      Rabs (RiemannInt_SF (phi1 n) - l)).
  replace (RiemannInt_SF (phi2 n) - l) with
  (RiemannInt_SF (phi2 n) - RiemannInt_SF (phi1 n) +
    (RiemannInt_SF (phi1 n) - l)); [ apply Rabs_triang | ring ].
  replace eps with (2 * (eps / 3) + eps / 3).
  apply Rplus_lt_compat.
  replace (RiemannInt_SF (phi2 n) - RiemannInt_SF (phi1 n)) with
  (RiemannInt_SF (phi2 n) + -1 * RiemannInt_SF (phi1 n));
  [ idtac | ring ].
  rewrite <- StepFun_P30.
  apply Rle_lt_trans with
    (RiemannInt_SF
      (mkStepFun (StepFun_P32 (mkStepFun (StepFun_P28 (-1) (phi2 n) (phi1 n)))))).
  apply StepFun_P34; assumption.
  apply Rle_lt_trans with
    (RiemannInt_SF (mkStepFun (StepFun_P28 1 (psi1 n) (psi2 n)))).
  apply StepFun_P37; try assumption; intros; simpl; rewrite Rmult_1_l.
  apply Rle_trans with (Rabs (phi2 n x - f x) + Rabs (f x - phi1 n x)).
  replace (phi2 n x + -1 * phi1 n x) with (phi2 n x - f x + (f x - phi1 n x));
  [ apply Rabs_triang | ring ].
  rewrite (Rplus_comm (psi1 n x)); apply Rplus_le_compat.
  rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; elim (H1 n); intros; apply H7.
  assert (H10 : Rmin a b = a).
  unfold Rmin; decide (Rle_dec a b) with Hyp; reflexivity.
  assert (H11 : Rmax a b = b).
  unfold Rmax; decide (Rle_dec a b) with Hyp; reflexivity.
  rewrite H10; rewrite H11; elim H6; intros; split; left; assumption.
  elim (H0 n); intros; apply H7; assert (H10 : Rmin a b = a).
  unfold Rmin; decide (Rle_dec a b) with Hyp; reflexivity.
  assert (H11 : Rmax a b = b).
  unfold Rmax; decide (Rle_dec a b) with Hyp; reflexivity.
  rewrite H10; rewrite H11; elim H6; intros; split; left; assumption.
  rewrite StepFun_P30; rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat.
  apply Rlt_trans with (pos (un n)).
  elim (H0 n); intros; apply Rle_lt_trans with (Rabs (RiemannInt_SF (psi1 n))).
  apply RRle_abs.
  assumption.
  replace (pos (un n)) with (R_dist (un n) 0).
  apply H; unfold ge; apply le_trans with N; try assumption.
  unfold N; apply le_max_l.
  unfold R_dist; unfold Rminus; rewrite Ropp_0;
    rewrite Rplus_0_r; apply Rabs_right.
  apply Rle_ge; left; apply (cond_pos (un n)).
  apply Rlt_trans with (pos (un n)).
  elim (H1 n); intros; apply Rle_lt_trans with (Rabs (RiemannInt_SF (psi2 n))).
  apply RRle_abs; assumption.
  assumption.
  replace (pos (un n)) with (R_dist (un n) 0).
  apply H; unfold ge; apply le_trans with N; try assumption;
    unfold N; apply le_max_l.
  unfold R_dist; unfold Rminus; rewrite Ropp_0;
    rewrite Rplus_0_r; apply Rabs_right; apply Rle_ge;
      left; apply (cond_pos (un n)).
  unfold R_dist in H2; apply H2; unfold ge; apply le_trans with N;
    try assumption; unfold N; apply le_max_r.
  apply Rmult_eq_reg_l with 3;
    [ unfold Rdiv; rewrite Rmult_plus_distr_l;
      do 2 rewrite (Rmult_comm 3); repeat rewrite Rmult_assoc;
        rewrite <- Rinv_l_sym; [ ring | discrR ]
      | discrR ].
  assert (H4 : 0 < eps / 3).
  unfold Rdiv; apply Rmult_lt_0_compat;
    [ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
  elim (H _ H4); clear H; intros N0 H.
  elim (H2 _ H4); clear H2; intros N1 H2.
  set (N := max N0 N1); exists N; intros; unfold R_dist.
  apply Rle_lt_trans with
    (Rabs (RiemannInt_SF (phi2 n) - RiemannInt_SF (phi1 n)) +
      Rabs (RiemannInt_SF (phi1 n) - l)).
  replace (RiemannInt_SF (phi2 n) - l) with
  (RiemannInt_SF (phi2 n) - RiemannInt_SF (phi1 n) +
    (RiemannInt_SF (phi1 n) - l)); [ apply Rabs_triang | ring ].
  assert (Hyp_b : b <= a).
  auto with real.
  replace eps with (2 * (eps / 3) + eps / 3).
  apply Rplus_lt_compat.
  replace (RiemannInt_SF (phi2 n) - RiemannInt_SF (phi1 n)) with
  (RiemannInt_SF (phi2 n) + -1 * RiemannInt_SF (phi1 n));
  [ idtac | ring ].
  rewrite <- StepFun_P30.
  rewrite StepFun_P39.
  rewrite Rabs_Ropp.
  apply Rle_lt_trans with
    (RiemannInt_SF
      (mkStepFun
        (StepFun_P32
          (mkStepFun
            (StepFun_P6
              (pre (mkStepFun (StepFun_P28 (-1) (phi2 n) (phi1 n))))))))).
  apply StepFun_P34; try assumption.
  apply Rle_lt_trans with
    (RiemannInt_SF
      (mkStepFun
        (StepFun_P6 (pre (mkStepFun (StepFun_P28 1 (psi1 n) (psi2 n))))))).
  apply StepFun_P37; try assumption.
  intros; simpl; rewrite Rmult_1_l.
  apply Rle_trans with (Rabs (phi2 n x - f x) + Rabs (f x - phi1 n x)).
  replace (phi2 n x + -1 * phi1 n x) with (phi2 n x - f x + (f x - phi1 n x));
  [ apply Rabs_triang | ring ].
  rewrite (Rplus_comm (psi1 n x)); apply Rplus_le_compat.
  rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; elim (H1 n); intros; apply H7.
  assert (H10 : Rmin a b = b).
  unfold Rmin; case (Rle_dec a b); intro;
    [ elim Hyp; assumption | reflexivity ].
  assert (H11 : Rmax a b = a).
  unfold Rmax; case (Rle_dec a b); intro;
    [ elim Hyp; assumption | reflexivity ].
  rewrite H10; rewrite H11; elim H6; intros; split; left; assumption.
  elim (H0 n); intros; apply H7; assert (H10 : Rmin a b = b).
  unfold Rmin; case (Rle_dec a b); intro;
    [ elim Hyp; assumption | reflexivity ].
  assert (H11 : Rmax a b = a).
  unfold Rmax; case (Rle_dec a b); intro;
    [ elim Hyp; assumption | reflexivity ].
  rewrite H10; rewrite H11; elim H6; intros; split; left; assumption.
  rewrite <-
    (Ropp_involutive
      (RiemannInt_SF
        (mkStepFun
          (StepFun_P6 (pre (mkStepFun (StepFun_P28 1 (psi1 n) (psi2 n))))))))
    .
  rewrite <- StepFun_P39.
  rewrite StepFun_P30.
  rewrite Rmult_1_l; rewrite double.
  rewrite Ropp_plus_distr; apply Rplus_lt_compat.
  apply Rlt_trans with (pos (un n)).
  elim (H0 n); intros; apply Rle_lt_trans with (Rabs (RiemannInt_SF (psi1 n))).
  rewrite <- Rabs_Ropp; apply RRle_abs.
  assumption.
  replace (pos (un n)) with (R_dist (un n) 0).
  apply H; unfold ge; apply le_trans with N; try assumption.
  unfold N; apply le_max_l.
  unfold R_dist; unfold Rminus; rewrite Ropp_0;
    rewrite Rplus_0_r; apply Rabs_right.
  apply Rle_ge; left; apply (cond_pos (un n)).
  apply Rlt_trans with (pos (un n)).
  elim (H1 n); intros; apply Rle_lt_trans with (Rabs (RiemannInt_SF (psi2 n))).
  rewrite <- Rabs_Ropp; apply RRle_abs; assumption.
  assumption.
  replace (pos (un n)) with (R_dist (un n) 0).
  apply H; unfold ge; apply le_trans with N; try assumption;
    unfold N; apply le_max_l.
  unfold R_dist; unfold Rminus; rewrite Ropp_0;
    rewrite Rplus_0_r; apply Rabs_right; apply Rle_ge;
      left; apply (cond_pos (un n)).
  unfold R_dist in H2; apply H2; unfold ge; apply le_trans with N;
    try assumption; unfold N; apply le_max_r.
  apply Rmult_eq_reg_l with 3;
    [ unfold Rdiv; rewrite Rmult_plus_distr_l;
      do 2 rewrite (Rmult_comm 3); repeat rewrite Rmult_assoc;
        rewrite <- Rinv_l_sym; [ ring | discrR ]
      | discrR ].
Qed.

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.
  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 R_dist 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 R_dist.
  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).
  repeat apply Rplus_lt_compat.
  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));
    [ repeat apply Rplus_lt_compat | ring ].
  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 le_trans with N;
        [ apply le_trans with (max N0 N1);
          [ apply le_max_r | unfold N; apply 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 le_trans with N;
        [ apply le_trans with (max N0 N1);
          [ apply le_max_r | unfold N; apply 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_sym.
  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 le_trans with N;
        [ apply le_trans with (max N2 N3);
          [ apply le_max_r | unfold N; apply le_max_r ]
          | assumption ] ].
  unfold Rdiv; rewrite Rinv_mult_distr;
    [ ring | discrR | apply Rabs_no_R0; assumption ].
  apply Rabs_no_R0; assumption.
  apply H3; unfold ge; apply le_trans with (max N0 N1);
    [ apply le_max_l
      | apply le_trans with N; [ unfold N; apply 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_sym.
  rewrite Rmult_1_l; replace (/ Rabs l * (eps / 5)) with (eps / (5 * Rabs l)).
  apply H6; unfold ge; apply le_trans with (max N2 N3);
    [ apply le_max_l
      | apply le_trans with N; [ unfold N; apply le_max_r | assumption ] ].
  unfold Rdiv; rewrite Rinv_mult_distr;
    [ ring | discrR | apply Rabs_no_R0; assumption ].
  apply Rabs_no_R0; assumption.
  apply Rmult_eq_reg_l with 5;
    [ unfold Rdiv; do 2 rewrite Rmult_plus_distr_l;
      do 3 rewrite (Rmult_comm 5); repeat rewrite Rmult_assoc;
        rewrite <- Rinv_l_sym; [ ring | discrR ]
      | discrR ].
Qed.

Lemma RiemannInt_P13 :
  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),
    RiemannInt pr3 = RiemannInt pr1 + l * RiemannInt pr2.
Proof.
  intros; destruct (Rle_dec a b) as [Hle|Hnle];
    [ apply RiemannInt_P12; assumption
      | assert (H : b <= a);
        [ auto with real
          | replace (RiemannInt pr3) with (- RiemannInt (RiemannInt_P1 pr3));
            [ idtac | symmetry ; apply RiemannInt_P8 ];
            replace (RiemannInt pr2) with (- RiemannInt (RiemannInt_P1 pr2));
            [ idtac | symmetry ; apply RiemannInt_P8 ];
            replace (RiemannInt pr1) with (- RiemannInt (RiemannInt_P1 pr1));
            [ idtac | symmetry ; apply RiemannInt_P8 ];
            rewrite
              (RiemannInt_P12 (RiemannInt_P1 pr1) (RiemannInt_P1 pr2)
                (RiemannInt_P1 pr3) H); ring ] ].
Qed.

Lemma RiemannInt_P14 : forall a b c:R, Riemann_integrable (fct_cte c) a b.
Proof.
  unfold Riemann_integrable; intros;
    split with (mkStepFun (StepFun_P4 a b c));
      split with (mkStepFun (StepFun_P4 a b 0)); split;
        [ intros; simpl; unfold Rminus; rewrite Rplus_opp_r;
          rewrite Rabs_R0; unfold fct_cte; right;
            reflexivity
          | rewrite StepFun_P18; rewrite Rmult_0_l; rewrite Rabs_R0;
            apply (cond_pos eps) ].
Qed.

Lemma RiemannInt_P15 :
  forall (a b c:R) (pr:Riemann_integrable (fct_cte c) a b),
    RiemannInt pr = c * (b - a).
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;
          try assumption.
  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)).
  unfold Un_cv; intros; split with 0%nat; intros; unfold R_dist;
    unfold phi2; rewrite StepFun_P18; unfold Rminus;
      rewrite Rplus_opp_r; rewrite Rabs_R0; apply H.
Qed.

Lemma RiemannInt_P16 :
  forall (f:R -> R) (a b:R),
    Riemann_integrable f a b -> Riemann_integrable (fun x:R => Rabs (f x)) a b.
Proof.
  unfold Riemann_integrable; intro f; intros; elim (X eps); clear X;
    intros phi [psi [H H0]]; split with (mkStepFun (StepFun_P32 phi));
      split with psi; split; try assumption; intros; simpl;
        apply Rle_trans with (Rabs (f t - phi t));
          [ apply Rabs_triang_inv2 | apply H; assumption ].
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.103 Sekunden  (vorverarbeitet)  ¤



vermutete Sprache:
Sekunden
vermutete Sprache:
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff