diff options
Diffstat (limited to 'theories/Reals/RiemannInt.v')
| -rw-r--r-- | theories/Reals/RiemannInt.v | 217 |
1 files changed, 109 insertions, 108 deletions
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 8d069e2d..ae2c3d77 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: RiemannInt.v 10710 2008-03-23 09:24:09Z herbelin $ i*) +(*i $Id$ i*) Require Import Rfunctions. Require Import SeqSeries. @@ -32,8 +33,8 @@ Definition Riemann_integrable (f:R -> R) (a b:R) : Type := 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) := +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 : @@ -54,7 +55,7 @@ Lemma RiemannInt_P1 : Proof. unfold Riemann_integrable in |- *; intros; elim (X eps); clear X; intros; elim p; clear p; intros; exists (mkStepFun (StepFun_P6 (pre x))); - exists (mkStepFun (StepFun_P6 (pre x0))); + 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; @@ -97,7 +98,7 @@ Proof. elim (H _ H3); intros N0 H4; exists N0; intros; unfold R_dist in |- *; 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)); + (RiemannInt_SF (vn n) + -1 * RiemannInt_SF (vn m)); [ idtac | ring ]; rewrite <- StepFun_P30; apply Rle_lt_trans with (RiemannInt_SF @@ -131,7 +132,7 @@ Proof. 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; + rewrite (double_var eps); apply Rplus_lt_compat; apply H4; assumption. Qed. @@ -179,8 +180,8 @@ Proof. rewrite Rabs_Ropp in H4; apply H4. apply H4. assert (H3 := RiemannInt_P2 _ _ _ _ H H1 H2); elim H3; intros; - exists (- x); unfold Un_cv in |- *; unfold Un_cv in p; - intros; elim (p _ H4); intros; exists x0; intros; + exists (- x); unfold Un_cv in |- *; unfold Un_cv in p; + intros; elim (p _ H4); intros; exists x0; intros; generalize (H5 _ H6); unfold R_dist, RiemannInt_SF in |- *; case (Rle_dec b a); case (Rle_dec a b); intros. elim n; assumption. @@ -189,7 +190,7 @@ Proof. (Int_SF (subdivision_val (mkStepFun (StepFun_P6 (pre (vn n0))))) (subdivision (mkStepFun (StepFun_P6 (pre (vn n0)))))); [ unfold Rminus in |- *; rewrite Ropp_involutive; rewrite <- Rabs_Ropp; - rewrite Ropp_plus_distr; rewrite Ropp_involutive; + rewrite Ropp_plus_distr; rewrite Ropp_involutive; apply H7 | symmetry in |- *; apply StepFun_P17 with (fe (vn n0)) a b; [ apply StepFun_P1 @@ -200,7 +201,7 @@ Proof. Qed. Lemma RiemannInt_exists : - forall (f:R -> R) (a b:R) (pr:Riemann_integrable f a b) + 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 }. @@ -281,7 +282,7 @@ Proof. assumption. replace (pos (un n)) with (Rabs (un n - 0)); [ apply H; unfold ge in |- *; apply le_trans with N; try assumption; - unfold N in |- *; apply le_trans with (max N0 N1); + unfold N in |- *; apply le_trans with (max N0 N1); apply le_max_l | unfold Rminus in |- *; rewrite Ropp_0; rewrite Rplus_0_r; apply Rabs_right; apply Rle_ge; left; apply (cond_pos (un n)) ]. @@ -346,7 +347,7 @@ Proof. unfold N in |- *; apply le_trans with (max N0 N1); [ apply le_max_r | apply le_max_l ] | unfold R_dist in |- *; unfold Rminus in |- *; rewrite Ropp_0; - rewrite Rplus_0_r; apply Rabs_right; apply Rle_ge; + 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)). @@ -354,7 +355,7 @@ Proof. assumption. replace (pos (un n)) with (Rabs (un n - 0)); [ apply H; unfold ge in |- *; apply le_trans with N; try assumption; - unfold N in |- *; apply le_trans with (max N0 N1); + unfold N in |- *; apply le_trans with (max N0 N1); apply le_max_l | unfold Rminus in |- *; rewrite Ropp_0; rewrite Rplus_0_r; apply Rabs_right; apply Rle_ge; left; apply (cond_pos (un n)) ]. @@ -382,7 +383,7 @@ Proof. 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 in |- *; - simpl in |- *; unfold Rminus in |- *; rewrite Ropp_0; + simpl in |- *; unfold Rminus in |- *; 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; @@ -406,7 +407,7 @@ Proof. red in |- *; intro; rewrite H6 in H; elim (Rlt_irrefl _ H). 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. @@ -416,14 +417,14 @@ Lemma RiemannInt_P5 : Proof. intros; unfold RiemannInt in |- *; case (RiemannInt_exists pr1 RinvN RinvN_cv); - case (RiemannInt_exists pr2 RinvN RinvN_cv); intros; + case (RiemannInt_exists pr2 RinvN RinvN_cv); intros; eapply UL_sequence; [ apply u0 | apply RiemannInt_P4 with pr2 RinvN; apply RinvN_cv || assumption ]. Qed. (***************************************) -(** C°([a,b]) is included in L1([a,b]) *) +(** C°([a,b]) is included in L1([a,b]) *) (***************************************) Lemma maxN : @@ -452,8 +453,8 @@ Proof. apply le_IZR; simpl in |- *; left; apply Rle_lt_trans with ((b - a) / del); assumption. assert (H5 := IZN _ H4); elim H5; clear H5; intros N H5; - unfold Nbound in |- *; exists N; intros; unfold I in H6; - apply INR_le; rewrite H5 in H2; rewrite <- INR_IZR_INZ in H2; + unfold Nbound in |- *; 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) @@ -465,7 +466,7 @@ Proof. elim (Rlt_irrefl _ H7) ] ]. Qed. -Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) {struct N} : Rlist := +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) @@ -498,11 +499,11 @@ Proof. a <= y <= b -> Rabs (x - y) < l -> Rabs (f x - f y) < eps)); assert (H1 : bound E). unfold bound in |- *; exists (b - a); unfold is_upper_bound in |- *; intros; - unfold E in H1; elim H1; clear H1; intros H1 _; elim H1; + 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 in |- *; + elim H2; intros; exists (Rmin x (b - a)); unfold E in |- *; split; [ split; [ unfold Rmin in |- *; case (Rle_dec x (b - a)); intro; @@ -530,7 +531,7 @@ Proof. 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; + 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. @@ -579,7 +580,7 @@ Proof. | intros; change (pos_Rl (SubEquiN (S n) (a0 + del0) b del0) - (pred (Rlength (SubEquiN (S n) (a0 + del0) b del0))) = b) + (pred (Rlength (SubEquiN (S n) (a0 + del0) b del0))) = b) in |- *; apply H ] ]. Qed. @@ -633,7 +634,7 @@ Proof. 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 in |- *; rewrite <- Rplus_0_r; - apply Rplus_le_compat_l; rewrite Rmult_1_l; left; + apply Rplus_le_compat_l; rewrite Rmult_1_l; left; apply (cond_pos del). Qed. @@ -686,7 +687,7 @@ Proof. [ reflexivity | elim n; left; assumption ]. 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 with (mkStepFun (StepFun_P4 a b (eps / (2 * (b - a))))); split. 2: rewrite StepFun_P18; unfold Rdiv in |- *; rewrite Rinv_mult_distr. 2: do 2 rewrite Rmult_assoc; rewrite <- Rinv_l_sym. @@ -731,7 +732,7 @@ Proof. apply Rplus_lt_reg_r 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; + (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))). @@ -760,20 +761,20 @@ Proof. intros; assumption. assert (H4 : Nbound I). unfold Nbound in |- *; exists (S (max_N del H)); intros; unfold max_N in |- *; - case (maxN del H); intros; elim a0; clear a0; intros _ H5; + case (maxN del H); intros; elim a0; clear a0; intros _ 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; + 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 in |- *; case (maxN del H); intros; apply INR_lt; apply Rmult_lt_reg_l with (pos del). apply (cond_pos del). apply Rplus_lt_reg_r with a; do 2 rewrite (Rmult_comm del); - apply Rle_lt_trans with t0; unfold I in H5; try assumption; - elim a0; intros; apply Rlt_le_trans with b; try assumption; + apply Rle_lt_trans with t0; unfold I in H5; try assumption; + elim a0; intros; apply Rlt_le_trans with b; try assumption; elim H8; intros. elim H11; intro. assumption. @@ -1027,7 +1028,7 @@ Proof. unfold Riemann_integrable in |- *; intros f g; intros; case (Req_EM_T l 0); intro. elim (X eps); intros; split with x; elim p; intros; split with x0; elim p0; - intros; split; try assumption; rewrite e; intros; + intros; split; try assumption; rewrite e; intros; rewrite Rmult_0_l; rewrite Rplus_0_r; apply H; assumption. assert (H : 0 < eps / 2). unfold Rdiv in |- *; apply Rmult_lt_0_compat; @@ -1038,8 +1039,8 @@ Proof. | apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; [ prove_sup0 | apply Rabs_pos_lt; assumption ] ]. elim (X (mkposreal _ H)); intros; elim (X0 (mkposreal _ H0)); intros; - split with (mkStepFun (StepFun_P28 l x x0)); elim p0; - elim p; intros; split with (mkStepFun (StepFun_P28 (Rabs l) x1 x2)); + split with (mkStepFun (StepFun_P28 l x x0)); elim p0; + elim p; intros; split with (mkStepFun (StepFun_P28 (Rabs l) x1 x2)); elim p1; elim p2; clear p1 p2 p0 p X X0; intros; split. intros; simpl in |- *; apply Rle_trans with (Rabs (f t - x t) + Rabs (l * (g t - x0 t))). @@ -1098,7 +1099,7 @@ Proof. 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)); + (RiemannInt_SF (phi2 n) + -1 * RiemannInt_SF (phi1 n)); [ idtac | ring ]. rewrite <- StepFun_P30. apply Rle_lt_trans with @@ -1146,7 +1147,7 @@ Proof. apply H; unfold ge in |- *; apply le_trans with N; try assumption; unfold N in |- *; apply le_max_l. unfold R_dist in |- *; unfold Rminus in |- *; rewrite Ropp_0; - rewrite Rplus_0_r; apply Rabs_right; apply Rle_ge; + 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 in |- *; apply le_trans with N; try assumption; unfold N in |- *; apply le_max_r. @@ -1172,7 +1173,7 @@ Proof. 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)); + (RiemannInt_SF (phi2 n) + -1 * RiemannInt_SF (phi1 n)); [ idtac | ring ]. rewrite <- StepFun_P30. rewrite StepFun_P39. @@ -1238,7 +1239,7 @@ Proof. apply H; unfold ge in |- *; apply le_trans with N; try assumption; unfold N in |- *; apply le_max_l. unfold R_dist in |- *; unfold Rminus in |- *; rewrite Ropp_0; - rewrite Rplus_0_r; apply Rabs_right; apply Rle_ge; + 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 in |- *; apply le_trans with N; try assumption; unfold N in |- *; apply le_max_r. @@ -1258,7 +1259,7 @@ Proof. intro f; intros; case (Req_dec l 0); intro. pattern l at 2 in |- *; rewrite H0; rewrite Rmult_0_l; rewrite Rplus_0_r; unfold RiemannInt in |- *; case (RiemannInt_exists pr3 RinvN RinvN_cv); - case (RiemannInt_exists pr1 RinvN RinvN_cv); intros; + case (RiemannInt_exists pr1 RinvN RinvN_cv); intros; eapply UL_sequence; [ apply u0 | set (psi1 := fun n:nat => proj1_sig (phi_sequence_prop RinvN pr1 n)); @@ -1283,13 +1284,13 @@ Proof. intros; apply u. unfold Un_cv in |- *; intros; unfold RiemannInt in |- *; case (RiemannInt_exists pr1 RinvN RinvN_cv); - case (RiemannInt_exists pr2 RinvN RinvN_cv); unfold Un_cv in |- *; + case (RiemannInt_exists pr2 RinvN RinvN_cv); unfold Un_cv in |- *; intros; assert (H2 : 0 < eps / 5). unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. elim (u0 _ H2); clear u0; 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)). + assert (H5 : 0 < eps / (5 * Rabs l)). unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; @@ -1380,7 +1381,7 @@ Proof. (RiemannInt_SF (phi_sequence RinvN pr3 n) + -1 * (RiemannInt_SF (phi_sequence RinvN pr1 n) + - l * RiemannInt_SF (phi_sequence RinvN pr2 n))); + l * RiemannInt_SF (phi_sequence RinvN pr2 n))); [ idtac | ring ]; do 2 rewrite <- StepFun_P30; assert (H10 : Rmin a b = a). unfold Rmin in |- *; case (Rle_dec a b); intro; [ reflexivity | elim n0; assumption ]. @@ -1421,7 +1422,7 @@ Proof. 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. + 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)). @@ -1487,7 +1488,7 @@ Proof. [ unfold Rdiv in |- *; do 2 rewrite Rmult_plus_distr_l; do 3 rewrite (Rmult_comm 5); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ ring | discrR ] - | discrR ]. + | discrR ]. Qed. Lemma RiemannInt_P13 : @@ -1517,7 +1518,7 @@ Proof. split with (mkStepFun (StepFun_P4 a b c)); split with (mkStepFun (StepFun_P4 a b 0)); split; [ intros; simpl in |- *; unfold Rminus in |- *; rewrite Rplus_opp_r; - rewrite Rabs_R0; unfold fct_cte in |- *; right; + rewrite Rabs_R0; unfold fct_cte in |- *; right; reflexivity | rewrite StepFun_P18; rewrite Rmult_0_l; rewrite Rabs_R0; apply (cond_pos eps) ]. @@ -1546,12 +1547,12 @@ Proof. elim H1; clear H1; intros psi1 H1; set (phi2 := fun n:nat => mkStepFun (StepFun_P4 a b c)); set (psi2 := fun n:nat => mkStepFun (StepFun_P4 a b 0)); - apply RiemannInt_P11 with f RinvN phi2 psi2 psi1; + apply RiemannInt_P11 with f RinvN phi2 psi2 psi1; try assumption. apply RinvN_cv. intro; split. intros; unfold f in |- *; simpl in |- *; unfold Rminus in |- *; - rewrite Rplus_opp_r; rewrite Rabs_R0; unfold fct_cte in |- *; + rewrite Rplus_opp_r; rewrite Rabs_R0; unfold fct_cte in |- *; right; reflexivity. unfold psi2 in |- *; rewrite StepFun_P18; rewrite Rmult_0_l; rewrite Rabs_R0; apply (cond_pos (RinvN n)). @@ -1594,7 +1595,7 @@ Proof. apply Rmult_eq_reg_l with 2; [ unfold Rdiv in |- *; do 2 rewrite (Rmult_comm 2); rewrite (Rmult_plus_distr_r (- l2) ((l1 + l2) * / 2) 2); - repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym; + repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ ring | discrR ] | discrR ]. apply Ropp_lt_cancel; apply Rplus_lt_reg_r with l1; @@ -1637,7 +1638,7 @@ Proof. Rabs (Rabs (f t) - phi3 n t) <= psi3 n t) /\ Rabs (RiemannInt_SF (psi3 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 n)). + apply (proj2_sig (phi_sequence_prop RinvN pr2 n)). assert (H1 : exists psi2 : nat -> StepFun a b, @@ -1674,7 +1675,7 @@ Lemma RiemannInt_P18 : Proof. intro f; intros; unfold RiemannInt in |- *; case (RiemannInt_exists pr1 RinvN RinvN_cv); - case (RiemannInt_exists pr2 RinvN RinvN_cv); intros; + case (RiemannInt_exists pr2 RinvN RinvN_cv); intros; eapply UL_sequence. apply u0. set (phi1 := fun N:nat => phi_sequence RinvN pr1 N); @@ -1688,7 +1689,7 @@ Proof. Rabs (f t - phi1 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 n)). + apply (proj2_sig (phi_sequence_prop RinvN pr1 n)). elim H1; clear H1; intros psi1 H1; set (phi2 := fun N:nat => phi_sequence RinvN pr2 N). set @@ -1712,10 +1713,10 @@ Proof. Rmin a b <= t /\ t <= Rmax a b -> Rabs (g t - phi2 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 n)). + apply (proj2_sig (phi_sequence_prop RinvN pr2 n)). elim H2; clear H2; intros psi2 H2; - apply RiemannInt_P11 with f RinvN phi2_m psi2 psi1; - try assumption. + apply RiemannInt_P11 with f RinvN phi2_m psi2 psi1; + try assumption. apply RinvN_cv. intro; elim (H2 n); intros; split; try assumption. intros; unfold phi2_m in |- *; simpl in |- *; unfold phi2_aux in |- *; @@ -1764,11 +1765,11 @@ Proof. right; reflexivity. intro; assert (H2 := pre (phi2 N)); unfold IsStepFun in H2; unfold is_subdivision in H2; elim H2; clear H2; intros l [lf H2]; - split with l; split with lf; unfold adapted_couple in H2; - decompose [and] H2; clear H2; unfold adapted_couple in |- *; + split with l; split with lf; unfold adapted_couple in H2; + decompose [and] H2; clear H2; unfold adapted_couple in |- *; repeat split; try assumption. intros; assert (H9 := H8 i H2); unfold constant_D_eq, open_interval in H9; - unfold constant_D_eq, open_interval in |- *; intros; + unfold constant_D_eq, open_interval in |- *; intros; rewrite <- (H9 x1 H7); assert (H10 : a <= pos_Rl l i). replace a with (Rmin a b). rewrite <- H5; elim (RList_P6 l); intros; apply H10. @@ -1808,7 +1809,7 @@ Proof. (RiemannInt (RiemannInt_P16 (RiemannInt_P10 (-1) pr2 pr1))). apply (RiemannInt_P17 (RiemannInt_P10 (-1) pr2 pr1) - (RiemannInt_P16 (RiemannInt_P10 (-1) pr2 pr1))); + (RiemannInt_P16 (RiemannInt_P10 (-1) pr2 pr1))); assumption. replace (RiemannInt pr2 + - RiemannInt pr1) with (RiemannInt (RiemannInt_P10 (-1) pr2 pr1)). @@ -1833,7 +1834,7 @@ Proof. Qed. Definition primitive (f:R -> R) (a b:R) (h:a <= b) - (pr:forall x:R, a <= x -> x <= b -> Riemann_integrable f a x) + (pr:forall x:R, a <= x -> x <= b -> Riemann_integrable f a x) (x:R) : R := match Rle_dec a x with | left r => @@ -1977,20 +1978,20 @@ Proof. | elim n0; left; assumption ]. apply StepFun_P46 with b; assumption. assert (H3 := pre psi2); unfold IsStepFun in H3; unfold is_subdivision in H3; - elim H3; clear H3; intros l1 [lf1 H3]; split with l1; - split with lf1; unfold adapted_couple in H3; decompose [and] H3; - clear H3; unfold adapted_couple in |- *; repeat split; + elim H3; clear H3; intros l1 [lf1 H3]; split with l1; + split with lf1; unfold adapted_couple in H3; decompose [and] H3; + clear H3; unfold adapted_couple in |- *; repeat split; try assumption. intros; assert (H9 := H8 i H3); unfold constant_D_eq, open_interval in |- *; - unfold constant_D_eq, open_interval in H9; intros; + unfold constant_D_eq, open_interval in H9; intros; rewrite <- (H9 x H7); unfold psi3 in |- *; assert (H10 : b < x). apply Rle_lt_trans with (pos_Rl l1 i). replace b with (Rmin b c). rewrite <- H5; elim (RList_P6 l1); intros; apply H10; try assumption. apply le_O_n. apply lt_trans with (pred (Rlength l1)); try assumption; apply lt_pred_n_n; - apply neq_O_lt; red in |- *; intro; rewrite <- H12 in H6; - discriminate. + apply neq_O_lt; red in |- *; intro; rewrite <- H12 in H6; + discriminate. unfold Rmin in |- *; case (Rle_dec b c); intro; [ reflexivity | elim n; assumption ]. elim H7; intros; assumption. @@ -2000,19 +2001,19 @@ Proof. | elim n; apply Rle_trans with b; [ assumption | left; assumption ] | elim n0; apply Rle_trans with b; [ assumption | left; assumption ] ]. assert (H3 := pre psi1); unfold IsStepFun in H3; unfold is_subdivision in H3; - elim H3; clear H3; intros l1 [lf1 H3]; split with l1; - split with lf1; unfold adapted_couple in H3; decompose [and] H3; - clear H3; unfold adapted_couple in |- *; repeat split; + elim H3; clear H3; intros l1 [lf1 H3]; split with l1; + split with lf1; unfold adapted_couple in H3; decompose [and] H3; + clear H3; unfold adapted_couple in |- *; repeat split; try assumption. intros; assert (H9 := H8 i H3); unfold constant_D_eq, open_interval in |- *; - unfold constant_D_eq, open_interval in H9; intros; + unfold constant_D_eq, open_interval in H9; intros; rewrite <- (H9 x H7); unfold psi3 in |- *; assert (H10 : x <= b). apply Rle_trans with (pos_Rl l1 (S i)). elim H7; intros; left; assumption. replace b with (Rmax a b). rewrite <- H4; elim (RList_P6 l1); intros; apply H10; try assumption. apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H12 in H6; - discriminate. + discriminate. unfold Rmax in |- *; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. assert (H11 : a <= x). @@ -2021,8 +2022,8 @@ Proof. rewrite <- H5; elim (RList_P6 l1); intros; apply H11; try assumption. apply le_O_n. apply lt_trans with (pred (Rlength l1)); try assumption; apply lt_pred_n_n; - apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H6; - discriminate. + apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H6; + discriminate. unfold Rmin in |- *; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. left; elim H7; intros; assumption. @@ -2030,19 +2031,19 @@ Proof. assumption. apply StepFun_P46 with b. assert (H3 := pre phi1); unfold IsStepFun in H3; unfold is_subdivision in H3; - elim H3; clear H3; intros l1 [lf1 H3]; split with l1; - split with lf1; unfold adapted_couple in H3; decompose [and] H3; - clear H3; unfold adapted_couple in |- *; repeat split; + elim H3; clear H3; intros l1 [lf1 H3]; split with l1; + split with lf1; unfold adapted_couple in H3; decompose [and] H3; + clear H3; unfold adapted_couple in |- *; repeat split; try assumption. intros; assert (H9 := H8 i H3); unfold constant_D_eq, open_interval in |- *; - unfold constant_D_eq, open_interval in H9; intros; + unfold constant_D_eq, open_interval in H9; intros; rewrite <- (H9 x H7); unfold psi3 in |- *; assert (H10 : x <= b). apply Rle_trans with (pos_Rl l1 (S i)). elim H7; intros; left; assumption. replace b with (Rmax a b). rewrite <- H4; elim (RList_P6 l1); intros; apply H10; try assumption. apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H12 in H6; - discriminate. + discriminate. unfold Rmax in |- *; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. assert (H11 : a <= x). @@ -2051,28 +2052,28 @@ Proof. rewrite <- H5; elim (RList_P6 l1); intros; apply H11; try assumption. apply le_O_n. apply lt_trans with (pred (Rlength l1)); try assumption; apply lt_pred_n_n; - apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H6; - discriminate. + apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H6; + discriminate. unfold Rmin in |- *; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. left; elim H7; intros; assumption. unfold phi3 in |- *; case (Rle_dec a x); case (Rle_dec x b); intros; reflexivity || elim n; assumption. assert (H3 := pre phi2); unfold IsStepFun in H3; unfold is_subdivision in H3; - elim H3; clear H3; intros l1 [lf1 H3]; split with l1; - split with lf1; unfold adapted_couple in H3; decompose [and] H3; - clear H3; unfold adapted_couple in |- *; repeat split; + elim H3; clear H3; intros l1 [lf1 H3]; split with l1; + split with lf1; unfold adapted_couple in H3; decompose [and] H3; + clear H3; unfold adapted_couple in |- *; repeat split; try assumption. intros; assert (H9 := H8 i H3); unfold constant_D_eq, open_interval in |- *; - unfold constant_D_eq, open_interval in H9; intros; + unfold constant_D_eq, open_interval in H9; intros; rewrite <- (H9 x H7); unfold psi3 in |- *; assert (H10 : b < x). apply Rle_lt_trans with (pos_Rl l1 i). replace b with (Rmin b c). rewrite <- H5; elim (RList_P6 l1); intros; apply H10; try assumption. apply le_O_n. apply lt_trans with (pred (Rlength l1)); try assumption; apply lt_pred_n_n; - apply neq_O_lt; red in |- *; intro; rewrite <- H12 in H6; - discriminate. + apply neq_O_lt; red in |- *; intro; rewrite <- H12 in H6; + discriminate. unfold Rmin in |- *; case (Rle_dec b c); intro; [ reflexivity | elim n; assumption ]. elim H7; intros; assumption. @@ -2088,7 +2089,7 @@ Lemma RiemannInt_P22 : Riemann_integrable f a b -> a <= c <= b -> Riemann_integrable f a c. Proof. unfold Riemann_integrable in |- *; intros; elim (X eps); clear X; - intros phi [psi H0]; elim H; elim H0; clear H H0; + intros phi [psi H0]; elim H; elim H0; clear H H0; intros; assert (H3 : IsStepFun phi a c). apply StepFun_P44 with b. apply (pre phi). @@ -2178,7 +2179,7 @@ Lemma RiemannInt_P23 : Riemann_integrable f a b -> a <= c <= b -> Riemann_integrable f c b. Proof. unfold Riemann_integrable in |- *; intros; elim (X eps); clear X; - intros phi [psi H0]; elim H; elim H0; clear H H0; + intros phi [psi H0]; elim H; elim H0; clear H H0; intros; assert (H3 : IsStepFun phi c b). apply StepFun_P45 with a. apply (pre phi). @@ -2294,7 +2295,7 @@ Proof. intros f a b c pr1 pr2 pr3 Hyp1 Hyp2; unfold RiemannInt in |- *; case (RiemannInt_exists pr1 RinvN RinvN_cv); case (RiemannInt_exists pr2 RinvN RinvN_cv); - case (RiemannInt_exists pr3 RinvN RinvN_cv); intros; + case (RiemannInt_exists pr3 RinvN RinvN_cv); intros; symmetry in |- *; eapply UL_sequence. apply u. unfold Un_cv in |- *; intros; assert (H0 : 0 < eps / 3). @@ -2309,7 +2310,7 @@ Proof. (RiemannInt_SF (phi_sequence RinvN pr1 n) + RiemannInt_SF (phi_sequence RinvN pr2 n))) 0). intro; elim (H3 _ H0); clear H3; intros N3 H3; - set (N0 := max (max N1 N2) N3); exists N0; intros; + set (N0 := max (max N1 N2) N3); exists N0; intros; unfold R_dist in |- *; apply Rle_lt_trans with (Rabs @@ -2368,7 +2369,7 @@ Proof. 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 n)). + apply (proj2_sig (phi_sequence_prop RinvN pr1 n)). assert (H2 : exists psi2 : nat -> StepFun b c, @@ -2378,7 +2379,7 @@ Proof. Rabs (f 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 n)). + apply (proj2_sig (phi_sequence_prop RinvN pr2 n)). assert (H3 : exists psi3 : nat -> StepFun a c, @@ -2388,9 +2389,9 @@ Proof. Rabs (f 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 n)). + apply (proj2_sig (phi_sequence_prop RinvN pr3 n)). elim H1; clear H1; intros psi1 H1; elim H2; clear H2; intros psi2 H2; elim H3; - clear H3; intros psi3 H3; assert (H := RinvN_cv); + clear H3; intros psi3 H3; assert (H := RinvN_cv); unfold Un_cv in |- *; intros; assert (H4 : 0 < eps / 3). unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. @@ -2401,14 +2402,14 @@ Proof. (R_dist (mkposreal (/ (INR n + 1)) (RinvN_pos n)) 0). apply H; assumption. unfold R_dist in |- *; unfold Rminus in |- *; rewrite Ropp_0; - rewrite Rplus_0_r; apply Rabs_right; apply Rle_ge; + rewrite Rplus_0_r; apply Rabs_right; apply Rle_ge; left; apply (cond_pos (RinvN n)). exists N0; intros; elim (H1 n); elim (H2 n); elim (H3 n); clear H1 H2 H3; - intros; unfold R_dist in |- *; unfold Rminus in |- *; - rewrite Ropp_0; rewrite Rplus_0_r; + intros; unfold R_dist in |- *; unfold Rminus in |- *; + rewrite Ropp_0; rewrite Rplus_0_r; set (phi1 := phi_sequence RinvN pr1 n) in H8 |- *; - set (phi2 := phi_sequence RinvN pr2 n) in H3 |- *; - set (phi3 := phi_sequence RinvN pr3 n) in H1 |- *; + set (phi2 := phi_sequence RinvN pr2 n) in H3 |- *; + set (phi3 := phi_sequence RinvN pr3 n) in H1 |- *; assert (H10 : IsStepFun phi3 a b). apply StepFun_P44 with c. apply (pre phi3). @@ -2832,7 +2833,7 @@ Proof. (derivable_pt_lim ((fct_cte (f b) * (id - fct_cte b))%F + fct_cte (RiemannInt (FTC_P1 h C0 h (Rle_refl b)))) b ( - f b + 0)) in |- *. + f b + 0)) in |- *. apply derivable_pt_lim_plus. pattern (f b) at 2 in |- *; replace (f b) with (0 * (id - fct_cte b)%F b + fct_cte (f b) b * 1). @@ -2899,7 +2900,7 @@ Proof. apply (RiemannInt_P17 (RiemannInt_P10 (-1) H13 (RiemannInt_P14 (b + h0) b (f b))) (RiemannInt_P16 - (RiemannInt_P10 (-1) H13 (RiemannInt_P14 (b + h0) b (f b))))); + (RiemannInt_P10 (-1) H13 (RiemannInt_P14 (b + h0) b (f b))))); left; assumption. apply Rle_lt_trans with (RiemannInt (RiemannInt_P14 (b + h0) b (eps / 2)) * Rabs (/ h0)). @@ -2953,13 +2954,13 @@ Proof. rewrite RiemannInt_P15. rewrite <- Ropp_mult_distr_l_reverse; apply Rmult_eq_reg_l with h0; [ repeat rewrite (Rmult_comm h0); unfold Rdiv in |- *; - repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym; + repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ ring | assumption ] | assumption ]. cut (a <= b + h0). cut (b + h0 <= b). intros; unfold primitive in |- *; case (Rle_dec a (b + h0)); - case (Rle_dec (b + h0) b); case (Rle_dec a b); case (Rle_dec b b); + case (Rle_dec (b + h0) b); case (Rle_dec a b); case (Rle_dec b b); intros; try (elim n; right; reflexivity) || (elim n; left; assumption). rewrite <- (RiemannInt_P26 (FTC_P1 h C0 r3 r2) H13 (FTC_P1 h C0 r1 r0)); ring. elim n; assumption. @@ -3083,7 +3084,7 @@ Proof. apply (RiemannInt_P17 (RiemannInt_P10 (-1) H13 (RiemannInt_P14 a (a + h0) (f a))) (RiemannInt_P16 - (RiemannInt_P10 (-1) H13 (RiemannInt_P14 a (a + h0) (f a))))); + (RiemannInt_P10 (-1) H13 (RiemannInt_P14 a (a + h0) (f a))))); left; assumption. apply Rle_lt_trans with (RiemannInt (RiemannInt_P14 a (a + h0) (eps / 2)) * Rabs (/ h0)). @@ -3138,7 +3139,7 @@ Proof. cut (a <= a + h0). cut (a + h0 <= b). intros; unfold primitive in |- *; case (Rle_dec a (a + h0)); - case (Rle_dec (a + h0) b); case (Rle_dec a a); case (Rle_dec a b); + case (Rle_dec (a + h0) b); case (Rle_dec a a); case (Rle_dec a b); intros; try (elim n; right; reflexivity) || (elim n; left; assumption). rewrite RiemannInt_P9; unfold Rminus in |- *; rewrite Ropp_0; rewrite Rplus_0_r; apply RiemannInt_P5. @@ -3174,7 +3175,7 @@ Proof. (derivable_pt_lim ((fct_cte (f b) * (id - fct_cte b))%F + fct_cte (RiemannInt (FTC_P1 h C0 h (Rle_refl b)))) b ( - f b + 0)) in |- *. + f b + 0)) in |- *. apply derivable_pt_lim_plus. pattern (f b) at 2 in |- *; replace (f b) with (0 * (id - fct_cte b)%F b + fct_cte (f b) b * 1). @@ -3198,7 +3199,7 @@ Proof. pattern a at 2 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; assumption. rewrite H1; unfold primitive in |- *; case (Rle_dec a (a + h0)); - case (Rle_dec (a + h0) b); case (Rle_dec a a); case (Rle_dec a b); + case (Rle_dec (a + h0) b); case (Rle_dec a a); case (Rle_dec a b); intros; try (elim n; right; assumption || reflexivity). elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r3 H10)). elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r2 H10)). @@ -3216,7 +3217,7 @@ Proof. assumption. elim H8; symmetry in |- *; assumption. rewrite H0 in H1; rewrite H1; unfold primitive in |- *; - case (Rle_dec a (b + h0)); case (Rle_dec (b + h0) b); + case (Rle_dec a (b + h0)); case (Rle_dec (b + h0) b); case (Rle_dec a b); case (Rle_dec b b); intros; try (elim n; right; assumption || reflexivity). rewrite H0 in H10; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r2 H10)). @@ -3286,7 +3287,7 @@ Proof. intros; apply (cont1 f). rewrite (RiemannInt_P20 H (FTC_P1 H H0) pr); assert (H1 := RiemannInt_P29 H H0); assert (H2 := RiemannInt_P31 f H); - elim (antiderivative_Ucte (derive f (diff0 f)) _ _ _ _ H1 H2); + elim (antiderivative_Ucte (derive f (diff0 f)) _ _ _ _ H1 H2); intros C H3; repeat rewrite H3; [ ring | split; [ right; reflexivity | assumption ] |