|
(* -*- 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.70 Sekunden
(vorverarbeitet)
¤
|
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.
|
