1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: RiemannInt_SF.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
12
Require Import Rfunctions.
13
Require Import Ranalysis.
14
Require Import Classical_Prop.
15
Open Local Scope R_scope.
17
Set Implicit Arguments.
19
(*****************************************************)
20
(** * Each bounded subset of N has a maximal element *)
21
(*****************************************************)
23
Definition Nbound (I:nat -> Prop) : Prop :=
24
exists n : nat, (forall i:nat, I i -> (i <= n)%nat).
26
Lemma IZN_var : forall z:Z, (0 <= z)%Z -> {n : nat | z = Z_of_nat n}.
28
intros; apply Z_of_nat_complete_inf; assumption.
33
(exists n : nat, I n) ->
34
Nbound I -> { n:nat | I n /\ (forall i:nat, I i -> (i <= n)%nat) }.
36
intros I H H0; set (E := fun x:R => exists i : nat, I i /\ INR i = x);
37
assert (H1 : bound E).
38
unfold Nbound in H0; elim H0; intros N H1; unfold bound in |- *;
39
exists (INR N); unfold is_upper_bound in |- *; intros;
40
unfold E in H2; elim H2; intros; elim H3; intros;
41
rewrite <- H5; apply le_INR; apply H1; assumption.
42
assert (H2 : exists x : R, E x).
43
elim H; intros; exists (INR x); unfold E in |- *; exists x; split;
44
[ assumption | reflexivity ].
45
assert (H3 := completeness E H1 H2); elim H3; intros; unfold is_lub in p;
46
elim p; clear p; intros; unfold is_upper_bound in H4, H5;
48
elim H2; intros; unfold E in H6; elim H6; intros; elim H7; intros;
49
apply Rle_trans with x0;
50
[ rewrite <- H9; change (INR 0 <= INR x1) in |- *; apply le_INR;
52
| apply H4; assumption ].
53
assert (H7 := archimed x); elim H7; clear H7; intros;
54
assert (H9 : x <= IZR (up x) - 1).
55
apply H5; intros; assert (H10 := H4 _ H9); unfold E in H9; elim H9; intros;
56
elim H11; intros; rewrite <- H13; apply Rplus_le_reg_l with 1;
57
replace (1 + (IZR (up x) - 1)) with (IZR (up x));
58
[ idtac | ring ]; replace (1 + INR x1) with (INR (S x1));
59
[ idtac | rewrite S_INR; ring ].
60
assert (H14 : (0 <= up x)%Z).
61
apply le_IZR; apply Rle_trans with x; [ apply H6 | left; assumption ].
62
assert (H15 := IZN _ H14); elim H15; clear H15; intros; rewrite H15;
63
rewrite <- INR_IZR_INZ; apply le_INR; apply lt_le_S;
64
apply INR_lt; rewrite H13; apply Rle_lt_trans with x;
65
[ assumption | rewrite INR_IZR_INZ; rewrite <- H15; assumption ].
66
assert (H10 : x = IZR (up x) - 1).
69
| apply Rplus_le_reg_l with (- x + 1);
70
replace (- x + 1 + (IZR (up x) - 1)) with (IZR (up x) - x);
71
[ idtac | ring ]; replace (- x + 1 + x) with 1;
72
[ assumption | ring ] ].
73
assert (H11 : (0 <= up x)%Z).
74
apply le_IZR; apply Rle_trans with x; [ apply H6 | left; assumption ].
75
assert (H12 := IZN_var H11); elim H12; clear H12; intros; assert (H13 : E x).
76
elim (classic (E x)); intro; try assumption.
77
cut (forall y:R, E y -> y <= x - 1).
78
intro; assert (H14 := H5 _ H13); cut (x - 1 < x).
79
intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H14 H15)).
80
apply Rminus_lt; replace (x - 1 - x) with (-1); [ idtac | ring ];
81
rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; apply Rlt_0_1.
82
intros; assert (H14 := H4 _ H13); elim H14; intro; unfold E in H13; elim H13;
83
intros; elim H16; intros; apply Rplus_le_reg_l with 1.
84
replace (1 + (x - 1)) with x; [ idtac | ring ]; rewrite <- H18;
85
replace (1 + INR x1) with (INR (S x1)); [ idtac | rewrite S_INR; ring ].
86
cut (x = INR (pred x0)).
87
intro; rewrite H19; apply le_INR; apply lt_le_S; apply INR_lt; rewrite H18;
88
rewrite <- H19; assumption.
89
rewrite H10; rewrite p; rewrite <- INR_IZR_INZ; replace 1 with (INR 1);
90
[ idtac | reflexivity ]; rewrite <- minus_INR.
91
replace (x0 - 1)%nat with (pred x0);
93
| case x0; [ reflexivity | intro; simpl in |- *; apply minus_n_O ] ].
94
induction x0 as [| x0 Hrecx0];
95
[ rewrite p in H7; rewrite <- INR_IZR_INZ in H7; simpl in H7;
96
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 H7))
97
| apply le_n_S; apply le_O_n ].
98
rewrite H15 in H13; elim H12; assumption.
99
split with (pred x0); unfold E in H13; elim H13; intros; elim H12; intros;
100
rewrite H10 in H15; rewrite p in H15; rewrite <- INR_IZR_INZ in H15;
101
assert (H16 : INR x0 = INR x1 + 1).
103
rewrite <- S_INR in H16; assert (H17 := INR_eq _ _ H16); rewrite H17;
104
simpl in |- *; split.
106
intros; apply INR_le; rewrite H15; rewrite <- H15; elim H12; intros;
107
rewrite H20; apply H4; unfold E in |- *; exists i;
108
split; [ assumption | reflexivity ].
111
(*******************************************)
112
(** * Step functions *)
113
(*******************************************)
115
Definition open_interval (a b x:R) : Prop := a < x < b.
116
Definition co_interval (a b x:R) : Prop := a <= x < b.
118
Definition adapted_couple (f:R -> R) (a b:R) (l lf:Rlist) : Prop :=
120
pos_Rl l 0 = Rmin a b /\
121
pos_Rl l (pred (Rlength l)) = Rmax a b /\
122
Rlength l = S (Rlength lf) /\
124
(i < pred (Rlength l))%nat ->
125
constant_D_eq f (open_interval (pos_Rl l i) (pos_Rl l (S i)))
128
Definition adapted_couple_opt (f:R -> R) (a b:R) (l lf:Rlist) :=
129
adapted_couple f a b l lf /\
131
(i < pred (Rlength lf))%nat ->
132
pos_Rl lf i <> pos_Rl lf (S i) \/ f (pos_Rl l (S i)) <> pos_Rl lf i) /\
133
(forall i:nat, (i < pred (Rlength l))%nat -> pos_Rl l i <> pos_Rl l (S i)).
135
Definition is_subdivision (f:R -> R) (a b:R) (l:Rlist) : Type :=
136
{ l0:Rlist & adapted_couple f a b l l0 }.
138
Definition IsStepFun (f:R -> R) (a b:R) : Type :=
139
{ l:Rlist & is_subdivision f a b l }.
141
(** ** Class of step functions *)
142
Record StepFun (a b:R) : Type := mkStepFun
143
{fe :> R -> R; pre : IsStepFun fe a b}.
145
Definition subdivision (a b:R) (f:StepFun a b) : Rlist := projT1 (pre f).
147
Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist :=
148
match projT2 (pre f) with
152
Boxed Fixpoint Int_SF (l k:Rlist) {struct l} : R :=
159
| cons x (cons y k') => a * (y - x) + Int_SF l' (cons y k')
163
(** ** Integral of step functions *)
164
Definition RiemannInt_SF (a b:R) (f:StepFun a b) : R :=
165
match Rle_dec a b with
166
| left _ => Int_SF (subdivision_val f) (subdivision f)
167
| right _ => - Int_SF (subdivision_val f) (subdivision f)
170
(************************************)
171
(** ** Properties of step functions *)
172
(************************************)
175
forall (a b:R) (f:StepFun a b),
176
adapted_couple f a b (subdivision f) (subdivision_val f).
178
intros a b f; unfold subdivision_val in |- *; case (projT2 (pre f)); intros;
183
forall (a b:R) (f:R -> R) (l lf:Rlist),
184
adapted_couple f a b l lf -> adapted_couple f b a l lf.
186
unfold adapted_couple in |- *; intros; decompose [and] H; clear H;
187
repeat split; try assumption.
188
rewrite H2; unfold Rmin in |- *; case (Rle_dec a b); intro;
189
case (Rle_dec b a); intro; try reflexivity.
190
apply Rle_antisym; assumption.
191
apply Rle_antisym; auto with real.
192
rewrite H1; unfold Rmax in |- *; case (Rle_dec a b); intro;
193
case (Rle_dec b a); intro; try reflexivity.
194
apply Rle_antisym; assumption.
195
apply Rle_antisym; auto with real.
201
adapted_couple (fct_cte c) a b (cons a (cons b nil)) (cons c nil).
203
intros; unfold adapted_couple in |- *; repeat split.
204
unfold ordered_Rlist in |- *; intros; simpl in H0; inversion H0;
205
[ simpl in |- *; assumption | elim (le_Sn_O _ H2) ].
206
simpl in |- *; unfold Rmin in |- *; case (Rle_dec a b); intro;
207
[ reflexivity | elim n; assumption ].
208
simpl in |- *; unfold Rmax in |- *; case (Rle_dec a b); intro;
209
[ reflexivity | elim n; assumption ].
210
unfold constant_D_eq, open_interval in |- *; intros; simpl in H0;
211
inversion H0; [ reflexivity | elim (le_Sn_O _ H3) ].
214
Lemma StepFun_P4 : forall a b c:R, IsStepFun (fct_cte c) a b.
216
intros; unfold IsStepFun in |- *; case (Rle_dec a b); intro.
217
apply existT with (cons a (cons b nil)); unfold is_subdivision in |- *;
218
apply existT with (cons c nil); apply (StepFun_P3 c r).
219
apply existT with (cons b (cons a nil)); unfold is_subdivision in |- *;
220
apply existT with (cons c nil); apply StepFun_P2;
221
apply StepFun_P3; auto with real.
225
forall (a b:R) (f:R -> R) (l:Rlist),
226
is_subdivision f a b l -> is_subdivision f b a l.
228
destruct 1 as (x,(H0,(H1,(H2,(H3,H4))))); exists x;
229
repeat split; try assumption.
230
rewrite H1; apply Rmin_comm.
231
rewrite H2; apply Rmax_comm.
235
forall (f:R -> R) (a b:R), IsStepFun f a b -> IsStepFun f b a.
237
unfold IsStepFun in |- *; intros; elim X; intros; apply existT with x;
238
apply StepFun_P5; assumption.
242
forall (a b r1 r2 r3:R) (f:R -> R) (l lf:Rlist),
244
adapted_couple f a b (cons r1 (cons r2 l)) (cons r3 lf) ->
245
adapted_couple f r2 b (cons r2 l) lf.
247
unfold adapted_couple in |- *; intros; decompose [and] H0; clear H0;
248
assert (H5 : Rmax a b = b).
249
unfold Rmax in |- *; case (Rle_dec a b); intro;
250
[ reflexivity | elim n; assumption ].
251
assert (H7 : r2 <= b).
252
rewrite H5 in H2; rewrite <- H2; apply RList_P7;
253
[ assumption | simpl in |- *; right; left; reflexivity ].
255
apply RList_P4 with r1; assumption.
256
rewrite H5 in H2; unfold Rmin in |- *; case (Rle_dec r2 b); intro;
257
[ reflexivity | elim n; assumption ].
258
unfold Rmax in |- *; case (Rle_dec r2 b); intro;
259
[ rewrite H5 in H2; rewrite <- H2; reflexivity | elim n; assumption ].
260
simpl in H4; simpl in |- *; apply INR_eq; apply Rplus_eq_reg_l with 1;
261
do 2 rewrite (Rplus_comm 1); do 2 rewrite <- S_INR;
262
rewrite H4; reflexivity.
263
intros; unfold constant_D_eq, open_interval in |- *; intros;
264
unfold constant_D_eq, open_interval in H6;
265
assert (H9 : (S i < pred (Rlength (cons r1 (cons r2 l))))%nat).
266
simpl in |- *; simpl in H0; apply lt_n_S; assumption.
267
assert (H10 := H6 _ H9); apply H10; assumption.
271
forall (f:R -> R) (l1 lf1:Rlist) (a b:R),
272
adapted_couple f a b l1 lf1 -> a = b -> Int_SF lf1 l1 = 0.
275
intros; induction lf1 as [| r lf1 Hreclf1]; reflexivity.
277
intros; induction lf1 as [| r1 lf1 Hreclf1].
279
unfold adapted_couple in H0; decompose [and] H0; clear H0; simpl in H5;
281
intros; induction lf1 as [| r3 lf1 Hreclf1].
283
simpl in |- *; cut (r = r1).
284
intro; rewrite H3; rewrite (H0 lf1 r b).
286
rewrite H3; apply StepFun_P7 with a r r3; [ right; assumption | assumption ].
287
clear H H0 Hreclf1 r0; unfold adapted_couple in H1; decompose [and] H1;
288
intros; simpl in H4; rewrite H4; unfold Rmin in |- *;
289
case (Rle_dec a b); intro; [ assumption | reflexivity ].
290
unfold adapted_couple in H1; decompose [and] H1; intros; apply Rle_antisym.
291
apply (H3 0%nat); simpl in |- *; apply lt_O_Sn.
292
simpl in H5; rewrite H2 in H5; rewrite H5; replace (Rmin b b) with (Rmax a b);
293
[ rewrite <- H4; apply RList_P7;
294
[ assumption | simpl in |- *; right; left; reflexivity ]
295
| unfold Rmin, Rmax in |- *; case (Rle_dec b b); case (Rle_dec a b); intros;
296
try assumption || reflexivity ].
300
forall (a b:R) (f:R -> R) (l lf:Rlist),
301
adapted_couple f a b l lf -> a <> b -> (2 <= Rlength l)%nat.
303
intros; unfold adapted_couple in H; decompose [and] H; clear H;
304
induction l as [| r l Hrecl];
305
[ simpl in H4; discriminate
306
| induction l as [| r0 l Hrecl0];
307
[ simpl in H3; simpl in H2; generalize H3; generalize H2;
308
unfold Rmin, Rmax in |- *; case (Rle_dec a b);
309
intros; elim H0; rewrite <- H5; rewrite <- H7;
311
| simpl in |- *; do 2 apply le_n_S; apply le_O_n ] ].
315
forall (f:R -> R) (l lf:Rlist) (a b:R),
317
adapted_couple f a b l lf ->
319
(exists lf' : Rlist, adapted_couple_opt f a b l' lf').
322
intros; unfold adapted_couple in H0; decompose [and] H0; simpl in H4;
324
intros; case (Req_dec a b); intro.
325
exists (cons a nil); exists nil; unfold adapted_couple_opt in |- *;
326
unfold adapted_couple in |- *; unfold ordered_Rlist in |- *;
327
repeat split; try (intros; simpl in H3; elim (lt_n_O _ H3)).
328
simpl in |- *; rewrite <- H2; unfold Rmin in |- *; case (Rle_dec a a); intro;
330
simpl in |- *; rewrite <- H2; unfold Rmax in |- *; case (Rle_dec a a); intro;
332
elim (RList_P20 _ (StepFun_P9 H1 H2)); intros t1 [t2 [t3 H3]];
333
induction lf as [| r1 lf Hreclf].
334
unfold adapted_couple in H1; decompose [and] H1; rewrite H3 in H7;
335
simpl in H7; discriminate.
336
clear Hreclf; assert (H4 : adapted_couple f t2 b r0 lf).
337
rewrite H3 in H1; assert (H4 := RList_P21 _ _ H3); simpl in H4; rewrite H4;
338
eapply StepFun_P7; [ apply H0 | apply H1 ].
340
intro; assert (H6 := H _ _ _ H5 H4); case (Req_dec t1 t2); intro Hyp_eq.
343
rewrite <- Hyp_eq; rewrite H3 in H1; unfold adapted_couple in H1;
344
decompose [and] H1; clear H1; simpl in H9; rewrite H9;
345
unfold Rmin in |- *; case (Rle_dec a b); intro;
346
[ reflexivity | elim n; assumption ].
347
elim H6; clear H6; intros l' [lf' H6]; case (Req_dec t2 b); intro.
348
exists (cons a (cons b nil)); exists (cons r1 nil);
349
unfold adapted_couple_opt in |- *; unfold adapted_couple in |- *;
351
unfold ordered_Rlist in |- *; intros; simpl in H8; inversion H8;
352
[ simpl in |- *; assumption | elim (le_Sn_O _ H10) ].
353
simpl in |- *; unfold Rmin in |- *; case (Rle_dec a b); intro;
354
[ reflexivity | elim n; assumption ].
355
simpl in |- *; unfold Rmax in |- *; case (Rle_dec a b); intro;
356
[ reflexivity | elim n; assumption ].
357
intros; simpl in H8; inversion H8.
358
unfold constant_D_eq, open_interval in |- *; intros; simpl in |- *;
359
simpl in H9; rewrite H3 in H1; unfold adapted_couple in H1;
360
decompose [and] H1; apply (H16 0%nat).
361
simpl in |- *; apply lt_O_Sn.
362
unfold open_interval in |- *; simpl in |- *; rewrite H7; simpl in H13;
363
rewrite H13; unfold Rmin in |- *; case (Rle_dec a b);
364
intro; [ assumption | elim n; assumption ].
365
elim (le_Sn_O _ H10).
366
intros; simpl in H8; elim (lt_n_O _ H8).
367
intros; simpl in H8; inversion H8;
368
[ simpl in |- *; assumption | elim (le_Sn_O _ H10) ].
369
assert (Hyp_min : Rmin t2 b = t2).
370
unfold Rmin in |- *; case (Rle_dec t2 b); intro;
371
[ reflexivity | elim n; assumption ].
372
unfold adapted_couple in H6; elim H6; clear H6; intros;
373
elim (RList_P20 _ (StepFun_P9 H6 H7)); intros s1 [s2 [s3 H9]];
374
induction lf' as [| r2 lf' Hreclf'].
375
unfold adapted_couple in H6; decompose [and] H6; rewrite H9 in H13;
376
simpl in H13; discriminate.
377
clear Hreclf'; case (Req_dec r1 r2); intro.
378
case (Req_dec (f t2) r1); intro.
379
exists (cons t1 (cons s2 s3)); exists (cons r1 lf'); rewrite H3 in H1;
380
rewrite H9 in H6; unfold adapted_couple in H6, H1;
381
decompose [and] H1; decompose [and] H6; clear H1 H6;
382
unfold adapted_couple_opt in |- *; unfold adapted_couple in |- *;
384
unfold ordered_Rlist in |- *; intros; simpl in H1;
385
induction i as [| i Hreci].
386
simpl in |- *; apply Rle_trans with s1.
389
simpl in |- *; apply lt_O_Sn.
390
simpl in H19; rewrite H19; symmetry in |- *; apply Hyp_min.
391
apply (H16 0%nat); simpl in |- *; apply lt_O_Sn.
392
change (pos_Rl (cons s2 s3) i <= pos_Rl (cons s2 s3) (S i)) in |- *;
393
apply (H16 (S i)); simpl in |- *; assumption.
394
simpl in |- *; simpl in H14; rewrite H14; reflexivity.
395
simpl in |- *; simpl in H18; rewrite H18; unfold Rmax in |- *;
396
case (Rle_dec a b); case (Rle_dec t2 b); intros; reflexivity || elim n;
398
simpl in |- *; simpl in H20; apply H20.
399
intros; simpl in H1; unfold constant_D_eq, open_interval in |- *; intros;
400
induction i as [| i Hreci].
401
simpl in |- *; simpl in H6; case (total_order_T x t2); intro.
404
[ simpl in |- *; apply lt_O_Sn
405
| unfold open_interval in |- *; simpl in |- *; elim H6; intros; split;
407
rewrite b0; assumption.
408
rewrite H10; apply (H22 0%nat);
409
[ simpl in |- *; apply lt_O_Sn
410
| unfold open_interval in |- *; simpl in |- *; replace s1 with t2;
411
[ elim H6; intros; split; assumption
412
| simpl in H19; rewrite H19; rewrite Hyp_min; reflexivity ] ].
413
simpl in |- *; simpl in H6; apply (H22 (S i));
414
[ simpl in |- *; assumption
415
| unfold open_interval in |- *; simpl in |- *; apply H6 ].
416
intros; simpl in H1; rewrite H10;
418
(pos_Rl (cons r2 lf') i <> pos_Rl (cons r2 lf') (S i) \/
419
f (pos_Rl (cons s1 (cons s2 s3)) (S i)) <> pos_Rl (cons r2 lf') i)
420
in |- *; rewrite <- H9; elim H8; intros; apply H6;
421
simpl in |- *; apply H1.
422
intros; induction i as [| i Hreci].
423
simpl in |- *; red in |- *; intro; elim Hyp_eq; apply Rle_antisym.
424
apply (H12 0%nat); simpl in |- *; apply lt_O_Sn.
425
rewrite <- Hyp_min; rewrite H6; simpl in H19; rewrite <- H19;
426
apply (H16 0%nat); simpl in |- *; apply lt_O_Sn.
427
elim H8; intros; rewrite H9 in H21; apply (H21 (S i)); simpl in |- *;
428
simpl in H1; apply H1.
429
exists (cons t1 l'); exists (cons r1 (cons r2 lf')); rewrite H9 in H6;
430
rewrite H3 in H1; unfold adapted_couple in H1, H6;
431
decompose [and] H6; decompose [and] H1; clear H6 H1;
432
unfold adapted_couple_opt in |- *; unfold adapted_couple in |- *;
434
rewrite H9; unfold ordered_Rlist in |- *; intros; simpl in H1;
435
induction i as [| i Hreci].
436
simpl in |- *; replace s1 with t2.
437
apply (H16 0%nat); simpl in |- *; apply lt_O_Sn.
438
simpl in H14; rewrite H14; rewrite Hyp_min; reflexivity.
440
(pos_Rl (cons s1 (cons s2 s3)) i <= pos_Rl (cons s1 (cons s2 s3)) (S i))
441
in |- *; apply (H12 i); simpl in |- *; apply lt_S_n;
443
simpl in |- *; simpl in H19; apply H19.
444
rewrite H9; simpl in |- *; simpl in H13; rewrite H13; unfold Rmax in |- *;
445
case (Rle_dec t2 b); case (Rle_dec a b); intros; reflexivity || elim n;
447
rewrite H9; simpl in |- *; simpl in H15; rewrite H15; reflexivity.
448
intros; simpl in H1; unfold constant_D_eq, open_interval in |- *; intros;
449
induction i as [| i Hreci].
450
simpl in |- *; rewrite H9 in H6; simpl in H6; apply (H22 0%nat).
451
simpl in |- *; apply lt_O_Sn.
452
unfold open_interval in |- *; simpl in |- *.
455
simpl in H14; rewrite H14; rewrite Hyp_min; reflexivity.
456
change (f x = pos_Rl (cons r2 lf') i) in |- *; clear Hreci; apply (H17 i).
457
simpl in |- *; rewrite H9 in H1; simpl in H1; apply lt_S_n; apply H1.
458
rewrite H9 in H6; unfold open_interval in |- *; apply H6.
459
intros; simpl in H1; induction i as [| i Hreci].
460
simpl in |- *; rewrite H9; right; simpl in |- *; replace s1 with t2.
462
simpl in H14; rewrite H14; rewrite Hyp_min; reflexivity.
463
elim H8; intros; apply (H6 i).
464
simpl in |- *; apply lt_S_n; apply H1.
465
intros; rewrite H9; induction i as [| i Hreci].
466
simpl in |- *; red in |- *; intro; elim Hyp_eq; apply Rle_antisym.
467
apply (H16 0%nat); simpl in |- *; apply lt_O_Sn.
468
rewrite <- Hyp_min; rewrite H6; simpl in H14; rewrite <- H14; right;
470
elim H8; intros; rewrite <- H9; apply (H21 i); rewrite H9; rewrite H9 in H1;
471
simpl in |- *; simpl in H1; apply lt_S_n; apply H1.
472
exists (cons t1 l'); exists (cons r1 (cons r2 lf')); rewrite H9 in H6;
473
rewrite H3 in H1; unfold adapted_couple in H1, H6;
474
decompose [and] H6; decompose [and] H1; clear H6 H1;
475
unfold adapted_couple_opt in |- *; unfold adapted_couple in |- *;
477
rewrite H9; unfold ordered_Rlist in |- *; intros; simpl in H1;
478
induction i as [| i Hreci].
479
simpl in |- *; replace s1 with t2.
480
apply (H15 0%nat); simpl in |- *; apply lt_O_Sn.
481
simpl in H13; rewrite H13; rewrite Hyp_min; reflexivity.
483
(pos_Rl (cons s1 (cons s2 s3)) i <= pos_Rl (cons s1 (cons s2 s3)) (S i))
484
in |- *; apply (H11 i); simpl in |- *; apply lt_S_n;
486
simpl in |- *; simpl in H18; apply H18.
487
rewrite H9; simpl in |- *; simpl in H12; rewrite H12; unfold Rmax in |- *;
488
case (Rle_dec t2 b); case (Rle_dec a b); intros; reflexivity || elim n;
490
rewrite H9; simpl in |- *; simpl in H14; rewrite H14; reflexivity.
491
intros; simpl in H1; unfold constant_D_eq, open_interval in |- *; intros;
492
induction i as [| i Hreci].
493
simpl in |- *; rewrite H9 in H6; simpl in H6; apply (H21 0%nat).
494
simpl in |- *; apply lt_O_Sn.
495
unfold open_interval in |- *; simpl in |- *; replace t2 with s1.
497
simpl in H13; rewrite H13; rewrite Hyp_min; reflexivity.
498
change (f x = pos_Rl (cons r2 lf') i) in |- *; clear Hreci; apply (H16 i).
499
simpl in |- *; rewrite H9 in H1; simpl in H1; apply lt_S_n; apply H1.
500
rewrite H9 in H6; unfold open_interval in |- *; apply H6.
501
intros; simpl in H1; induction i as [| i Hreci].
502
simpl in |- *; left; assumption.
503
elim H8; intros; apply (H6 i).
504
simpl in |- *; apply lt_S_n; apply H1.
505
intros; rewrite H9; induction i as [| i Hreci].
506
simpl in |- *; red in |- *; intro; elim Hyp_eq; apply Rle_antisym.
507
apply (H15 0%nat); simpl in |- *; apply lt_O_Sn.
508
rewrite <- Hyp_min; rewrite H6; simpl in H13; rewrite <- H13; right;
510
elim H8; intros; rewrite <- H9; apply (H20 i); rewrite H9; rewrite H9 in H1;
511
simpl in |- *; simpl in H1; apply lt_S_n; apply H1.
512
rewrite H3 in H1; clear H4; unfold adapted_couple in H1; decompose [and] H1;
513
clear H1; clear H H7 H9; cut (Rmax a b = b);
514
[ intro; rewrite H in H5; rewrite <- H5; apply RList_P7;
515
[ assumption | simpl in |- *; right; left; reflexivity ]
516
| unfold Rmax in |- *; case (Rle_dec a b); intro;
517
[ reflexivity | elim n; assumption ] ].
521
forall (a b r r1 r3 s1 s2 r4:R) (r2 lf1 s3 lf2:Rlist)
524
adapted_couple f a b (cons r (cons r1 r2)) (cons r3 lf1) ->
525
adapted_couple_opt f a b (cons s1 (cons s2 s3)) (cons r4 lf2) -> r1 <= s2.
527
intros; unfold adapted_couple_opt in H1; elim H1; clear H1; intros;
528
unfold adapted_couple in H0, H1; decompose [and] H0;
529
decompose [and] H1; clear H0 H1; assert (H12 : r = s1).
530
simpl in H10; simpl in H5; rewrite H10; rewrite H5; reflexivity.
531
assert (H14 := H3 0%nat (lt_O_Sn _)); simpl in H14; elim H14; intro.
532
assert (H15 := H7 0%nat (lt_O_Sn _)); simpl in H15; elim H15; intro.
533
rewrite <- H12 in H1; case (Rle_dec r1 s2); intro; try assumption.
534
assert (H16 : s2 < r1); auto with real.
535
induction s3 as [| r0 s3 Hrecs3].
536
simpl in H9; rewrite H9 in H16; cut (r1 <= Rmax a b).
537
intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H17 H16)).
538
rewrite <- H4; apply RList_P7;
539
[ assumption | simpl in |- *; right; left; reflexivity ].
540
clear Hrecs3; induction lf2 as [| r5 lf2 Hreclf2].
541
simpl in H11; discriminate.
542
clear Hreclf2; assert (H17 : r3 = r4).
543
set (x := (r + s2) / 2); assert (H17 := H8 0%nat (lt_O_Sn _));
544
assert (H18 := H13 0%nat (lt_O_Sn _));
545
unfold constant_D_eq, open_interval in H17, H18; simpl in H17;
546
simpl in H18; rewrite <- (H17 x).
549
rewrite <- H12; unfold x in |- *; split.
550
apply Rmult_lt_reg_l with 2;
552
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
553
rewrite <- Rinv_r_sym;
554
[ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption
556
apply Rmult_lt_reg_l with 2;
558
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
559
rewrite <- Rinv_r_sym;
560
[ rewrite Rmult_1_l; rewrite (Rplus_comm r); rewrite double;
561
apply Rplus_lt_compat_l; assumption
563
unfold x in |- *; split.
564
apply Rmult_lt_reg_l with 2;
566
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
567
rewrite <- Rinv_r_sym;
568
[ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption
570
apply Rlt_trans with s2;
571
[ apply Rmult_lt_reg_l with 2;
573
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2));
574
rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym;
575
[ rewrite Rmult_1_l; rewrite (Rplus_comm r); rewrite double;
576
apply Rplus_lt_compat_l; assumption
579
assert (H18 : f s2 = r3).
581
[ simpl in |- *; apply lt_O_Sn
582
| unfold open_interval in |- *; simpl in |- *; split; assumption ].
583
assert (H19 : r3 = r5).
584
assert (H19 := H7 1%nat); simpl in H19;
585
assert (H20 := H19 (lt_n_S _ _ (lt_O_Sn _))); elim H20;
587
set (x := (s2 + Rmin r1 r0) / 2); assert (H22 := H8 0%nat);
588
assert (H23 := H13 1%nat); simpl in H22; simpl in H23;
589
rewrite <- (H22 (lt_O_Sn _) x).
590
rewrite <- (H23 (lt_n_S _ _ (lt_O_Sn _)) x).
592
unfold open_interval in |- *; simpl in |- *; unfold x in |- *; split.
593
apply Rmult_lt_reg_l with 2;
595
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
596
rewrite <- Rinv_r_sym;
597
[ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l;
598
unfold Rmin in |- *; case (Rle_dec r1 r0); intro;
601
apply Rmult_lt_reg_l with 2;
603
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
604
rewrite <- Rinv_r_sym;
605
[ rewrite Rmult_1_l; rewrite double;
606
apply Rlt_le_trans with (r0 + Rmin r1 r0);
607
[ do 2 rewrite <- (Rplus_comm (Rmin r1 r0)); apply Rplus_lt_compat_l;
609
| apply Rplus_le_compat_l; apply Rmin_r ]
611
unfold open_interval in |- *; simpl in |- *; unfold x in |- *; split.
612
apply Rlt_trans with s2;
614
| apply Rmult_lt_reg_l with 2;
616
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2));
617
rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym;
618
[ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l;
619
unfold Rmin in |- *; case (Rle_dec r1 r0);
622
apply Rmult_lt_reg_l with 2;
624
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
625
rewrite <- Rinv_r_sym;
626
[ rewrite Rmult_1_l; rewrite double;
627
apply Rlt_le_trans with (r1 + Rmin r1 r0);
628
[ do 2 rewrite <- (Rplus_comm (Rmin r1 r0)); apply Rplus_lt_compat_l;
630
| apply Rplus_le_compat_l; apply Rmin_l ]
632
elim H2; clear H2; intros; assert (H23 := H22 1%nat); simpl in H23;
633
assert (H24 := H23 (lt_n_S _ _ (lt_O_Sn _))); elim H24;
635
elim H2; intros; assert (H22 := H20 0%nat); simpl in H22;
636
assert (H23 := H22 (lt_O_Sn _)); elim H23; intro;
637
[ elim H24; rewrite <- H17; rewrite <- H19; reflexivity
638
| elim H24; rewrite <- H17; assumption ].
639
elim H2; clear H2; intros; assert (H17 := H16 0%nat); simpl in H17;
640
elim (H17 (lt_O_Sn _)); assumption.
641
rewrite <- H0; rewrite H12; apply (H7 0%nat); simpl in |- *; apply lt_O_Sn.
645
forall (a b:R) (f:R -> R) (l lf:Rlist),
646
adapted_couple_opt f a b l lf -> adapted_couple_opt f b a l lf.
648
unfold adapted_couple_opt in |- *; unfold adapted_couple in |- *; intros;
649
decompose [and] H; clear H; repeat split; try assumption.
650
rewrite H0; unfold Rmin in |- *; case (Rle_dec a b); intro;
651
case (Rle_dec b a); intro; try reflexivity.
652
apply Rle_antisym; assumption.
653
apply Rle_antisym; auto with real.
654
rewrite H3; unfold Rmax in |- *; case (Rle_dec a b); intro;
655
case (Rle_dec b a); intro; try reflexivity.
656
apply Rle_antisym; assumption.
657
apply Rle_antisym; auto with real.
661
forall (a b r r1 r3 s1 s2 r4:R) (r2 lf1 s3 lf2:Rlist)
664
adapted_couple f a b (cons r (cons r1 r2)) (cons r3 lf1) ->
665
adapted_couple_opt f a b (cons s1 (cons s2 s3)) (cons r4 lf2) -> r1 <= s2.
667
intros; case (total_order_T a b); intro.
669
eapply StepFun_P11; [ apply a0 | apply H0 | apply H1 ].
672
[ apply r0 | apply StepFun_P2; apply H0 | apply StepFun_P12; apply H1 ].
676
forall (f:R -> R) (l1 l2 lf1 lf2:Rlist) (a b:R),
678
adapted_couple f a b l1 lf1 ->
679
adapted_couple_opt f a b l2 lf2 -> Int_SF lf1 l1 = Int_SF lf2 l2.
682
intros l2 lf1 lf2 a b Hyp H H0; unfold adapted_couple in H; decompose [and] H;
683
clear H H0 H2 H3 H1 H6; simpl in H4; discriminate.
685
intros; case (Req_dec a b); intro.
686
unfold adapted_couple_opt in H2; elim H2; intros; rewrite (StepFun_P8 H4 H3);
687
rewrite (StepFun_P8 H1 H3); reflexivity.
688
assert (H4 := StepFun_P9 H1 H3); simpl in H4;
689
elim (le_Sn_O _ (le_S_n _ _ H4)).
690
intros; clear H; unfold adapted_couple_opt in H3; elim H3; clear H3; intros;
691
case (Req_dec a b); intro.
692
rewrite (StepFun_P8 H2 H4); rewrite (StepFun_P8 H H4); reflexivity.
693
assert (Hyp_min : Rmin a b = a).
694
unfold Rmin in |- *; case (Rle_dec a b); intro;
695
[ reflexivity | elim n; assumption ].
696
assert (Hyp_max : Rmax a b = b).
697
unfold Rmax in |- *; case (Rle_dec a b); intro;
698
[ reflexivity | elim n; assumption ].
699
elim (RList_P20 _ (StepFun_P9 H H4)); intros s1 [s2 [s3 H5]]; rewrite H5 in H;
700
rewrite H5; induction lf1 as [| r3 lf1 Hreclf1].
701
unfold adapted_couple in H2; decompose [and] H2;
702
clear H H2 H4 H5 H3 H6 H8 H7 H11; simpl in H9; discriminate.
703
clear Hreclf1; induction lf2 as [| r4 lf2 Hreclf2].
704
unfold adapted_couple in H; decompose [and] H;
705
clear H H2 H4 H5 H3 H6 H8 H7 H11; simpl in H9; discriminate.
706
clear Hreclf2; assert (H6 : r = s1).
707
unfold adapted_couple in H, H2; decompose [and] H; decompose [and] H2;
708
clear H H2; simpl in H13; simpl in H8; rewrite H13;
709
rewrite H8; reflexivity.
710
assert (H7 : r3 = r4 \/ r = r1).
711
case (Req_dec r r1); intro.
713
left; cut (r1 <= s2).
714
intro; unfold adapted_couple in H2, H; decompose [and] H; decompose [and] H2;
715
clear H H2; set (x := (r + r1) / 2); assert (H18 := H14 0%nat);
716
assert (H20 := H19 0%nat); unfold constant_D_eq, open_interval in H18, H20;
717
simpl in H18; simpl in H20; rewrite <- (H18 (lt_O_Sn _) x).
718
rewrite <- (H20 (lt_O_Sn _) x).
720
assert (H21 := H13 0%nat (lt_O_Sn _)); simpl in H21; elim H21; intro;
721
[ idtac | elim H7; assumption ]; unfold x in |- *;
723
apply Rmult_lt_reg_l with 2;
725
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
726
rewrite <- Rinv_r_sym;
727
[ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; apply H
729
apply Rmult_lt_reg_l with 2;
731
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
732
rewrite <- Rinv_r_sym;
733
[ rewrite Rmult_1_l; rewrite <- (Rplus_comm r1); rewrite double;
734
apply Rplus_lt_compat_l; apply H
736
rewrite <- H6; assert (H21 := H13 0%nat (lt_O_Sn _)); simpl in H21; elim H21;
737
intro; [ idtac | elim H7; assumption ]; unfold x in |- *;
739
apply Rmult_lt_reg_l with 2;
741
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
742
rewrite <- Rinv_r_sym;
743
[ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; apply H
745
apply Rlt_le_trans with r1;
746
[ apply Rmult_lt_reg_l with 2;
748
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2));
749
rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym;
750
[ rewrite Rmult_1_l; rewrite <- (Rplus_comm r1); rewrite double;
751
apply Rplus_lt_compat_l; apply H
757
unfold adapted_couple_opt in |- *; split.
759
rewrite H5 in H3; apply H3.
760
assert (H8 : r1 <= s2).
764
unfold adapted_couple_opt in |- *; split.
766
rewrite H5 in H3; apply H3.
768
simpl in |- *; elim H8; intro.
769
replace (r4 * (s2 - s1)) with (r3 * (r1 - r) + r3 * (s2 - r1));
770
[ idtac | rewrite H9; rewrite H6; ring ].
771
rewrite Rplus_assoc; apply Rplus_eq_compat_l;
773
(Int_SF lf1 (cons r1 r2) = Int_SF (cons r3 lf2) (cons r1 (cons s2 s3)))
774
in |- *; apply H0 with r1 b.
775
unfold adapted_couple in H2; decompose [and] H2; clear H2;
776
replace b with (Rmax a b).
777
rewrite <- H12; apply RList_P7;
778
[ assumption | simpl in |- *; right; left; reflexivity ].
782
unfold adapted_couple_opt in |- *; split.
783
apply StepFun_P7 with a a r3.
785
unfold adapted_couple in H2, H; decompose [and] H2; decompose [and] H;
786
clear H H2; assert (H20 : r = a).
787
simpl in H13; rewrite H13; apply Hyp_min.
788
unfold adapted_couple in |- *; repeat split.
789
unfold ordered_Rlist in |- *; intros; simpl in H; induction i as [| i Hreci].
790
simpl in |- *; rewrite <- H20; apply (H11 0%nat).
791
simpl in |- *; apply lt_O_Sn.
792
induction i as [| i Hreci0].
793
simpl in |- *; assumption.
794
change (pos_Rl (cons s2 s3) i <= pos_Rl (cons s2 s3) (S i)) in |- *;
795
apply (H15 (S i)); simpl in |- *; apply lt_S_n; assumption.
796
simpl in |- *; symmetry in |- *; apply Hyp_min.
797
rewrite <- H17; reflexivity.
798
simpl in H19; simpl in |- *; rewrite H19; reflexivity.
799
intros; simpl in H; unfold constant_D_eq, open_interval in |- *; intros;
800
induction i as [| i Hreci].
801
simpl in |- *; apply (H16 0%nat).
802
simpl in |- *; apply lt_O_Sn.
803
simpl in H2; rewrite <- H20 in H2; unfold open_interval in |- *;
804
simpl in |- *; apply H2.
805
clear Hreci; induction i as [| i Hreci].
806
simpl in |- *; simpl in H2; rewrite H9; apply (H21 0%nat).
807
simpl in |- *; apply lt_O_Sn.
808
unfold open_interval in |- *; simpl in |- *; elim H2; intros; split.
809
apply Rle_lt_trans with r1; try assumption; rewrite <- H6; apply (H11 0%nat);
810
simpl in |- *; apply lt_O_Sn.
812
clear Hreci; simpl in |- *; apply (H21 (S i)).
813
simpl in |- *; apply lt_S_n; assumption.
814
unfold open_interval in |- *; apply H2.
815
elim H3; clear H3; intros; split.
819
(i < pred (Rlength (cons r4 lf2)))%nat ->
820
pos_Rl (cons r4 lf2) i <> pos_Rl (cons r4 lf2) (S i) \/
821
f (pos_Rl (cons s1 (cons s2 s3)) (S i)) <> pos_Rl (cons r4 lf2) i)
822
in |- *; rewrite <- H5; apply H3.
823
rewrite H5 in H11; intros; simpl in H12; induction i as [| i Hreci].
824
simpl in |- *; red in |- *; intro; rewrite H13 in H10;
825
elim (Rlt_irrefl _ H10).
826
clear Hreci; apply (H11 (S i)); simpl in |- *; apply H12.
827
rewrite H9; rewrite H10; rewrite H6; apply Rplus_eq_compat_l; rewrite <- H10;
829
unfold adapted_couple in H2; decompose [and] H2; clear H2;
830
replace b with (Rmax a b).
831
rewrite <- H12; apply RList_P7;
832
[ assumption | simpl in |- *; right; left; reflexivity ].
836
unfold adapted_couple_opt in |- *; split.
837
apply StepFun_P7 with a a r3.
839
unfold adapted_couple in H2, H; decompose [and] H2; decompose [and] H;
840
clear H H2; assert (H20 : r = a).
841
simpl in H13; rewrite H13; apply Hyp_min.
842
unfold adapted_couple in |- *; repeat split.
843
unfold ordered_Rlist in |- *; intros; simpl in H; induction i as [| i Hreci].
844
simpl in |- *; rewrite <- H20; apply (H11 0%nat); simpl in |- *;
846
rewrite H10; apply (H15 (S i)); simpl in |- *; assumption.
847
simpl in |- *; symmetry in |- *; apply Hyp_min.
848
rewrite <- H17; rewrite H10; reflexivity.
849
simpl in H19; simpl in |- *; apply H19.
850
intros; simpl in H; unfold constant_D_eq, open_interval in |- *; intros;
851
induction i as [| i Hreci].
852
simpl in |- *; apply (H16 0%nat).
853
simpl in |- *; apply lt_O_Sn.
854
simpl in H2; rewrite <- H20 in H2; unfold open_interval in |- *;
855
simpl in |- *; apply H2.
856
clear Hreci; simpl in |- *; apply (H21 (S i)).
857
simpl in |- *; assumption.
858
rewrite <- H10; unfold open_interval in |- *; apply H2.
859
elim H3; clear H3; intros; split.
860
rewrite H5 in H3; intros; apply (H3 (S i)).
861
simpl in |- *; replace (Rlength lf2) with (S (pred (Rlength lf2))).
862
apply lt_n_S; apply H12.
863
symmetry in |- *; apply S_pred with 0%nat; apply neq_O_lt; red in |- *;
864
intro; rewrite <- H13 in H12; elim (lt_n_O _ H12).
865
intros; simpl in H12; rewrite H10; rewrite H5 in H11; apply (H11 (S i));
866
simpl in |- *; apply lt_n_S; apply H12.
867
simpl in |- *; rewrite H9; unfold Rminus in |- *; rewrite Rplus_opp_r;
868
rewrite Rmult_0_r; rewrite Rplus_0_l;
870
(Int_SF lf1 (cons r1 r2) = Int_SF (cons r4 lf2) (cons s1 (cons s2 s3)))
873
2: rewrite H5 in H3; unfold adapted_couple_opt in |- *; split; assumption.
874
assert (H10 : r = a).
875
unfold adapted_couple in H2; decompose [and] H2; clear H2; simpl in H12;
876
rewrite H12; apply Hyp_min.
877
rewrite <- H9; rewrite H10; apply StepFun_P7 with a r r3;
879
| pattern a at 2 in |- *; rewrite <- H10; pattern r at 2 in |- *; rewrite H9;
884
forall (f:R -> R) (l1 l2 lf1 lf2:Rlist) (a b:R),
885
adapted_couple f a b l1 lf1 ->
886
adapted_couple_opt f a b l2 lf2 -> Int_SF lf1 l1 = Int_SF lf2 l2.
888
intros; case (Rle_dec a b); intro;
889
[ apply (StepFun_P14 r H H0)
890
| assert (H1 : b <= a);
892
| eapply StepFun_P14;
893
[ apply H1 | apply StepFun_P2; apply H | apply StepFun_P12; apply H0 ] ] ].
897
forall (f:R -> R) (l lf:Rlist) (a b:R),
898
adapted_couple f a b l lf ->
900
(exists lf' : Rlist, adapted_couple_opt f a b l' lf').
902
intros; case (Rle_dec a b); intro;
903
[ apply (StepFun_P10 r H)
904
| assert (H1 : b <= a);
906
| assert (H2 := StepFun_P10 H1 (StepFun_P2 H)); elim H2;
907
intros l' [lf' H3]; exists l'; exists lf'; apply StepFun_P12;
912
forall (f:R -> R) (l1 l2 lf1 lf2:Rlist) (a b:R),
913
adapted_couple f a b l1 lf1 ->
914
adapted_couple f a b l2 lf2 -> Int_SF lf1 l1 = Int_SF lf2 l2.
916
intros; elim (StepFun_P16 H); intros l' [lf' H1]; rewrite (StepFun_P15 H H1);
917
rewrite (StepFun_P15 H0 H1); reflexivity.
921
forall a b c:R, RiemannInt_SF (mkStepFun (StepFun_P4 a b c)) = c * (b - a).
923
intros; unfold RiemannInt_SF in |- *; case (Rle_dec a b); intro.
925
(Int_SF (subdivision_val (mkStepFun (StepFun_P4 a b c)))
926
(subdivision (mkStepFun (StepFun_P4 a b c)))) with
927
(Int_SF (cons c nil) (cons a (cons b nil)));
928
[ simpl in |- *; ring
929
| apply StepFun_P17 with (fct_cte c) a b;
930
[ apply StepFun_P3; assumption
931
| apply (StepFun_P1 (mkStepFun (StepFun_P4 a b c))) ] ].
933
(Int_SF (subdivision_val (mkStepFun (StepFun_P4 a b c)))
934
(subdivision (mkStepFun (StepFun_P4 a b c)))) with
935
(Int_SF (cons c nil) (cons b (cons a nil)));
936
[ simpl in |- *; ring
937
| apply StepFun_P17 with (fct_cte c) a b;
938
[ apply StepFun_P2; apply StepFun_P3; auto with real
939
| apply (StepFun_P1 (mkStepFun (StepFun_P4 a b c))) ] ].
943
forall (l1:Rlist) (f g:R -> R) (l:R),
944
Int_SF (FF l1 (fun x:R => f x + l * g x)) l1 =
945
Int_SF (FF l1 f) l1 + l * Int_SF (FF l1 g) l1.
947
intros; induction l1 as [| r l1 Hrecl1];
948
[ simpl in |- *; ring
949
| induction l1 as [| r0 l1 Hrecl0]; simpl in |- *;
950
[ ring | simpl in Hrecl1; rewrite Hrecl1; ring ] ].
954
forall (l:Rlist) (f:R -> R),
955
(0 < Rlength l)%nat -> Rlength l = S (Rlength (FF l f)).
957
intros l f H; induction l;
958
[ elim (lt_irrefl _ H)
959
| simpl in |- *; rewrite RList_P18; rewrite RList_P14; reflexivity ].
963
forall (a b:R) (f:R -> R) (l:Rlist),
964
is_subdivision f a b l -> adapted_couple f a b l (FF l f).
966
intros; unfold adapted_couple in |- *; unfold is_subdivision in X;
967
unfold adapted_couple in X; elim X; clear X; intros;
968
decompose [and] p; clear p; repeat split; try assumption.
969
apply StepFun_P20; rewrite H2; apply lt_O_Sn.
970
intros; assert (H5 := H4 _ H3); unfold constant_D_eq, open_interval in H5;
971
unfold constant_D_eq, open_interval in |- *; intros;
972
induction l as [| r l Hrecl].
974
unfold FF in |- *; rewrite RList_P12.
976
change (f x0 = f (pos_Rl (mid_Rlist (cons r l) r) (S i))) in |- *;
977
rewrite RList_P13; try assumption; rewrite (H5 x0 H6);
981
apply Rmult_lt_reg_l with 2;
983
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
984
rewrite <- Rinv_r_sym;
985
[ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; elim H6;
986
intros; apply Rlt_trans with x0; assumption
988
apply Rmult_lt_reg_l with 2;
990
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
991
rewrite <- Rinv_r_sym;
992
[ rewrite Rmult_1_l; rewrite double;
993
rewrite (Rplus_comm (pos_Rl (cons r l) i));
994
apply Rplus_lt_compat_l; elim H6; intros; apply Rlt_trans with x0;
997
rewrite RList_P14; simpl in H3; apply H3.
1001
forall (a b:R) (f g:R -> R) (lf lg:Rlist),
1003
is_subdivision f a b lf ->
1004
is_subdivision g a b lg -> is_subdivision f a b (cons_ORlist lf lg).
1006
unfold is_subdivision in |- *; intros a b f g lf lg Hyp X X0; elim X; elim X0;
1007
clear X X0; intros lg0 p lf0 p0; assert (Hyp_min : Rmin a b = a).
1008
unfold Rmin in |- *; case (Rle_dec a b); intro;
1009
[ reflexivity | elim n; assumption ].
1010
assert (Hyp_max : Rmax a b = b).
1011
unfold Rmax in |- *; case (Rle_dec a b); intro;
1012
[ reflexivity | elim n; assumption ].
1013
apply existT with (FF (cons_ORlist lf lg) f); unfold adapted_couple in p, p0;
1014
decompose [and] p; decompose [and] p0; clear p p0;
1015
rewrite Hyp_min in H6; rewrite Hyp_min in H1; rewrite Hyp_max in H0;
1016
rewrite Hyp_max in H5; unfold adapted_couple in |- *;
1018
apply RList_P2; assumption.
1019
rewrite Hyp_min; symmetry in |- *; apply Rle_antisym.
1020
induction lf as [| r lf Hreclf].
1021
simpl in |- *; right; symmetry in |- *; assumption.
1024
In (pos_Rl (cons_ORlist (cons r lf) lg) 0) (cons_ORlist (cons r lf) lg)).
1026
(RList_P3 (cons_ORlist (cons r lf) lg)
1027
(pos_Rl (cons_ORlist (cons r lf) lg) 0)); intros _ H10;
1028
apply H10; exists 0%nat; split;
1029
[ reflexivity | rewrite RList_P11; simpl in |- *; apply lt_O_Sn ].
1030
elim (RList_P9 (cons r lf) lg (pos_Rl (cons_ORlist (cons r lf) lg) 0));
1031
intros H12 _; assert (H13 := H12 H10); elim H13; intro.
1032
elim (RList_P3 (cons r lf) (pos_Rl (cons_ORlist (cons r lf) lg) 0));
1033
intros H11 _; assert (H14 := H11 H8); elim H14; intros;
1034
elim H15; clear H15; intros; rewrite H15; rewrite <- H6;
1035
elim (RList_P6 (cons r lf)); intros; apply H17;
1036
[ assumption | apply le_O_n | assumption ].
1037
elim (RList_P3 lg (pos_Rl (cons_ORlist (cons r lf) lg) 0)); intros H11 _;
1038
assert (H14 := H11 H8); elim H14; intros; elim H15;
1039
clear H15; intros; rewrite H15; rewrite <- H1; elim (RList_P6 lg);
1040
intros; apply H17; [ assumption | apply le_O_n | assumption ].
1041
induction lf as [| r lf Hreclf].
1042
simpl in |- *; right; assumption.
1043
assert (H8 : In a (cons_ORlist (cons r lf) lg)).
1044
elim (RList_P9 (cons r lf) lg a); intros; apply H10; left;
1045
elim (RList_P3 (cons r lf) a); intros; apply H12;
1046
exists 0%nat; split;
1047
[ symmetry in |- *; assumption | simpl in |- *; apply lt_O_Sn ].
1048
apply RList_P5; [ apply RList_P2; assumption | assumption ].
1049
rewrite Hyp_max; apply Rle_antisym.
1050
induction lf as [| r lf Hreclf].
1051
simpl in |- *; right; assumption.
1055
(pos_Rl (cons_ORlist (cons r lf) lg)
1056
(pred (Rlength (cons_ORlist (cons r lf) lg))))
1057
(cons_ORlist (cons r lf) lg)).
1059
(RList_P3 (cons_ORlist (cons r lf) lg)
1060
(pos_Rl (cons_ORlist (cons r lf) lg)
1061
(pred (Rlength (cons_ORlist (cons r lf) lg)))));
1062
intros _ H10; apply H10;
1063
exists (pred (Rlength (cons_ORlist (cons r lf) lg)));
1064
split; [ reflexivity | rewrite RList_P11; simpl in |- *; apply lt_n_Sn ].
1066
(RList_P9 (cons r lf) lg
1067
(pos_Rl (cons_ORlist (cons r lf) lg)
1068
(pred (Rlength (cons_ORlist (cons r lf) lg)))));
1070
assert (H11 := H10 H8); elim H11; intro.
1072
(RList_P3 (cons r lf)
1073
(pos_Rl (cons_ORlist (cons r lf) lg)
1074
(pred (Rlength (cons_ORlist (cons r lf) lg)))));
1075
intros H13 _; assert (H14 := H13 H12); elim H14; intros;
1076
elim H15; clear H15; intros; rewrite H15; rewrite <- H5;
1077
elim (RList_P6 (cons r lf)); intros; apply H17;
1079
| simpl in |- *; simpl in H14; apply lt_n_Sm_le; assumption
1080
| simpl in |- *; apply lt_n_Sn ].
1083
(pos_Rl (cons_ORlist (cons r lf) lg)
1084
(pred (Rlength (cons_ORlist (cons r lf) lg)))));
1085
intros H13 _; assert (H14 := H13 H12); elim H14; intros;
1086
elim H15; clear H15; intros.
1087
rewrite H15; assert (H17 : Rlength lg = S (pred (Rlength lg))).
1088
apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro;
1089
rewrite <- H17 in H16; elim (lt_n_O _ H16).
1090
rewrite <- H0; elim (RList_P6 lg); intros; apply H18;
1092
| rewrite H17 in H16; apply lt_n_Sm_le; assumption
1093
| apply lt_pred_n_n; rewrite H17; apply lt_O_Sn ].
1094
induction lf as [| r lf Hreclf].
1095
simpl in |- *; right; symmetry in |- *; assumption.
1096
assert (H8 : In b (cons_ORlist (cons r lf) lg)).
1097
elim (RList_P9 (cons r lf) lg b); intros; apply H10; left;
1098
elim (RList_P3 (cons r lf) b); intros; apply H12;
1099
exists (pred (Rlength (cons r lf))); split;
1100
[ symmetry in |- *; assumption | simpl in |- *; apply lt_n_Sn ].
1101
apply RList_P7; [ apply RList_P2; assumption | assumption ].
1102
apply StepFun_P20; rewrite RList_P11; rewrite H2; rewrite H7; simpl in |- *;
1104
intros; unfold constant_D_eq, open_interval in |- *; intros;
1108
(open_interval (pos_Rl (cons_ORlist lf lg) i)
1109
(pos_Rl (cons_ORlist lf lg) (S i))) l).
1110
intros; elim H11; clear H11; intros; assert (H12 := H11);
1113
exists r : R, (exists r0 : Rlist, cons_ORlist lf lg = cons r r0)).
1114
apply RList_P19; red in |- *; intro; rewrite H13 in H8; elim (lt_n_O _ H8).
1115
elim Hyp_cons; clear Hyp_cons; intros r [r0 Hyp_cons]; rewrite Hyp_cons;
1116
unfold FF in |- *; rewrite RList_P12.
1117
change (f x = f (pos_Rl (mid_Rlist (cons r r0) r) (S i))) in |- *;
1118
rewrite <- Hyp_cons; rewrite RList_P13.
1119
assert (H13 := RList_P2 _ _ H _ H8); elim H13; intro.
1120
unfold constant_D_eq, open_interval in H11, H12; rewrite (H11 x H10);
1123
pos_Rl (cons_ORlist lf lg) i <
1124
(pos_Rl (cons_ORlist lf lg) i + pos_Rl (cons_ORlist lf lg) (S i)) / 2 <
1125
pos_Rl (cons_ORlist lf lg) (S i)).
1127
apply Rmult_lt_reg_l with 2;
1129
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
1130
rewrite <- Rinv_r_sym;
1131
[ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption
1133
apply Rmult_lt_reg_l with 2;
1135
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
1136
rewrite <- Rinv_r_sym;
1137
[ rewrite Rmult_1_l; rewrite double;
1138
rewrite (Rplus_comm (pos_Rl (cons_ORlist lf lg) i));
1139
apply Rplus_lt_compat_l; assumption
1141
rewrite (H11 _ H15); reflexivity.
1142
elim H10; intros; rewrite H14 in H15;
1143
elim (Rlt_irrefl _ (Rlt_trans _ _ _ H16 H15)).
1145
rewrite RList_P14; rewrite Hyp_cons in H8; simpl in H8; apply H8.
1146
assert (H11 : a < b).
1147
apply Rle_lt_trans with (pos_Rl (cons_ORlist lf lg) i).
1148
rewrite <- H6; rewrite <- (RList_P15 lf lg).
1149
elim (RList_P6 (cons_ORlist lf lg)); intros; apply H11.
1150
apply RList_P2; assumption.
1152
apply lt_trans with (pred (Rlength (cons_ORlist lf lg)));
1154
| apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro;
1155
rewrite <- H13 in H8; elim (lt_n_O _ H8) ].
1158
rewrite H1; assumption.
1159
apply Rlt_le_trans with (pos_Rl (cons_ORlist lf lg) (S i)).
1160
elim H10; intros; apply Rlt_trans with x; assumption.
1161
rewrite <- H5; rewrite <- (RList_P16 lf lg); try assumption.
1162
elim (RList_P6 (cons_ORlist lf lg)); intros; apply H11.
1163
apply RList_P2; assumption.
1164
apply lt_n_Sm_le; apply lt_n_S; assumption.
1165
apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H8;
1167
rewrite H0; assumption.
1171
pos_Rl lf j <= pos_Rl (cons_ORlist lf lg) i /\ (j < Rlength lf)%nat);
1172
assert (H12 : Nbound I).
1173
unfold Nbound in |- *; exists (Rlength lf); intros; unfold I in H12; elim H12;
1174
intros; apply lt_le_weak; assumption.
1175
assert (H13 : exists n : nat, I n).
1176
exists 0%nat; unfold I in |- *; split.
1177
apply Rle_trans with (pos_Rl (cons_ORlist lf lg) 0).
1178
right; symmetry in |- *.
1179
apply RList_P15; try assumption; rewrite H1; assumption.
1180
elim (RList_P6 (cons_ORlist lf lg)); intros; apply H13.
1181
apply RList_P2; assumption.
1183
apply lt_trans with (pred (Rlength (cons_ORlist lf lg))).
1185
apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H15 in H8;
1187
apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H5;
1188
rewrite <- H6 in H11; rewrite <- H5 in H11; elim (Rlt_irrefl _ H11).
1189
assert (H14 := Nzorn H13 H12); elim H14; clear H14; intros x0 H14;
1190
exists (pos_Rl lf0 x0); unfold constant_D_eq, open_interval in |- *;
1191
intros; assert (H16 := H9 x0); assert (H17 : (x0 < pred (Rlength lf))%nat).
1192
elim H14; clear H14; intros; unfold I in H14; elim H14; clear H14; intros;
1193
apply lt_S_n; replace (S (pred (Rlength lf))) with (Rlength lf).
1195
2: apply lt_n_S; assumption.
1196
cut (x0 = pred (Rlength lf)).
1197
intro; rewrite H19 in H14; rewrite H5 in H14;
1198
cut (pos_Rl (cons_ORlist lf lg) i < b).
1199
intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H14 H21)).
1200
apply Rlt_le_trans with (pos_Rl (cons_ORlist lf lg) (S i)).
1201
elim H10; intros; apply Rlt_trans with x; assumption.
1203
apply Rle_trans with
1204
(pos_Rl (cons_ORlist lf lg) (pred (Rlength (cons_ORlist lf lg)))).
1205
elim (RList_P6 (cons_ORlist lf lg)); intros; apply H21.
1206
apply RList_P2; assumption.
1207
apply lt_n_Sm_le; apply lt_n_S; assumption.
1208
apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H23 in H8;
1210
right; apply RList_P16; try assumption; rewrite H0; assumption.
1211
rewrite <- H20; reflexivity.
1212
apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro;
1213
rewrite <- H19 in H18; elim (lt_n_O _ H18).
1214
assert (H18 := H16 H17); unfold constant_D_eq, open_interval in H18;
1217
elim H15; clear H15; intros; elim H14; clear H14; intros; unfold I in H14;
1218
elim H14; clear H14; intros; split.
1219
apply Rle_lt_trans with (pos_Rl (cons_ORlist lf lg) i); assumption.
1220
apply Rlt_le_trans with (pos_Rl (cons_ORlist lf lg) (S i)); try assumption.
1221
assert (H22 : (S x0 < Rlength lf)%nat).
1222
replace (Rlength lf) with (S (pred (Rlength lf)));
1223
[ apply lt_n_S; assumption
1224
| symmetry in |- *; apply S_pred with 0%nat; apply neq_O_lt; red in |- *;
1225
intro; rewrite <- H22 in H21; elim (lt_n_O _ H21) ].
1226
elim (Rle_dec (pos_Rl lf (S x0)) (pos_Rl (cons_ORlist lf lg) i)); intro.
1227
assert (H23 : (S x0 <= x0)%nat).
1228
apply H20; unfold I in |- *; split; assumption.
1229
elim (le_Sn_n _ H23).
1230
assert (H23 : pos_Rl (cons_ORlist lf lg) i < pos_Rl lf (S x0)).
1232
clear b0; apply RList_P17; try assumption.
1233
apply RList_P2; assumption.
1234
elim (RList_P9 lf lg (pos_Rl lf (S x0))); intros; apply H25; left;
1235
elim (RList_P3 lf (pos_Rl lf (S x0))); intros; apply H27;
1236
exists (S x0); split; [ reflexivity | apply H22 ].
1240
forall (a b:R) (f g:R -> R) (lf lg:Rlist),
1241
is_subdivision f a b lf ->
1242
is_subdivision g a b lg -> is_subdivision f a b (cons_ORlist lf lg).
1244
intros; case (Rle_dec a b); intro;
1245
[ apply StepFun_P22 with g; assumption
1246
| apply StepFun_P5; apply StepFun_P22 with g;
1248
| apply StepFun_P5; assumption
1249
| apply StepFun_P5; assumption ] ].
1253
forall (a b:R) (f g:R -> R) (lf lg:Rlist),
1255
is_subdivision f a b lf ->
1256
is_subdivision g a b lg -> is_subdivision g a b (cons_ORlist lf lg).
1258
unfold is_subdivision in |- *; intros a b f g lf lg Hyp X X0; elim X; elim X0;
1259
clear X X0; intros lg0 p lf0 p0; assert (Hyp_min : Rmin a b = a).
1260
unfold Rmin in |- *; case (Rle_dec a b); intro;
1261
[ reflexivity | elim n; assumption ].
1262
assert (Hyp_max : Rmax a b = b).
1263
unfold Rmax in |- *; case (Rle_dec a b); intro;
1264
[ reflexivity | elim n; assumption ].
1265
apply existT with (FF (cons_ORlist lf lg) g); unfold adapted_couple in p, p0;
1266
decompose [and] p; decompose [and] p0; clear p p0;
1267
rewrite Hyp_min in H1; rewrite Hyp_min in H6; rewrite Hyp_max in H0;
1268
rewrite Hyp_max in H5; unfold adapted_couple in |- *;
1270
apply RList_P2; assumption.
1271
rewrite Hyp_min; symmetry in |- *; apply Rle_antisym.
1272
induction lf as [| r lf Hreclf].
1273
simpl in |- *; right; symmetry in |- *; assumption.
1276
In (pos_Rl (cons_ORlist (cons r lf) lg) 0) (cons_ORlist (cons r lf) lg)).
1278
(RList_P3 (cons_ORlist (cons r lf) lg)
1279
(pos_Rl (cons_ORlist (cons r lf) lg) 0)); intros _ H10;
1280
apply H10; exists 0%nat; split;
1281
[ reflexivity | rewrite RList_P11; simpl in |- *; apply lt_O_Sn ].
1282
elim (RList_P9 (cons r lf) lg (pos_Rl (cons_ORlist (cons r lf) lg) 0));
1283
intros H12 _; assert (H13 := H12 H10); elim H13; intro.
1284
elim (RList_P3 (cons r lf) (pos_Rl (cons_ORlist (cons r lf) lg) 0));
1285
intros H11 _; assert (H14 := H11 H8); elim H14; intros;
1286
elim H15; clear H15; intros; rewrite H15; rewrite <- H6;
1287
elim (RList_P6 (cons r lf)); intros; apply H17;
1288
[ assumption | apply le_O_n | assumption ].
1289
elim (RList_P3 lg (pos_Rl (cons_ORlist (cons r lf) lg) 0)); intros H11 _;
1290
assert (H14 := H11 H8); elim H14; intros; elim H15;
1291
clear H15; intros; rewrite H15; rewrite <- H1; elim (RList_P6 lg);
1292
intros; apply H17; [ assumption | apply le_O_n | assumption ].
1293
induction lf as [| r lf Hreclf].
1294
simpl in |- *; right; assumption.
1295
assert (H8 : In a (cons_ORlist (cons r lf) lg)).
1296
elim (RList_P9 (cons r lf) lg a); intros; apply H10; left;
1297
elim (RList_P3 (cons r lf) a); intros; apply H12;
1298
exists 0%nat; split;
1299
[ symmetry in |- *; assumption | simpl in |- *; apply lt_O_Sn ].
1300
apply RList_P5; [ apply RList_P2; assumption | assumption ].
1301
rewrite Hyp_max; apply Rle_antisym.
1302
induction lf as [| r lf Hreclf].
1303
simpl in |- *; right; assumption.
1307
(pos_Rl (cons_ORlist (cons r lf) lg)
1308
(pred (Rlength (cons_ORlist (cons r lf) lg))))
1309
(cons_ORlist (cons r lf) lg)).
1311
(RList_P3 (cons_ORlist (cons r lf) lg)
1312
(pos_Rl (cons_ORlist (cons r lf) lg)
1313
(pred (Rlength (cons_ORlist (cons r lf) lg)))));
1314
intros _ H10; apply H10;
1315
exists (pred (Rlength (cons_ORlist (cons r lf) lg)));
1316
split; [ reflexivity | rewrite RList_P11; simpl in |- *; apply lt_n_Sn ].
1318
(RList_P9 (cons r lf) lg
1319
(pos_Rl (cons_ORlist (cons r lf) lg)
1320
(pred (Rlength (cons_ORlist (cons r lf) lg)))));
1321
intros H10 _; assert (H11 := H10 H8); elim H11; intro.
1323
(RList_P3 (cons r lf)
1324
(pos_Rl (cons_ORlist (cons r lf) lg)
1325
(pred (Rlength (cons_ORlist (cons r lf) lg)))));
1326
intros H13 _; assert (H14 := H13 H12); elim H14; intros;
1327
elim H15; clear H15; intros; rewrite H15; rewrite <- H5;
1328
elim (RList_P6 (cons r lf)); intros; apply H17;
1330
| simpl in |- *; simpl in H14; apply lt_n_Sm_le; assumption
1331
| simpl in |- *; apply lt_n_Sn ].
1334
(pos_Rl (cons_ORlist (cons r lf) lg)
1335
(pred (Rlength (cons_ORlist (cons r lf) lg)))));
1336
intros H13 _; assert (H14 := H13 H12); elim H14; intros;
1337
elim H15; clear H15; intros; rewrite H15;
1338
assert (H17 : Rlength lg = S (pred (Rlength lg))).
1339
apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro;
1340
rewrite <- H17 in H16; elim (lt_n_O _ H16).
1341
rewrite <- H0; elim (RList_P6 lg); intros; apply H18;
1343
| rewrite H17 in H16; apply lt_n_Sm_le; assumption
1344
| apply lt_pred_n_n; rewrite H17; apply lt_O_Sn ].
1345
induction lf as [| r lf Hreclf].
1346
simpl in |- *; right; symmetry in |- *; assumption.
1347
assert (H8 : In b (cons_ORlist (cons r lf) lg)).
1348
elim (RList_P9 (cons r lf) lg b); intros; apply H10; left;
1349
elim (RList_P3 (cons r lf) b); intros; apply H12;
1350
exists (pred (Rlength (cons r lf))); split;
1351
[ symmetry in |- *; assumption | simpl in |- *; apply lt_n_Sn ].
1352
apply RList_P7; [ apply RList_P2; assumption | assumption ].
1353
apply StepFun_P20; rewrite RList_P11; rewrite H7; rewrite H2; simpl in |- *;
1355
unfold constant_D_eq, open_interval in |- *; intros;
1359
(open_interval (pos_Rl (cons_ORlist lf lg) i)
1360
(pos_Rl (cons_ORlist lf lg) (S i))) l).
1361
intros; elim H11; clear H11; intros; assert (H12 := H11);
1364
exists r : R, (exists r0 : Rlist, cons_ORlist lf lg = cons r r0)).
1365
apply RList_P19; red in |- *; intro; rewrite H13 in H8; elim (lt_n_O _ H8).
1366
elim Hyp_cons; clear Hyp_cons; intros r [r0 Hyp_cons]; rewrite Hyp_cons;
1367
unfold FF in |- *; rewrite RList_P12.
1368
change (g x = g (pos_Rl (mid_Rlist (cons r r0) r) (S i))) in |- *;
1369
rewrite <- Hyp_cons; rewrite RList_P13.
1370
assert (H13 := RList_P2 _ _ H _ H8); elim H13; intro.
1371
unfold constant_D_eq, open_interval in H11, H12; rewrite (H11 x H10);
1374
pos_Rl (cons_ORlist lf lg) i <
1375
(pos_Rl (cons_ORlist lf lg) i + pos_Rl (cons_ORlist lf lg) (S i)) / 2 <
1376
pos_Rl (cons_ORlist lf lg) (S i)).
1378
apply Rmult_lt_reg_l with 2;
1380
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
1381
rewrite <- Rinv_r_sym;
1382
[ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption
1384
apply Rmult_lt_reg_l with 2;
1386
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
1387
rewrite <- Rinv_r_sym;
1388
[ rewrite Rmult_1_l; rewrite double;
1389
rewrite (Rplus_comm (pos_Rl (cons_ORlist lf lg) i));
1390
apply Rplus_lt_compat_l; assumption
1392
rewrite (H11 _ H15); reflexivity.
1393
elim H10; intros; rewrite H14 in H15;
1394
elim (Rlt_irrefl _ (Rlt_trans _ _ _ H16 H15)).
1396
rewrite RList_P14; rewrite Hyp_cons in H8; simpl in H8; apply H8.
1397
assert (H11 : a < b).
1398
apply Rle_lt_trans with (pos_Rl (cons_ORlist lf lg) i).
1399
rewrite <- H6; rewrite <- (RList_P15 lf lg); try assumption.
1400
elim (RList_P6 (cons_ORlist lf lg)); intros; apply H11.
1401
apply RList_P2; assumption.
1403
apply lt_trans with (pred (Rlength (cons_ORlist lf lg)));
1405
| apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro;
1406
rewrite <- H13 in H8; elim (lt_n_O _ H8) ].
1407
rewrite H1; assumption.
1408
apply Rlt_le_trans with (pos_Rl (cons_ORlist lf lg) (S i)).
1409
elim H10; intros; apply Rlt_trans with x; assumption.
1410
rewrite <- H5; rewrite <- (RList_P16 lf lg); try assumption.
1411
elim (RList_P6 (cons_ORlist lf lg)); intros; apply H11.
1412
apply RList_P2; assumption.
1413
apply lt_n_Sm_le; apply lt_n_S; assumption.
1414
apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H8;
1416
rewrite H0; assumption.
1420
pos_Rl lg j <= pos_Rl (cons_ORlist lf lg) i /\ (j < Rlength lg)%nat);
1421
assert (H12 : Nbound I).
1422
unfold Nbound in |- *; exists (Rlength lg); intros; unfold I in H12; elim H12;
1423
intros; apply lt_le_weak; assumption.
1424
assert (H13 : exists n : nat, I n).
1425
exists 0%nat; unfold I in |- *; split.
1426
apply Rle_trans with (pos_Rl (cons_ORlist lf lg) 0).
1427
right; symmetry in |- *; rewrite H1; rewrite <- H6; apply RList_P15;
1428
try assumption; rewrite H1; assumption.
1429
elim (RList_P6 (cons_ORlist lf lg)); intros; apply H13;
1430
[ apply RList_P2; assumption
1432
| apply lt_trans with (pred (Rlength (cons_ORlist lf lg)));
1434
| apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro;
1435
rewrite <- H15 in H8; elim (lt_n_O _ H8) ] ].
1436
apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H0;
1437
rewrite <- H1 in H11; rewrite <- H0 in H11; elim (Rlt_irrefl _ H11).
1438
assert (H14 := Nzorn H13 H12); elim H14; clear H14; intros x0 H14;
1439
exists (pos_Rl lg0 x0); unfold constant_D_eq, open_interval in |- *;
1440
intros; assert (H16 := H4 x0); assert (H17 : (x0 < pred (Rlength lg))%nat).
1441
elim H14; clear H14; intros; unfold I in H14; elim H14; clear H14; intros;
1442
apply lt_S_n; replace (S (pred (Rlength lg))) with (Rlength lg).
1444
2: apply lt_n_S; assumption.
1445
cut (x0 = pred (Rlength lg)).
1446
intro; rewrite H19 in H14; rewrite H0 in H14;
1447
cut (pos_Rl (cons_ORlist lf lg) i < b).
1448
intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H14 H21)).
1449
apply Rlt_le_trans with (pos_Rl (cons_ORlist lf lg) (S i)).
1450
elim H10; intros; apply Rlt_trans with x; assumption.
1452
apply Rle_trans with
1453
(pos_Rl (cons_ORlist lf lg) (pred (Rlength (cons_ORlist lf lg)))).
1454
elim (RList_P6 (cons_ORlist lf lg)); intros; apply H21.
1455
apply RList_P2; assumption.
1456
apply lt_n_Sm_le; apply lt_n_S; assumption.
1457
apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H23 in H8;
1459
right; rewrite H0; rewrite <- H5; apply RList_P16; try assumption.
1460
rewrite H0; assumption.
1461
rewrite <- H20; reflexivity.
1462
apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro;
1463
rewrite <- H19 in H18; elim (lt_n_O _ H18).
1464
assert (H18 := H16 H17); unfold constant_D_eq, open_interval in H18;
1467
elim H15; clear H15; intros; elim H14; clear H14; intros; unfold I in H14;
1468
elim H14; clear H14; intros; split.
1469
apply Rle_lt_trans with (pos_Rl (cons_ORlist lf lg) i); assumption.
1470
apply Rlt_le_trans with (pos_Rl (cons_ORlist lf lg) (S i)); try assumption.
1471
assert (H22 : (S x0 < Rlength lg)%nat).
1472
replace (Rlength lg) with (S (pred (Rlength lg))).
1473
apply lt_n_S; assumption.
1474
symmetry in |- *; apply S_pred with 0%nat; apply neq_O_lt; red in |- *;
1475
intro; rewrite <- H22 in H21; elim (lt_n_O _ H21).
1476
elim (Rle_dec (pos_Rl lg (S x0)) (pos_Rl (cons_ORlist lf lg) i)); intro.
1477
assert (H23 : (S x0 <= x0)%nat);
1478
[ apply H20; unfold I in |- *; split; assumption | elim (le_Sn_n _ H23) ].
1479
assert (H23 : pos_Rl (cons_ORlist lf lg) i < pos_Rl lg (S x0)).
1481
clear b0; apply RList_P17; try assumption;
1482
[ apply RList_P2; assumption
1483
| elim (RList_P9 lf lg (pos_Rl lg (S x0))); intros; apply H25; right;
1484
elim (RList_P3 lg (pos_Rl lg (S x0))); intros;
1485
apply H27; exists (S x0); split; [ reflexivity | apply H22 ] ].
1489
forall (a b:R) (f g:R -> R) (lf lg:Rlist),
1490
is_subdivision f a b lf ->
1491
is_subdivision g a b lg -> is_subdivision g a b (cons_ORlist lf lg).
1493
intros a b f g lf lg H H0; case (Rle_dec a b); intro;
1494
[ apply StepFun_P24 with f; assumption
1495
| apply StepFun_P5; apply StepFun_P24 with f;
1497
| apply StepFun_P5; assumption
1498
| apply StepFun_P5; assumption ] ].
1502
forall (a b l:R) (f g:R -> R) (l1:Rlist),
1503
is_subdivision f a b l1 ->
1504
is_subdivision g a b l1 ->
1505
is_subdivision (fun x:R => f x + l * g x) a b l1.
1507
intros a b l f g l1 (x0,(H0,(H1,(H2,(H3,H4)))))
1508
(x,(_,(_,(_,(_,H9))))).
1509
exists (FF l1 (fun x:R => f x + l * g x)); repeat split; try assumption.
1510
apply StepFun_P20; rewrite H3; auto with arith.
1511
intros i H8 x1 H10; unfold open_interval in H10, H9, H4;
1512
rewrite (H9 _ H8 _ H10); rewrite (H4 _ H8 _ H10);
1513
assert (H11 : l1 <> nil).
1514
red in |- *; intro H11; rewrite H11 in H8; elim (lt_n_O _ H8).
1515
destruct (RList_P19 _ H11) as (r,(r0,H12));
1516
rewrite H12; unfold FF in |- *;
1518
(pos_Rl x0 i + l * pos_Rl x i =
1520
(app_Rlist (mid_Rlist (cons r r0) r) (fun x2:R => f x2 + l * g x2))
1521
(S i)) in |- *; rewrite RList_P12.
1523
rewrite <- H12; rewrite (H9 _ H8); try rewrite (H4 _ H8);
1525
(elim H10; clear H10; intros; split;
1526
[ apply Rmult_lt_reg_l with 2;
1528
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2));
1529
rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym;
1530
[ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l;
1531
apply Rlt_trans with x1; assumption
1533
| apply Rmult_lt_reg_l with 2;
1535
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2));
1536
rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym;
1537
[ rewrite Rmult_1_l; rewrite double;
1538
rewrite (Rplus_comm (pos_Rl l1 i)); apply Rplus_lt_compat_l;
1539
apply Rlt_trans with x1; assumption
1541
rewrite <- H12; assumption.
1542
rewrite RList_P14; simpl in |- *; rewrite H12 in H8; simpl in H8;
1543
apply lt_n_S; apply H8.
1547
forall (a b l:R) (f g:R -> R) (lf lg:Rlist),
1548
is_subdivision f a b lf ->
1549
is_subdivision g a b lg ->
1550
is_subdivision (fun x:R => f x + l * g x) a b (cons_ORlist lf lg).
1552
intros a b l f g lf lg H H0; apply StepFun_P26;
1553
[ apply StepFun_P23 with g; assumption
1554
| apply StepFun_P25 with f; assumption ].
1557
(** The set of step functions on [a,b] is a vectorial space *)
1559
forall (a b l:R) (f g:StepFun a b), IsStepFun (fun x:R => f x + l * g x) a b.
1561
intros a b l f g; unfold IsStepFun in |- *; assert (H := pre f);
1562
assert (H0 := pre g); unfold IsStepFun in H, H0; elim H;
1563
elim H0; intros; apply existT with (cons_ORlist x0 x);
1564
apply StepFun_P27; assumption.
1568
forall (a b:R) (f:StepFun a b), is_subdivision f a b (subdivision f).
1570
intros a b f; unfold is_subdivision in |- *;
1571
apply existT with (subdivision_val f); apply StepFun_P1.
1575
forall (a b l:R) (f g:StepFun a b),
1576
RiemannInt_SF (mkStepFun (StepFun_P28 l f g)) =
1577
RiemannInt_SF f + l * RiemannInt_SF g.
1579
intros a b l f g; unfold RiemannInt_SF in |- *; case (Rle_dec a b);
1582
(Int_SF (subdivision_val (mkStepFun (StepFun_P28 l f g)))
1583
(subdivision (mkStepFun (StepFun_P28 l f g)))) with
1585
(FF (cons_ORlist (subdivision f) (subdivision g))
1586
(fun x:R => f x + l * g x))
1587
(cons_ORlist (subdivision f) (subdivision g)));
1588
[ rewrite StepFun_P19;
1590
(Int_SF (FF (cons_ORlist (subdivision f) (subdivision g)) f)
1591
(cons_ORlist (subdivision f) (subdivision g))) with
1592
(Int_SF (subdivision_val f) (subdivision f));
1594
(Int_SF (FF (cons_ORlist (subdivision f) (subdivision g)) g)
1595
(cons_ORlist (subdivision f) (subdivision g))) with
1596
(Int_SF (subdivision_val g) (subdivision g));
1598
| apply StepFun_P17 with (fe g) a b;
1600
| apply StepFun_P21; apply StepFun_P25 with (fe f);
1601
apply StepFun_P29 ] ]
1602
| apply StepFun_P17 with (fe f) a b;
1604
| apply StepFun_P21; apply StepFun_P23 with (fe g);
1605
apply StepFun_P29 ] ]
1606
| apply StepFun_P17 with (fun x:R => f x + l * g x) a b;
1607
[ apply StepFun_P21; apply StepFun_P27; apply StepFun_P29
1608
| apply (StepFun_P1 (mkStepFun (StepFun_P28 l f g))) ] ]).
1612
forall (a b:R) (f:R -> R) (l lf:Rlist),
1613
adapted_couple f a b l lf ->
1614
adapted_couple (fun x:R => Rabs (f x)) a b l (app_Rlist lf Rabs).
1616
unfold adapted_couple in |- *; intros; decompose [and] H; clear H;
1617
repeat split; try assumption.
1618
symmetry in |- *; rewrite H3; rewrite RList_P18; reflexivity.
1619
intros; unfold constant_D_eq, open_interval in |- *;
1620
unfold constant_D_eq, open_interval in H5; intros;
1621
rewrite (H5 _ H _ H4); rewrite RList_P12;
1622
[ reflexivity | rewrite H3 in H; simpl in H; apply H ].
1626
forall (a b:R) (f:StepFun a b), IsStepFun (fun x:R => Rabs (f x)) a b.
1628
intros a b f; unfold IsStepFun in |- *; apply existT with (subdivision f);
1629
unfold is_subdivision in |- *;
1630
apply existT with (app_Rlist (subdivision_val f) Rabs);
1631
apply StepFun_P31; apply StepFun_P1.
1636
ordered_Rlist l1 -> Rabs (Int_SF l2 l1) <= Int_SF (app_Rlist l2 Rabs) l1.
1638
simple induction l2; intros.
1639
simpl in |- *; rewrite Rabs_R0; right; reflexivity.
1640
simpl in |- *; induction l1 as [| r1 l1 Hrecl1].
1641
rewrite Rabs_R0; right; reflexivity.
1642
induction l1 as [| r2 l1 Hrecl0].
1643
rewrite Rabs_R0; right; reflexivity.
1644
apply Rle_trans with (Rabs (r * (r2 - r1)) + Rabs (Int_SF r0 (cons r2 l1))).
1646
rewrite Rabs_mult; rewrite (Rabs_right (r2 - r1));
1647
[ apply Rplus_le_compat_l; apply H; apply RList_P4 with r1; assumption
1648
| apply Rge_minus; apply Rle_ge; apply (H0 0%nat); simpl in |- *;
1653
forall (a b:R) (f:StepFun a b),
1655
Rabs (RiemannInt_SF f) <= RiemannInt_SF (mkStepFun (StepFun_P32 f)).
1657
intros; unfold RiemannInt_SF in |- *; case (Rle_dec a b); intro.
1659
(Int_SF (subdivision_val (mkStepFun (StepFun_P32 f)))
1660
(subdivision (mkStepFun (StepFun_P32 f)))) with
1661
(Int_SF (app_Rlist (subdivision_val f) Rabs) (subdivision f)).
1662
apply StepFun_P33; assert (H0 := StepFun_P29 f); unfold is_subdivision in H0;
1663
elim H0; intros; unfold adapted_couple in p; decompose [and] p;
1665
apply StepFun_P17 with (fun x:R => Rabs (f x)) a b;
1666
[ apply StepFun_P31; apply StepFun_P1
1667
| apply (StepFun_P1 (mkStepFun (StepFun_P32 f))) ].
1672
forall (l:Rlist) (a b:R) (f g:R -> R),
1675
pos_Rl l (pred (Rlength l)) = b ->
1676
(forall x:R, a < x < b -> f x <= g x) ->
1677
Int_SF (FF l f) l <= Int_SF (FF l g) l.
1679
simple induction l; intros.
1681
simpl in |- *; induction r0 as [| r0 r1 Hrecr0].
1683
simpl in |- *; apply Rplus_le_compat.
1684
case (Req_dec r r0); intro.
1685
rewrite H4; right; ring.
1686
do 2 rewrite <- (Rmult_comm (r0 - r)); apply Rmult_le_compat_l.
1687
apply Rge_le; apply Rge_minus; apply Rle_ge; apply (H0 0%nat); simpl in |- *;
1690
apply Rmult_lt_reg_l with 2.
1692
unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
1693
rewrite <- Rinv_r_sym.
1694
assert (H5 : r = a).
1696
rewrite H5; rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l.
1697
assert (H6 := H0 0%nat (lt_O_Sn _)).
1700
rewrite H5 in H7; apply H7.
1701
elim H4; assumption.
1703
apply Rmult_lt_reg_l with 2.
1705
unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
1706
rewrite <- Rinv_r_sym.
1707
rewrite Rmult_1_l; rewrite double; assert (H5 : r0 <= b).
1709
(pos_Rl (cons r (cons r0 r1)) (pred (Rlength (cons r (cons r0 r1))))).
1710
replace r0 with (pos_Rl (cons r (cons r0 r1)) 1).
1711
elim (RList_P6 (cons r (cons r0 r1))); intros; apply H5.
1713
simpl in |- *; apply le_n_S.
1715
simpl in |- *; apply lt_n_Sn.
1717
apply Rle_lt_trans with (r + b).
1718
apply Rplus_le_compat_l; assumption.
1719
rewrite (Rplus_comm r); apply Rplus_lt_compat_l.
1720
apply Rlt_le_trans with r0.
1721
assert (H6 := H0 0%nat (lt_O_Sn _)).
1725
elim H4; assumption.
1728
simpl in H; apply H with r0 b.
1729
apply RList_P4 with r; assumption.
1731
rewrite <- H2; reflexivity.
1732
intros; apply H3; elim H4; intros; split; try assumption.
1733
apply Rle_lt_trans with r0; try assumption.
1735
simpl in |- *; apply (H0 0%nat); simpl in |- *; apply lt_O_Sn.
1739
forall (a b:R) (f g:StepFun a b) (l:Rlist),
1741
is_subdivision f a b l ->
1742
is_subdivision g a b l ->
1743
(forall x:R, a < x < b -> f x <= g x) ->
1744
RiemannInt_SF f <= RiemannInt_SF g.
1746
intros; unfold RiemannInt_SF in |- *; case (Rle_dec a b); intro.
1747
replace (Int_SF (subdivision_val f) (subdivision f)) with (Int_SF (FF l f) l).
1748
replace (Int_SF (subdivision_val g) (subdivision g)) with (Int_SF (FF l g) l).
1749
unfold is_subdivision in X; elim X; clear X; intros;
1750
unfold adapted_couple in p; decompose [and] p; clear p;
1751
assert (H5 : Rmin a b = a);
1752
[ unfold Rmin in |- *; case (Rle_dec a b); intro;
1753
[ reflexivity | elim n; assumption ]
1754
| assert (H7 : Rmax a b = b);
1755
[ unfold Rmax in |- *; case (Rle_dec a b); intro;
1756
[ reflexivity | elim n; assumption ]
1757
| rewrite H5 in H3; rewrite H7 in H2; eapply StepFun_P35 with a b;
1759
apply StepFun_P17 with (fe g) a b;
1760
[ apply StepFun_P21; assumption | apply StepFun_P1 ].
1761
apply StepFun_P17 with (fe f) a b;
1762
[ apply StepFun_P21; assumption | apply StepFun_P1 ].
1767
forall (a b:R) (f g:StepFun a b),
1769
(forall x:R, a < x < b -> f x <= g x) ->
1770
RiemannInt_SF f <= RiemannInt_SF g.
1772
intros; eapply StepFun_P36; try assumption.
1773
eapply StepFun_P25; apply StepFun_P29.
1774
eapply StepFun_P23; apply StepFun_P29.
1778
forall (l:Rlist) (a b:R) (f:R -> R),
1781
pos_Rl l (pred (Rlength l)) = b ->
1785
(i < pred (Rlength l))%nat ->
1786
constant_D_eq g (co_interval (pos_Rl l i) (pos_Rl l (S i)))
1787
(f (pos_Rl l i))) }.
1789
intros l a b f; generalize a; clear a; induction l.
1790
intros a H H0 H1; simpl in H0; simpl in H1;
1791
exists (mkStepFun (StepFun_P4 a b (f b))); split.
1793
intros; elim (lt_n_O _ H2).
1794
intros; destruct l as [| r1 l].
1795
simpl in H1; simpl in H0; exists (mkStepFun (StepFun_P4 a b (f b))); split.
1797
intros i H2; elim (lt_n_O _ H2).
1798
intros; assert (H2 : ordered_Rlist (cons r1 l)).
1799
apply RList_P4 with r; assumption.
1800
assert (H3 : pos_Rl (cons r1 l) 0 = r1).
1802
assert (H4 : pos_Rl (cons r1 l) (pred (Rlength (cons r1 l))) = b).
1803
rewrite <- H1; reflexivity.
1804
elim (IHl r1 H2 H3 H4); intros g [H5 H6].
1807
fun x:R => match Rle_dec r1 x with
1811
assert (H7 : r1 <= b).
1812
rewrite <- H4; apply RList_P7; [ assumption | left; reflexivity ].
1813
assert (H8 : IsStepFun g' a b).
1814
unfold IsStepFun in |- *; assert (H8 := pre g); unfold IsStepFun in H8;
1815
elim H8; intros lg H9; unfold is_subdivision in H9;
1816
elim H9; clear H9; intros lg2 H9; split with (cons a lg);
1817
unfold is_subdivision in |- *; split with (cons (f a) lg2);
1818
unfold adapted_couple in H9; decompose [and] H9; clear H9;
1819
unfold adapted_couple in |- *; repeat split.
1820
unfold ordered_Rlist in |- *; intros; simpl in H9;
1821
induction i as [| i Hreci].
1822
simpl in |- *; rewrite H12; replace (Rmin r1 b) with r1.
1823
simpl in H0; rewrite <- H0; apply (H 0%nat); simpl in |- *; apply lt_O_Sn.
1824
unfold Rmin in |- *; case (Rle_dec r1 b); intro;
1825
[ reflexivity | elim n; assumption ].
1826
apply (H10 i); apply lt_S_n.
1827
replace (S (pred (Rlength lg))) with (Rlength lg).
1829
apply S_pred with 0%nat; apply neq_O_lt; intro; rewrite <- H14 in H9;
1831
simpl in |- *; assert (H14 : a <= b).
1832
rewrite <- H1; simpl in H0; rewrite <- H0; apply RList_P7;
1833
[ assumption | left; reflexivity ].
1834
unfold Rmin in |- *; case (Rle_dec a b); intro;
1835
[ reflexivity | elim n; assumption ].
1836
assert (H14 : a <= b).
1837
rewrite <- H1; simpl in H0; rewrite <- H0; apply RList_P7;
1838
[ assumption | left; reflexivity ].
1839
replace (Rmax a b) with (Rmax r1 b).
1840
rewrite <- H11; induction lg as [| r0 lg Hreclg].
1841
simpl in H13; discriminate.
1843
unfold Rmax in |- *; case (Rle_dec a b); case (Rle_dec r1 b); intros;
1844
reflexivity || elim n; assumption.
1845
simpl in |- *; rewrite H13; reflexivity.
1846
intros; simpl in H9; induction i as [| i Hreci].
1847
unfold constant_D_eq, open_interval in |- *; simpl in |- *; intros;
1848
assert (H16 : Rmin r1 b = r1).
1849
unfold Rmin in |- *; case (Rle_dec r1 b); intro;
1850
[ reflexivity | elim n; assumption ].
1851
rewrite H16 in H12; rewrite H12 in H14; elim H14; clear H14; intros _ H14;
1852
unfold g' in |- *; case (Rle_dec r1 x); intro r3.
1853
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r3 H14)).
1856
(constant_D_eq g' (open_interval (pos_Rl lg i) (pos_Rl lg (S i)))
1857
(pos_Rl lg2 i)) in |- *; clear Hreci; assert (H16 := H15 i);
1858
assert (H17 : (i < pred (Rlength lg))%nat).
1860
replace (S (pred (Rlength lg))) with (Rlength lg).
1862
apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro;
1863
rewrite <- H14 in H9; elim (lt_n_O _ H9).
1864
assert (H18 := H16 H17); unfold constant_D_eq, open_interval in H18;
1865
unfold constant_D_eq, open_interval in |- *; intros;
1866
assert (H19 := H18 _ H14); rewrite <- H19; unfold g' in |- *;
1867
case (Rle_dec r1 x); intro.
1869
elim n; replace r1 with (Rmin r1 b).
1870
rewrite <- H12; elim H14; clear H14; intros H14 _; left;
1871
apply Rle_lt_trans with (pos_Rl lg i); try assumption.
1874
elim (RList_P3 lg (pos_Rl lg i)); intros; apply H21; exists i; split.
1876
apply lt_trans with (pred (Rlength lg)); try assumption.
1877
apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H22 in H17;
1878
elim (lt_n_O _ H17).
1879
unfold Rmin in |- *; case (Rle_dec r1 b); intro;
1880
[ reflexivity | elim n0; assumption ].
1881
exists (mkStepFun H8); split.
1882
simpl in |- *; unfold g' in |- *; case (Rle_dec r1 b); intro.
1885
intros; simpl in H9; induction i as [| i Hreci].
1886
unfold constant_D_eq, co_interval in |- *; simpl in |- *; intros; simpl in H0;
1887
rewrite H0; elim H10; clear H10; intros; unfold g' in |- *;
1888
case (Rle_dec r1 x); intro r3.
1889
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r3 H11)).
1893
(constant_D_eq (mkStepFun H8)
1894
(co_interval (pos_Rl (cons r1 l) i) (pos_Rl (cons r1 l) (S i)))
1895
(f (pos_Rl (cons r1 l) i))) in |- *; assert (H10 := H6 i);
1896
assert (H11 : (i < pred (Rlength (cons r1 l)))%nat).
1897
simpl in |- *; apply lt_S_n; assumption.
1898
assert (H12 := H10 H11); unfold constant_D_eq, co_interval in H12;
1899
unfold constant_D_eq, co_interval in |- *; intros;
1900
rewrite <- (H12 _ H13); simpl in |- *; unfold g' in |- *;
1901
case (Rle_dec r1 x); intro.
1903
elim n; elim H13; clear H13; intros;
1904
apply Rle_trans with (pos_Rl (cons r1 l) i); try assumption;
1905
change (pos_Rl (cons r1 l) 0 <= pos_Rl (cons r1 l) i) in |- *;
1906
elim (RList_P6 (cons r1 l)); intros; apply H15;
1909
| simpl in |- *; apply lt_trans with (Rlength l);
1910
[ apply lt_S_n; assumption | apply lt_n_Sn ] ].
1914
forall (a b:R) (f:StepFun a b),
1915
RiemannInt_SF f = - RiemannInt_SF (mkStepFun (StepFun_P6 (pre f))).
1917
intros; unfold RiemannInt_SF in |- *; case (Rle_dec a b); case (Rle_dec b a);
1919
assert (H : adapted_couple f a b (subdivision f) (subdivision_val f));
1923
adapted_couple (mkStepFun (StepFun_P6 (pre f))) b a
1924
(subdivision (mkStepFun (StepFun_P6 (pre f))))
1925
(subdivision_val (mkStepFun (StepFun_P6 (pre f)))));
1927
| assert (H1 : a = b);
1928
[ apply Rle_antisym; assumption
1929
| rewrite (StepFun_P8 H H1); assert (H2 : b = a);
1930
[ symmetry in |- *; apply H1 | rewrite (StepFun_P8 H0 H2); ring ] ] ] ].
1931
rewrite Ropp_involutive; eapply StepFun_P17;
1933
| apply StepFun_P2; set (H := StepFun_P6 (pre f)); unfold IsStepFun in H;
1934
elim H; intros; unfold is_subdivision in |- *;
1935
elim p; intros; apply p0 ].
1936
apply Ropp_eq_compat; eapply StepFun_P17;
1938
| apply StepFun_P2; set (H := StepFun_P6 (pre f)); unfold IsStepFun in H;
1939
elim H; intros; unfold is_subdivision in |- *;
1940
elim p; intros; apply p0 ].
1943
| assert (H0 : b < a);
1944
[ auto with real | elim (Rlt_irrefl _ (Rlt_trans _ _ _ H H0)) ] ].
1948
forall (f:R -> R) (a b c:R) (l1 l2 lf1 lf2:Rlist),
1951
adapted_couple f a b l1 lf1 ->
1952
adapted_couple f b c l2 lf2 ->
1953
adapted_couple f a c (cons_Rlist l1 l2) (FF (cons_Rlist l1 l2) f).
1955
intros f a b c l1 l2 lf1 lf2 H H0 H1 H2; unfold adapted_couple in H1, H2;
1956
unfold adapted_couple in |- *; decompose [and] H1;
1957
decompose [and] H2; clear H1 H2; repeat split.
1958
apply RList_P25; try assumption.
1959
rewrite H10; rewrite H4; unfold Rmin, Rmax in |- *; case (Rle_dec a b);
1960
case (Rle_dec b c); intros;
1961
(right; reflexivity) || (elim n; left; assumption).
1963
rewrite H5; unfold Rmin, Rmax in |- *; case (Rle_dec a b); case (Rle_dec a c);
1966
| elim n; apply Rle_trans with b; left; assumption
1967
| elim n; left; assumption
1968
| elim n0; left; assumption ].
1969
red in |- *; intro; rewrite H1 in H6; discriminate.
1971
rewrite H9; unfold Rmin, Rmax in |- *; case (Rle_dec b c); case (Rle_dec a c);
1974
| elim n; apply Rle_trans with b; left; assumption
1975
| elim n; left; assumption
1976
| elim n0; left; assumption ].
1977
red in |- *; intro; rewrite H1 in H11; discriminate.
1979
rewrite RList_P23; apply neq_O_lt; red in |- *; intro.
1980
assert (H2 : (Rlength l1 + Rlength l2)%nat = 0%nat).
1981
symmetry in |- *; apply H1.
1982
elim (plus_is_O _ _ H2); intros; rewrite H12 in H6; discriminate.
1983
unfold constant_D_eq, open_interval in |- *; intros;
1984
elim (le_or_lt (S (S i)) (Rlength l1)); intro.
1985
assert (H14 : pos_Rl (cons_Rlist l1 l2) i = pos_Rl l1 i).
1986
apply RList_P26; apply lt_S_n; apply le_lt_n_Sm; apply le_S_n;
1987
apply le_trans with (Rlength l1); [ assumption | apply le_n_Sn ].
1988
assert (H15 : pos_Rl (cons_Rlist l1 l2) (S i) = pos_Rl l1 (S i)).
1989
apply RList_P26; apply lt_S_n; apply le_lt_n_Sm; assumption.
1990
rewrite H14 in H2; rewrite H15 in H2; assert (H16 : (2 <= Rlength l1)%nat).
1991
apply le_trans with (S (S i));
1992
[ repeat apply le_n_S; apply le_O_n | assumption ].
1993
elim (RList_P20 _ H16); intros r1 [r2 [r3 H17]]; rewrite H17;
1995
(f x = pos_Rl (app_Rlist (mid_Rlist (cons_Rlist (cons r2 r3) l2) r1) f) i)
1996
in |- *; rewrite RList_P12.
1997
induction i as [| i Hreci].
1998
simpl in |- *; assert (H18 := H8 0%nat);
1999
unfold constant_D_eq, open_interval in H18;
2000
assert (H19 : (0 < pred (Rlength l1))%nat).
2001
rewrite H17; simpl in |- *; apply lt_O_Sn.
2002
assert (H20 := H18 H19); repeat rewrite H20.
2004
assert (H21 : r1 <= r2).
2005
rewrite H17 in H3; apply (H3 0%nat).
2006
simpl in |- *; apply lt_O_Sn.
2009
rewrite H17; simpl in |- *; apply Rmult_lt_reg_l with 2;
2011
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
2012
rewrite <- Rinv_r_sym;
2013
[ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption
2015
rewrite H17; simpl in |- *; apply Rmult_lt_reg_l with 2;
2017
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
2018
rewrite <- Rinv_r_sym;
2019
[ rewrite Rmult_1_l; rewrite (Rplus_comm r1); rewrite double;
2020
apply Rplus_lt_compat_l; assumption
2022
elim H2; intros; rewrite H17 in H23; rewrite H17 in H24; simpl in H24;
2023
simpl in H23; rewrite H22 in H23;
2024
elim (Rlt_irrefl _ (Rlt_trans _ _ _ H23 H24)).
2026
clear Hreci; rewrite RList_P13.
2027
rewrite H17 in H14; rewrite H17 in H15;
2029
(pos_Rl (cons_Rlist (cons r2 r3) l2) i =
2030
pos_Rl (cons r1 (cons r2 r3)) (S i)) in H14; rewrite H14;
2032
(pos_Rl (cons_Rlist (cons r2 r3) l2) (S i) =
2033
pos_Rl (cons r1 (cons r2 r3)) (S (S i))) in H15;
2034
rewrite H15; assert (H18 := H8 (S i));
2035
unfold constant_D_eq, open_interval in H18;
2036
assert (H19 : (S i < pred (Rlength l1))%nat).
2037
apply lt_pred; apply lt_S_n; apply le_lt_n_Sm; assumption.
2038
assert (H20 := H18 H19); repeat rewrite H20.
2040
rewrite <- H17; assert (H21 : pos_Rl l1 (S i) <= pos_Rl l1 (S (S i))).
2041
apply (H3 (S i)); apply lt_pred; apply lt_S_n; apply le_lt_n_Sm; assumption.
2044
apply Rmult_lt_reg_l with 2;
2046
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
2047
rewrite <- Rinv_r_sym;
2048
[ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption
2050
apply Rmult_lt_reg_l with 2;
2052
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
2053
rewrite <- Rinv_r_sym;
2054
[ rewrite Rmult_1_l; rewrite (Rplus_comm (pos_Rl l1 (S i)));
2055
rewrite double; apply Rplus_lt_compat_l; assumption
2057
elim H2; intros; rewrite H22 in H23;
2058
elim (Rlt_irrefl _ (Rlt_trans _ _ _ H23 H24)).
2060
simpl in |- *; rewrite H17 in H1; simpl in H1; apply lt_S_n; assumption.
2061
rewrite RList_P14; rewrite H17 in H1; simpl in H1; apply H1.
2063
assert (H16 : pos_Rl (cons_Rlist l1 l2) (S i) = b).
2065
rewrite H15; rewrite <- minus_n_n; rewrite H10; unfold Rmin in |- *;
2066
case (Rle_dec b c); intro; [ reflexivity | elim n; left; assumption ].
2067
rewrite H15; apply le_n.
2068
induction l1 as [| r l1 Hrecl1].
2069
simpl in H15; discriminate.
2070
clear Hrecl1; simpl in H1; simpl in |- *; apply lt_n_S; assumption.
2071
assert (H17 : pos_Rl (cons_Rlist l1 l2) i = b).
2073
replace i with (pred (Rlength l1));
2074
[ rewrite H4; unfold Rmax in |- *; case (Rle_dec a b); intro;
2075
[ reflexivity | elim n; left; assumption ]
2076
| rewrite H15; reflexivity ].
2077
rewrite H15; apply lt_n_Sn.
2078
rewrite H16 in H2; rewrite H17 in H2; elim H2; intros;
2079
elim (Rlt_irrefl _ (Rlt_trans _ _ _ H14 H18)).
2080
assert (H16 : pos_Rl (cons_Rlist l1 l2) i = pos_Rl l2 (i - Rlength l1)).
2082
apply le_S_n; assumption.
2083
apply lt_le_trans with (pred (Rlength (cons_Rlist l1 l2)));
2084
[ assumption | apply le_pred_n ].
2086
(H17 : pos_Rl (cons_Rlist l1 l2) (S i) = pos_Rl l2 (S (i - Rlength l1))).
2087
replace (S (i - Rlength l1)) with (S i - Rlength l1)%nat.
2089
apply le_S_n; apply le_trans with (S i); [ assumption | apply le_n_Sn ].
2090
induction l1 as [| r l1 Hrecl1].
2091
simpl in H6; discriminate.
2092
clear Hrecl1; simpl in H1; simpl in |- *; apply lt_n_S; assumption.
2093
symmetry in |- *; apply minus_Sn_m; apply le_S_n; assumption.
2094
assert (H18 : (2 <= Rlength l1)%nat).
2095
clear f c l2 lf2 H0 H3 H8 H7 H10 H9 H11 H13 i H1 x H2 H12 m H14 H15 H16 H17;
2096
induction l1 as [| r l1 Hrecl1].
2098
clear Hrecl1; induction l1 as [| r0 l1 Hrecl1].
2099
simpl in H5; simpl in H4; assert (H0 : Rmin a b < Rmax a b).
2100
unfold Rmin, Rmax in |- *; case (Rle_dec a b); intro;
2101
[ assumption | elim n; left; assumption ].
2102
rewrite <- H5 in H0; rewrite <- H4 in H0; elim (Rlt_irrefl _ H0).
2103
clear Hrecl1; simpl in |- *; repeat apply le_n_S; apply le_O_n.
2104
elim (RList_P20 _ H18); intros r1 [r2 [r3 H19]]; rewrite H19;
2106
(f x = pos_Rl (app_Rlist (mid_Rlist (cons_Rlist (cons r2 r3) l2) r1) f) i)
2107
in |- *; rewrite RList_P12.
2108
induction i as [| i Hreci].
2109
assert (H20 := le_S_n _ _ H15); assert (H21 := le_trans _ _ _ H18 H20);
2110
elim (le_Sn_O _ H21).
2111
clear Hreci; rewrite RList_P13.
2112
rewrite H19 in H16; rewrite H19 in H17;
2114
(pos_Rl (cons_Rlist (cons r2 r3) l2) i =
2115
pos_Rl l2 (S i - Rlength (cons r1 (cons r2 r3))))
2116
in H16; rewrite H16;
2118
(pos_Rl (cons_Rlist (cons r2 r3) l2) (S i) =
2119
pos_Rl l2 (S (S i - Rlength (cons r1 (cons r2 r3)))))
2120
in H17; rewrite H17; assert (H20 := H13 (S i - Rlength l1)%nat);
2121
unfold constant_D_eq, open_interval in H20;
2122
assert (H21 : (S i - Rlength l1 < pred (Rlength l2))%nat).
2123
apply lt_pred; rewrite minus_Sn_m.
2124
apply plus_lt_reg_l with (Rlength l1); rewrite <- le_plus_minus.
2125
rewrite H19 in H1; simpl in H1; rewrite H19; simpl in |- *;
2126
rewrite RList_P23 in H1; apply lt_n_S; assumption.
2127
apply le_trans with (S i); [ apply le_S_n; assumption | apply le_n_Sn ].
2128
apply le_S_n; assumption.
2129
assert (H22 := H20 H21); repeat rewrite H22.
2133
(H23 : pos_Rl l2 (S i - Rlength l1) <= pos_Rl l2 (S (S i - Rlength l1))).
2134
apply H7; apply lt_pred.
2136
apply plus_lt_reg_l with (Rlength l1); rewrite <- le_plus_minus.
2137
rewrite H19 in H1; simpl in H1; rewrite H19; simpl in |- *;
2138
rewrite RList_P23 in H1; apply lt_n_S; assumption.
2139
apply le_trans with (S i); [ apply le_S_n; assumption | apply le_n_Sn ].
2140
apply le_S_n; assumption.
2143
apply Rmult_lt_reg_l with 2;
2145
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
2146
rewrite <- Rinv_r_sym;
2147
[ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption
2149
apply Rmult_lt_reg_l with 2;
2151
| unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
2152
rewrite <- Rinv_r_sym;
2153
[ rewrite Rmult_1_l; rewrite (Rplus_comm (pos_Rl l2 (S i - Rlength l1)));
2154
rewrite double; apply Rplus_lt_compat_l; assumption
2156
rewrite <- H19 in H16; rewrite <- H19 in H17; elim H2; intros;
2157
rewrite H19 in H25; rewrite H19 in H26; simpl in H25;
2158
simpl in H16; rewrite H16 in H25; simpl in H26; simpl in H17;
2159
rewrite H17 in H26; simpl in H24; rewrite H24 in H25;
2160
elim (Rlt_irrefl _ (Rlt_trans _ _ _ H25 H26)).
2161
assert (H23 : pos_Rl (cons_Rlist l1 l2) (S i) = pos_Rl l2 (S i - Rlength l1)).
2162
rewrite H19; simpl in |- *; simpl in H16; apply H16.
2165
pos_Rl (cons_Rlist l1 l2) (S (S i)) = pos_Rl l2 (S (S i - Rlength l1))).
2166
rewrite H19; simpl in |- *; simpl in H17; apply H17.
2167
rewrite <- H23; rewrite <- H24; assumption.
2168
simpl in |- *; rewrite H19 in H1; simpl in H1; apply lt_S_n; assumption.
2169
rewrite RList_P14; rewrite H19 in H1; simpl in H1; simpl in |- *; apply H1.
2173
forall (f:R -> R) (a b c:R),
2174
a <= b -> b <= c -> IsStepFun f a b -> IsStepFun f b c -> IsStepFun f a c.
2176
intros f a b c H H0 (l1,(lf1,H1)) (l2,(lf2,H2));
2177
destruct (total_order_T a b) as [[Hltab|Hab]|Hgtab].
2178
destruct (total_order_T b c) as [[Hltbc|Hbc]|Hgtbc].
2179
exists (cons_Rlist l1 l2); exists (FF (cons_Rlist l1 l2) f);
2180
apply StepFun_P40 with b lf1 lf2; assumption.
2181
exists l1; exists lf1; rewrite Hbc in H1; assumption.
2182
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 Hgtbc)).
2183
exists l2; exists lf2; rewrite <- Hab in H2; assumption.
2184
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgtab)).
2188
forall (l1 l2:Rlist) (f:R -> R),
2189
pos_Rl l1 (pred (Rlength l1)) = pos_Rl l2 0 ->
2190
Int_SF (FF (cons_Rlist l1 l2) f) (cons_Rlist l1 l2) =
2191
Int_SF (FF l1 f) l1 + Int_SF (FF l2 f) l2.
2193
intros l1 l2 f; induction l1 as [| r l1 IHl1]; intros H;
2194
[ simpl in |- *; ring
2195
| destruct l1 as [| r0 r1];
2196
[ simpl in H; simpl in |- *; destruct l2 as [| r0 r1];
2197
[ simpl in |- *; ring | simpl in |- *; simpl in H; rewrite H; ring ]
2198
| simpl in |- *; rewrite Rplus_assoc; apply Rplus_eq_compat_l; apply IHl1;
2199
rewrite <- H; reflexivity ] ].
2203
forall (f:R -> R) (a b c:R) (pr1:IsStepFun f a b)
2204
(pr2:IsStepFun f b c) (pr3:IsStepFun f a c),
2205
RiemannInt_SF (mkStepFun pr1) + RiemannInt_SF (mkStepFun pr2) =
2206
RiemannInt_SF (mkStepFun pr3).
2209
pose proof pr1 as (l1,(lf1,H1)).
2210
pose proof pr2 as (l2,(lf2,H2)).
2211
pose proof pr3 as (l3,(lf3,H3)).
2212
replace (RiemannInt_SF (mkStepFun pr1)) with
2213
match Rle_dec a b with
2214
| left _ => Int_SF lf1 l1
2215
| right _ => - Int_SF lf1 l1
2217
replace (RiemannInt_SF (mkStepFun pr2)) with
2218
match Rle_dec b c with
2219
| left _ => Int_SF lf2 l2
2220
| right _ => - Int_SF lf2 l2
2222
replace (RiemannInt_SF (mkStepFun pr3)) with
2223
match Rle_dec a c with
2224
| left _ => Int_SF lf3 l3
2225
| right _ => - Int_SF lf3 l3
2227
case (Rle_dec a b); case (Rle_dec b c); case (Rle_dec a c); intros.
2230
replace (Int_SF lf3 l3) with
2231
(Int_SF (FF (cons_Rlist l1 l2) f) (cons_Rlist l1 l2)).
2232
replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1).
2233
replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2).
2234
symmetry in |- *; apply StepFun_P42.
2235
unfold adapted_couple in H1, H2; decompose [and] H1; decompose [and] H2;
2236
clear H1 H2; rewrite H11; rewrite H5; unfold Rmax, Rmin in |- *;
2237
case (Rle_dec a b); case (Rle_dec b c); intros; reflexivity || elim n;
2240
[ apply StepFun_P21; unfold is_subdivision in |- *; split with lf2; apply H2;
2244
[ apply StepFun_P21; unfold is_subdivision in |- *; split with lf1; apply H1
2246
eapply StepFun_P17; [ apply (StepFun_P40 H H0 H1 H2) | apply H3 ].
2247
replace (Int_SF lf2 l2) with 0.
2248
rewrite Rplus_0_r; eapply StepFun_P17;
2249
[ apply H1 | rewrite <- H0 in H3; apply H3 ].
2250
symmetry in |- *; eapply StepFun_P8; [ apply H2 | assumption ].
2251
replace (Int_SF lf1 l1) with 0.
2252
rewrite Rplus_0_l; eapply StepFun_P17;
2253
[ apply H2 | rewrite H in H3; apply H3 ].
2254
symmetry in |- *; eapply StepFun_P8; [ apply H1 | assumption ].
2255
elim n; apply Rle_trans with b; assumption.
2256
apply Rplus_eq_reg_l with (Int_SF lf2 l2);
2257
replace (Int_SF lf2 l2 + (Int_SF lf1 l1 + - Int_SF lf2 l2)) with
2258
(Int_SF lf1 l1); [ idtac | ring ].
2263
replace (Int_SF lf1 l1) with
2264
(Int_SF (FF (cons_Rlist l3 l2) f) (cons_Rlist l3 l2)).
2265
replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3).
2266
replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2).
2268
unfold adapted_couple in H2, H3; decompose [and] H2; decompose [and] H3;
2269
clear H3 H2; rewrite H10; rewrite H6; unfold Rmax, Rmin in |- *;
2270
case (Rle_dec a c); case (Rle_dec b c); intros;
2271
[ elim n; assumption
2273
| elim n0; assumption
2274
| elim n1; assumption ].
2276
[ apply StepFun_P21; unfold is_subdivision in |- *; split with lf2; apply H2
2279
[ apply StepFun_P21; unfold is_subdivision in |- *; split with lf3; apply H3
2282
[ apply (StepFun_P40 H0 H H3 (StepFun_P2 H2)) | apply H1 ].
2283
replace (Int_SF lf3 l3) with 0.
2284
rewrite Rplus_0_r; eapply StepFun_P17;
2285
[ apply H1 | apply StepFun_P2; rewrite <- H0 in H2; apply H2 ].
2286
symmetry in |- *; eapply StepFun_P8; [ apply H3 | assumption ].
2287
replace (Int_SF lf2 l2) with (Int_SF lf3 l3 + Int_SF lf1 l1).
2290
replace (Int_SF lf2 l2) with
2291
(Int_SF (FF (cons_Rlist l3 l1) f) (cons_Rlist l3 l1)).
2292
replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3).
2293
replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1).
2294
symmetry in |- *; apply StepFun_P42.
2295
unfold adapted_couple in H1, H3; decompose [and] H1; decompose [and] H3;
2296
clear H3 H1; rewrite H9; rewrite H5; unfold Rmax, Rmin in |- *;
2297
case (Rle_dec a c); case (Rle_dec a b); intros;
2298
[ elim n; assumption
2299
| elim n1; assumption
2301
| elim n1; assumption ].
2303
[ apply StepFun_P21; unfold is_subdivision in |- *; split with lf1; apply H1
2306
[ apply StepFun_P21; unfold is_subdivision in |- *; split with lf3; apply H3
2309
assert (H0 : c < a).
2311
apply (StepFun_P40 H0 H (StepFun_P2 H3) H1).
2312
apply StepFun_P2; apply H2.
2313
replace (Int_SF lf1 l1) with 0.
2314
rewrite Rplus_0_r; eapply StepFun_P17;
2315
[ apply H3 | rewrite <- H in H2; apply H2 ].
2316
symmetry in |- *; eapply StepFun_P8; [ apply H1 | assumption ].
2319
replace (Int_SF lf2 l2) with (Int_SF lf3 l3 + Int_SF lf1 l1).
2321
rewrite Rplus_comm; elim r; intro.
2322
replace (Int_SF lf2 l2) with
2323
(Int_SF (FF (cons_Rlist l1 l3) f) (cons_Rlist l1 l3)).
2324
replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3).
2325
replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1).
2326
symmetry in |- *; apply StepFun_P42.
2327
unfold adapted_couple in H1, H3; decompose [and] H1; decompose [and] H3;
2328
clear H3 H1; rewrite H11; rewrite H5; unfold Rmax, Rmin in |- *;
2329
case (Rle_dec a c); case (Rle_dec a b); intros;
2330
[ elim n; assumption
2332
| elim n0; assumption
2333
| elim n1; assumption ].
2335
[ apply StepFun_P21; unfold is_subdivision in |- *; split with lf1; apply H1
2338
[ apply StepFun_P21; unfold is_subdivision in |- *; split with lf3; apply H3
2341
apply (StepFun_P40 H H0 (StepFun_P2 H1) H3).
2343
replace (Int_SF lf3 l3) with 0.
2344
rewrite Rplus_0_r; eapply StepFun_P17;
2345
[ apply H1 | rewrite <- H0 in H2; apply StepFun_P2; apply H2 ].
2346
symmetry in |- *; eapply StepFun_P8; [ apply H3 | assumption ].
2349
replace (Int_SF lf1 l1) with (Int_SF lf2 l2 + Int_SF lf3 l3).
2352
replace (Int_SF lf1 l1) with
2353
(Int_SF (FF (cons_Rlist l2 l3) f) (cons_Rlist l2 l3)).
2354
replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3).
2355
replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2).
2356
symmetry in |- *; apply StepFun_P42.
2357
unfold adapted_couple in H2, H3; decompose [and] H2; decompose [and] H3;
2358
clear H3 H2; rewrite H11; rewrite H5; unfold Rmax, Rmin in |- *;
2359
case (Rle_dec a c); case (Rle_dec b c); intros;
2360
[ elim n; assumption
2361
| elim n1; assumption
2363
| elim n1; assumption ].
2365
[ apply StepFun_P21; unfold is_subdivision in |- *; split with lf2; apply H2
2368
[ apply StepFun_P21; unfold is_subdivision in |- *; split with lf3; apply H3
2371
apply (StepFun_P40 H0 H H2 (StepFun_P2 H3)).
2372
apply StepFun_P2; apply H1.
2373
replace (Int_SF lf2 l2) with 0.
2374
rewrite Rplus_0_l; eapply StepFun_P17;
2375
[ apply H3 | rewrite H0 in H1; apply H1 ].
2376
symmetry in |- *; eapply StepFun_P8; [ apply H2 | assumption ].
2377
elim n; apply Rle_trans with a; try assumption.
2381
assert (H0 : b < a).
2383
replace (Int_SF lf3 l3) with (Int_SF lf2 l2 + Int_SF lf1 l1).
2385
replace (Int_SF lf3 l3) with
2386
(Int_SF (FF (cons_Rlist l2 l1) f) (cons_Rlist l2 l1)).
2387
replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1).
2388
replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2).
2389
symmetry in |- *; apply StepFun_P42.
2390
unfold adapted_couple in H2, H1; decompose [and] H2; decompose [and] H1;
2391
clear H1 H2; rewrite H11; rewrite H5; unfold Rmax, Rmin in |- *;
2392
case (Rle_dec a b); case (Rle_dec b c); intros;
2393
[ elim n1; assumption
2394
| elim n1; assumption
2395
| elim n0; assumption
2398
[ apply StepFun_P21; unfold is_subdivision in |- *; split with lf2; apply H2
2401
[ apply StepFun_P21; unfold is_subdivision in |- *; split with lf1; apply H1
2404
apply (StepFun_P40 H H0 (StepFun_P2 H2) (StepFun_P2 H1)).
2405
apply StepFun_P2; apply H3.
2406
unfold RiemannInt_SF in |- *; case (Rle_dec a c); intro.
2410
(adapted_couple (mkStepFun pr3) a c (subdivision (mkStepFun pr3))
2411
(subdivision_val (mkStepFun pr3))) in |- *; apply StepFun_P1.
2412
apply Ropp_eq_compat; eapply StepFun_P17.
2415
(adapted_couple (mkStepFun pr3) a c (subdivision (mkStepFun pr3))
2416
(subdivision_val (mkStepFun pr3))) in |- *; apply StepFun_P1.
2417
unfold RiemannInt_SF in |- *; case (Rle_dec b c); intro.
2421
(adapted_couple (mkStepFun pr2) b c (subdivision (mkStepFun pr2))
2422
(subdivision_val (mkStepFun pr2))) in |- *; apply StepFun_P1.
2423
apply Ropp_eq_compat; eapply StepFun_P17.
2426
(adapted_couple (mkStepFun pr2) b c (subdivision (mkStepFun pr2))
2427
(subdivision_val (mkStepFun pr2))) in |- *; apply StepFun_P1.
2428
unfold RiemannInt_SF in |- *; case (Rle_dec a b); intro.
2432
(adapted_couple (mkStepFun pr1) a b (subdivision (mkStepFun pr1))
2433
(subdivision_val (mkStepFun pr1))) in |- *; apply StepFun_P1.
2434
apply Ropp_eq_compat; eapply StepFun_P17.
2437
(adapted_couple (mkStepFun pr1) a b (subdivision (mkStepFun pr1))
2438
(subdivision_val (mkStepFun pr1))) in |- *; apply StepFun_P1.
2442
forall (f:R -> R) (a b c:R),
2443
IsStepFun f a b -> a <= c <= b -> IsStepFun f a c.
2445
intros f; intros; assert (H0 : a <= b).
2446
elim H; intros; apply Rle_trans with c; assumption.
2447
elim H; clear H; intros; unfold IsStepFun in X; unfold is_subdivision in X;
2448
elim X; clear X; intros l1 [lf1 H2];
2450
(forall (l1 lf1:Rlist) (a b c:R) (f:R -> R),
2451
adapted_couple f a b l1 lf1 ->
2453
{ l:Rlist & { l0:Rlist & adapted_couple f a c l l0 } }).
2454
intro X; unfold IsStepFun in |- *; unfold is_subdivision in |- *; eapply X.
2457
clear f a b c H0 H H1 H2 l1 lf1; simple induction l1.
2458
intros; unfold adapted_couple in H; decompose [and] H; clear H; simpl in H4;
2460
simple induction r0.
2461
intros X lf1 a b c f H H0; assert (H1 : a = b).
2462
unfold adapted_couple in H; decompose [and] H; clear H; simpl in H3;
2463
simpl in H2; assert (H7 : a <= b).
2464
elim H0; intros; apply Rle_trans with c; assumption.
2465
replace a with (Rmin a b).
2466
pattern b at 2 in |- *; replace b with (Rmax a b).
2467
rewrite <- H2; rewrite H3; reflexivity.
2468
unfold Rmax in |- *; case (Rle_dec a b); intro;
2469
[ reflexivity | elim n; assumption ].
2470
unfold Rmin in |- *; case (Rle_dec a b); intro;
2471
[ reflexivity | elim n; assumption ].
2472
split with (cons r nil); split with lf1; assert (H2 : c = b).
2473
rewrite H1 in H0; elim H0; intros; apply Rle_antisym; assumption.
2474
rewrite H2; assumption.
2475
intros r1 r2 _ X0 lf1 a b c f H H0; induction lf1 as [| r3 lf1 Hreclf1].
2476
unfold adapted_couple in H; decompose [and] H; clear H; simpl in H4;
2478
clear Hreclf1; assert (H1 : {c <= r1} + {r1 < c}).
2479
case (Rle_dec c r1); intro; [ left; assumption | right; auto with real ].
2481
split with (cons r (cons c nil)); split with (cons r3 nil);
2482
unfold adapted_couple in H; decompose [and] H; clear H;
2483
assert (H6 : r = a).
2484
simpl in H4; rewrite H4; unfold Rmin in |- *; case (Rle_dec a b); intro;
2486
| elim n; elim H0; intros; apply Rle_trans with c; assumption ].
2487
elim H0; clear H0; intros; unfold adapted_couple in |- *; repeat split.
2488
rewrite H6; unfold ordered_Rlist in |- *; intros; simpl in H8; inversion H8;
2489
[ simpl in |- *; assumption | elim (le_Sn_O _ H10) ].
2490
simpl in |- *; unfold Rmin in |- *; case (Rle_dec a c); intro;
2491
[ assumption | elim n; assumption ].
2492
simpl in |- *; unfold Rmax in |- *; case (Rle_dec a c); intro;
2493
[ reflexivity | elim n; assumption ].
2494
unfold constant_D_eq, open_interval in |- *; intros; simpl in H8;
2496
simpl in |- *; assert (H10 := H7 0%nat);
2497
assert (H12 : (0 < pred (Rlength (cons r (cons r1 r2))))%nat).
2498
simpl in |- *; apply lt_O_Sn.
2499
apply (H10 H12); unfold open_interval in |- *; simpl in |- *;
2500
rewrite H11 in H9; simpl in H9; elim H9; clear H9;
2501
intros; split; try assumption.
2502
apply Rlt_le_trans with c; assumption.
2503
elim (le_Sn_O _ H11).
2504
cut (adapted_couple f r1 b (cons r1 r2) lf1).
2507
elim (X0 _ _ _ _ _ H3 H2); intros l1' [lf1' H4]; split with (cons r l1');
2508
split with (cons r3 lf1'); unfold adapted_couple in H, H4;
2509
decompose [and] H; decompose [and] H4; clear H H4 X0;
2510
assert (H14 : a <= b).
2511
elim H0; intros; apply Rle_trans with c; assumption.
2512
assert (H16 : r = a).
2513
simpl in H7; rewrite H7; unfold Rmin in |- *; case (Rle_dec a b); intro;
2514
[ reflexivity | elim n; assumption ].
2515
induction l1' as [| r4 l1' Hrecl1'].
2516
simpl in H13; discriminate.
2517
clear Hrecl1'; unfold adapted_couple in |- *; repeat split.
2518
unfold ordered_Rlist in |- *; intros; simpl in H; induction i as [| i Hreci].
2519
simpl in |- *; replace r4 with r1.
2521
simpl in |- *; apply lt_O_Sn.
2522
simpl in H12; rewrite H12; unfold Rmin in |- *; case (Rle_dec r1 c); intro;
2523
[ reflexivity | elim n; left; assumption ].
2524
apply (H9 i); simpl in |- *; apply lt_S_n; assumption.
2525
simpl in |- *; unfold Rmin in |- *; case (Rle_dec a c); intro;
2526
[ assumption | elim n; elim H0; intros; assumption ].
2527
replace (Rmax a c) with (Rmax r1 c).
2528
rewrite <- H11; reflexivity.
2529
unfold Rmax in |- *; case (Rle_dec r1 c); case (Rle_dec a c); intros;
2531
| elim n; elim H0; intros; assumption
2532
| elim n; left; assumption
2533
| elim n0; left; assumption ].
2534
simpl in |- *; simpl in H13; rewrite H13; reflexivity.
2535
intros; simpl in H; unfold constant_D_eq, open_interval in |- *; intros;
2536
induction i as [| i Hreci].
2537
simpl in |- *; assert (H17 := H10 0%nat);
2538
assert (H18 : (0 < pred (Rlength (cons r (cons r1 r2))))%nat).
2539
simpl in |- *; apply lt_O_Sn.
2540
apply (H17 H18); unfold open_interval in |- *; simpl in |- *; simpl in H4;
2541
elim H4; clear H4; intros; split; try assumption;
2544
simpl in H12; rewrite H12; unfold Rmin in |- *; case (Rle_dec r1 c); intro;
2545
[ reflexivity | elim n; left; assumption ].
2546
clear Hreci; simpl in |- *; apply H15.
2547
simpl in |- *; apply lt_S_n; assumption.
2548
unfold open_interval in |- *; apply H4.
2551
elim H0; intros; assumption.
2553
[ elim H0; intros; apply Rle_trans with c; [ apply H2 | apply H3 ]
2558
forall (f:R -> R) (a b c:R),
2559
IsStepFun f a b -> a <= c <= b -> IsStepFun f c b.
2561
intros f; intros; assert (H0 : a <= b).
2562
elim H; intros; apply Rle_trans with c; assumption.
2563
elim H; clear H; intros; unfold IsStepFun in X; unfold is_subdivision in X;
2564
elim X; clear X; intros l1 [lf1 H2];
2566
(forall (l1 lf1:Rlist) (a b c:R) (f:R -> R),
2567
adapted_couple f a b l1 lf1 ->
2569
{ l:Rlist & { l0:Rlist & adapted_couple f c b l l0 } }).
2570
intro X; unfold IsStepFun in |- *; unfold is_subdivision in |- *; eapply X;
2571
[ apply H2 | split; assumption ].
2572
clear f a b c H0 H H1 H2 l1 lf1; simple induction l1.
2573
intros; unfold adapted_couple in H; decompose [and] H; clear H; simpl in H4;
2575
simple induction r0.
2576
intros X lf1 a b c f H H0; assert (H1 : a = b).
2577
unfold adapted_couple in H; decompose [and] H; clear H; simpl in H3;
2578
simpl in H2; assert (H7 : a <= b).
2579
elim H0; intros; apply Rle_trans with c; assumption.
2580
replace a with (Rmin a b).
2581
pattern b at 2 in |- *; replace b with (Rmax a b).
2582
rewrite <- H2; rewrite H3; reflexivity.
2583
unfold Rmax in |- *; case (Rle_dec a b); intro;
2584
[ reflexivity | elim n; assumption ].
2585
unfold Rmin in |- *; case (Rle_dec a b); intro;
2586
[ reflexivity | elim n; assumption ].
2587
split with (cons r nil); split with lf1; assert (H2 : c = b).
2588
rewrite H1 in H0; elim H0; intros; apply Rle_antisym; assumption.
2589
rewrite <- H2 in H1; rewrite <- H1; assumption.
2590
intros r1 r2 _ X0 lf1 a b c f H H0; induction lf1 as [| r3 lf1 Hreclf1].
2591
unfold adapted_couple in H; decompose [and] H; clear H; simpl in H4;
2593
clear Hreclf1; assert (H1 : {c <= r1} + {r1 < c}).
2594
case (Rle_dec c r1); intro; [ left; assumption | right; auto with real ].
2596
split with (cons c (cons r1 r2)); split with (cons r3 lf1);
2597
unfold adapted_couple in H; decompose [and] H; clear H;
2598
unfold adapted_couple in |- *; repeat split.
2599
unfold ordered_Rlist in |- *; intros; simpl in H; induction i as [| i Hreci].
2600
simpl in |- *; assumption.
2601
clear Hreci; apply (H2 (S i)); simpl in |- *; assumption.
2602
simpl in |- *; unfold Rmin in |- *; case (Rle_dec c b); intro;
2603
[ reflexivity | elim n; elim H0; intros; assumption ].
2604
replace (Rmax c b) with (Rmax a b).
2605
rewrite <- H3; reflexivity.
2606
unfold Rmax in |- *; case (Rle_dec a b); case (Rle_dec c b); intros;
2608
| elim n; elim H0; intros; assumption
2609
| elim n; elim H0; intros; apply Rle_trans with c; assumption
2610
| elim n0; elim H0; intros; apply Rle_trans with c; assumption ].
2611
simpl in |- *; simpl in H5; apply H5.
2612
intros; simpl in H; induction i as [| i Hreci].
2613
unfold constant_D_eq, open_interval in |- *; intros; simpl in |- *;
2615
simpl in |- *; apply lt_O_Sn.
2616
unfold open_interval in |- *; simpl in |- *; simpl in H6; elim H6; clear H6;
2617
intros; split; try assumption; apply Rle_lt_trans with c;
2618
try assumption; replace r with a.
2619
elim H0; intros; assumption.
2620
simpl in H4; rewrite H4; unfold Rmin in |- *; case (Rle_dec a b); intros;
2622
| elim n; elim H0; intros; apply Rle_trans with c; assumption ].
2623
clear Hreci; apply (H7 (S i)); simpl in |- *; assumption.
2624
cut (adapted_couple f r1 b (cons r1 r2) lf1).
2626
intros; elim (X0 _ _ _ _ _ H3 H2); intros l1' [lf1' H4]; split with l1';
2627
split with lf1'; assumption.
2628
split; [ left; assumption | elim H0; intros; assumption ].
2630
[ elim H0; intros; apply Rle_trans with c; [ apply H2 | apply H3 ]
2635
forall (f:R -> R) (a b c:R),
2636
IsStepFun f a b -> IsStepFun f b c -> IsStepFun f a c.
2638
intros f; intros; case (Rle_dec a b); case (Rle_dec b c); intros.
2639
apply StepFun_P41 with b; assumption.
2640
case (Rle_dec a c); intro.
2641
apply StepFun_P44 with b; try assumption.
2642
split; [ assumption | auto with real ].
2643
apply StepFun_P6; apply StepFun_P44 with b.
2644
apply StepFun_P6; assumption.
2645
split; auto with real.
2646
case (Rle_dec a c); intro.
2647
apply StepFun_P45 with b; try assumption.
2648
split; auto with real.
2649
apply StepFun_P6; apply StepFun_P45 with b.
2650
apply StepFun_P6; assumption.
2651
split; [ assumption | auto with real ].
2652
apply StepFun_P6; apply StepFun_P41 with b;
2653
auto with real || apply StepFun_P6; assumption.
added
removed
theories/Reals/RiemannInt_SF.v
