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: NewtonInt.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
12
Require Import Rfunctions.
13
Require Import SeqSeries.
14
Require Import Rtrigo.
15
Require Import Ranalysis.
16
Open Local Scope R_scope.
18
(*******************************************)
19
(* Newton's Integral *)
20
(*******************************************)
22
Definition Newton_integrable (f:R -> R) (a b:R) : Type :=
23
{ g:R -> R | antiderivative f g a b \/ antiderivative f g b a }.
25
Definition NewtonInt (f:R -> R) (a b:R) (pr:Newton_integrable f a b) : R :=
26
let (g,_) := pr in g b - g a.
28
(* If f is differentiable, then f' is Newton integrable (Tautology ?) *)
30
forall (f:Differential) (a b:R),
31
Newton_integrable (fun x:R => derive_pt f x (cond_diff f x)) a b.
33
intros f a b; unfold Newton_integrable in |- *; exists (d1 f);
34
unfold antiderivative in |- *; intros; case (Rle_dec a b);
36
[ left; split; [ intros; exists (cond_diff f x); reflexivity | assumption ]
38
[ intros; exists (cond_diff f x); reflexivity | auto with real ] ].
41
(* By definition, we have the Fondamental Theorem of Calculus *)
43
forall (f:Differential) (a b:R),
44
NewtonInt (fun x:R => derive_pt f x (cond_diff f x)) a b
45
(FTCN_step1 f a b) = f b - f a.
47
intros; unfold NewtonInt in |- *; reflexivity.
50
(* $\int_a^a f$ exists forall a:R and f:R->R *)
51
Lemma NewtonInt_P1 : forall (f:R -> R) (a:R), Newton_integrable f a a.
53
intros f a; unfold Newton_integrable in |- *;
54
exists (fct_cte (f a) * id)%F; left;
55
unfold antiderivative in |- *; split.
56
intros; assert (H1 : derivable_pt (fct_cte (f a) * id) x).
57
apply derivable_pt_mult.
58
apply derivable_pt_const.
59
apply derivable_pt_id.
60
exists H1; assert (H2 : x = a).
61
elim H; intros; apply Rle_antisym; assumption.
62
symmetry in |- *; apply derive_pt_eq_0;
63
replace (f x) with (0 * id x + fct_cte (f a) x * 1);
64
[ apply (derivable_pt_lim_mult (fct_cte (f a)) id x);
65
[ apply derivable_pt_lim_const | apply derivable_pt_lim_id ]
66
| unfold id, fct_cte in |- *; rewrite H2; ring ].
70
(* $\int_a^a f = 0$ *)
72
forall (f:R -> R) (a:R), NewtonInt f a a (NewtonInt_P1 f a) = 0.
74
intros; unfold NewtonInt in |- *; simpl in |- *;
75
unfold mult_fct, fct_cte, id in |- *; ring.
78
(* If $\int_a^b f$ exists, then $\int_b^a f$ exists too *)
80
forall (f:R -> R) (a b:R) (X:Newton_integrable f a b),
81
Newton_integrable f b a.
83
unfold Newton_integrable in |- *; intros; elim X; intros g H;
87
(* $\int_a^b f = -\int_b^a f$ *)
89
forall (f:R -> R) (a b:R) (pr:Newton_integrable f a b),
90
NewtonInt f a b pr = - NewtonInt f b a (NewtonInt_P3 f a b pr).
92
intros; unfold Newton_integrable in pr; elim pr; intros; elim p; intro.
93
unfold NewtonInt in |- *;
97
(fun g:R -> R => antiderivative f g a b \/ antiderivative f g b a) x
99
intros; elim o; intro.
100
unfold antiderivative in H0; elim H0; intros; elim H2; intro.
101
unfold antiderivative in H; elim H; intros;
102
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H5 H3)).
104
assert (H1 := antiderivative_Ucte f x x0 a b H H0); elim H1; intros;
105
unfold antiderivative in H0; elim H0; clear H0; intros _ H0.
106
assert (H3 : a <= a <= b).
107
split; [ right; reflexivity | assumption ].
108
assert (H4 : a <= b <= b).
109
split; [ assumption | right; reflexivity ].
110
assert (H5 := H2 _ H3); assert (H6 := H2 _ H4); rewrite H5; rewrite H6; ring.
111
unfold NewtonInt in |- *;
115
(fun g:R -> R => antiderivative f g a b \/ antiderivative f g b a) x
116
p)); intros; elim o; intro.
117
assert (H1 := antiderivative_Ucte f x x0 b a H H0); elim H1; intros;
118
unfold antiderivative in H0; elim H0; clear H0; intros _ H0.
119
assert (H3 : b <= a <= a).
120
split; [ assumption | right; reflexivity ].
121
assert (H4 : b <= b <= a).
122
split; [ right; reflexivity | assumption ].
123
assert (H5 := H2 _ H3); assert (H6 := H2 _ H4); rewrite H5; rewrite H6; ring.
124
unfold antiderivative in H0; elim H0; intros; elim H2; intro.
125
unfold antiderivative in H; elim H; intros;
126
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H5 H3)).
130
(* The set of Newton integrable functions is a vectorial space *)
132
forall (f g:R -> R) (l a b:R),
133
Newton_integrable f a b ->
134
Newton_integrable g a b ->
135
Newton_integrable (fun x:R => l * f x + g x) a b.
137
unfold Newton_integrable in |- *; intros f g l a b X X0;
138
elim X; intros; elim X0; intros;
139
exists (fun y:R => l * x y + x0 y).
142
left; unfold antiderivative in |- *; unfold antiderivative in H, H0; elim H;
143
clear H; intros; elim H0; clear H0; intros H0 _.
145
intros; elim (H _ H2); elim (H0 _ H2); intros.
146
assert (H5 : derivable_pt (fun y:R => l * x y + x0 y) x1).
148
exists H5; symmetry in |- *; reg; rewrite <- H3; rewrite <- H4; reflexivity.
150
unfold antiderivative in H, H0; elim H; elim H0; intros; elim H4; intro.
151
elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H5 H2)).
152
left; rewrite <- H5; unfold antiderivative in |- *; split.
153
intros; elim H6; intros; assert (H9 : x1 = a).
154
apply Rle_antisym; assumption.
155
assert (H10 : a <= x1 <= b).
156
split; right; [ symmetry in |- *; assumption | rewrite <- H5; assumption ].
157
assert (H11 : b <= x1 <= a).
158
split; right; [ rewrite <- H5; symmetry in |- *; assumption | assumption ].
159
assert (H12 : derivable_pt x x1).
160
unfold derivable_pt in |- *; exists (f x1); elim (H3 _ H10); intros;
161
eapply derive_pt_eq_1; symmetry in |- *; apply H12.
162
assert (H13 : derivable_pt x0 x1).
163
unfold derivable_pt in |- *; exists (g x1); elim (H1 _ H11); intros;
164
eapply derive_pt_eq_1; symmetry in |- *; apply H13.
165
assert (H14 : derivable_pt (fun y:R => l * x y + x0 y) x1).
167
exists H14; symmetry in |- *; reg.
168
assert (H15 : derive_pt x0 x1 H13 = g x1).
169
elim (H1 _ H11); intros; rewrite H15; apply pr_nu.
170
assert (H16 : derive_pt x x1 H12 = f x1).
171
elim (H3 _ H10); intros; rewrite H16; apply pr_nu.
172
rewrite H15; rewrite H16; ring.
175
unfold antiderivative in H, H0; elim H; elim H0; intros; elim H4; intro.
176
elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H5 H2)).
177
left; rewrite H5; unfold antiderivative in |- *; split.
178
intros; elim H6; intros; assert (H9 : x1 = a).
179
apply Rle_antisym; assumption.
180
assert (H10 : a <= x1 <= b).
181
split; right; [ symmetry in |- *; assumption | rewrite H5; assumption ].
182
assert (H11 : b <= x1 <= a).
183
split; right; [ rewrite H5; symmetry in |- *; assumption | assumption ].
184
assert (H12 : derivable_pt x x1).
185
unfold derivable_pt in |- *; exists (f x1); elim (H3 _ H11); intros;
186
eapply derive_pt_eq_1; symmetry in |- *; apply H12.
187
assert (H13 : derivable_pt x0 x1).
188
unfold derivable_pt in |- *; exists (g x1); elim (H1 _ H10); intros;
189
eapply derive_pt_eq_1; symmetry in |- *; apply H13.
190
assert (H14 : derivable_pt (fun y:R => l * x y + x0 y) x1).
192
exists H14; symmetry in |- *; reg.
193
assert (H15 : derive_pt x0 x1 H13 = g x1).
194
elim (H1 _ H10); intros; rewrite H15; apply pr_nu.
195
assert (H16 : derive_pt x x1 H12 = f x1).
196
elim (H3 _ H11); intros; rewrite H16; apply pr_nu.
197
rewrite H15; rewrite H16; ring.
199
right; unfold antiderivative in |- *; unfold antiderivative in H, H0; elim H;
200
clear H; intros; elim H0; clear H0; intros H0 _; split.
201
intros; elim (H _ H2); elim (H0 _ H2); intros.
202
assert (H5 : derivable_pt (fun y:R => l * x y + x0 y) x1).
204
exists H5; symmetry in |- *; reg; rewrite <- H3; rewrite <- H4; reflexivity.
209
Lemma antiderivative_P1 :
210
forall (f g F G:R -> R) (l a b:R),
211
antiderivative f F a b ->
212
antiderivative g G a b ->
213
antiderivative (fun x:R => l * f x + g x) (fun x:R => l * F x + G x) a b.
215
unfold antiderivative in |- *; intros; elim H; elim H0; clear H H0; intros;
217
intros; elim (H _ H3); elim (H1 _ H3); intros.
218
assert (H6 : derivable_pt (fun x:R => l * F x + G x) x).
220
exists H6; symmetry in |- *; reg; rewrite <- H4; rewrite <- H5; ring.
224
(* $\int_a^b \lambda f + g = \lambda \int_a^b f + \int_a^b f *)
226
forall (f g:R -> R) (l a b:R) (pr1:Newton_integrable f a b)
227
(pr2:Newton_integrable g a b),
228
NewtonInt (fun x:R => l * f x + g x) a b (NewtonInt_P5 f g l a b pr1 pr2) =
229
l * NewtonInt f a b pr1 + NewtonInt g a b pr2.
231
intros f g l a b pr1 pr2; unfold NewtonInt in |- *;
232
case (NewtonInt_P5 f g l a b pr1 pr2); intros; case pr1;
233
intros; case pr2; intros; case (total_order_T a b);
239
assert (H2 := antiderivative_P1 f g x0 x1 l a b H0 H1);
240
assert (H3 := antiderivative_Ucte _ _ _ _ _ H H2);
241
elim H3; intros; assert (H5 : a <= a <= b).
242
split; [ right; reflexivity | left; assumption ].
243
assert (H6 : a <= b <= b).
244
split; [ left; assumption | right; reflexivity ].
245
assert (H7 := H4 _ H5); assert (H8 := H4 _ H6); rewrite H7; rewrite H8; ring.
246
unfold antiderivative in H1; elim H1; intros;
247
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H3 a0)).
248
unfold antiderivative in H0; elim H0; intros;
249
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 a0)).
250
unfold antiderivative in H; elim H; intros;
251
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 a0)).
254
unfold antiderivative in H; elim H; intros;
255
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 r)).
257
unfold antiderivative in H0; elim H0; intros;
258
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 r)).
260
unfold antiderivative in H1; elim H1; intros;
261
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H3 r)).
262
assert (H2 := antiderivative_P1 f g x0 x1 l b a H0 H1);
263
assert (H3 := antiderivative_Ucte _ _ _ _ _ H H2);
264
elim H3; intros; assert (H5 : b <= a <= a).
265
split; [ left; assumption | right; reflexivity ].
266
assert (H6 : b <= b <= a).
267
split; [ right; reflexivity | left; assumption ].
268
assert (H7 := H4 _ H5); assert (H8 := H4 _ H6); rewrite H7; rewrite H8; ring.
271
Lemma antiderivative_P2 :
272
forall (f F0 F1:R -> R) (a b c:R),
273
antiderivative f F0 a b ->
274
antiderivative f F1 b c ->
277
match Rle_dec x b with
279
| right _ => F1 x + (F0 b - F1 b)
282
unfold antiderivative in |- *; intros; elim H; clear H; intros; elim H0;
283
clear H0; intros; split.
284
2: apply Rle_trans with b; assumption.
285
intros; elim H3; clear H3; intros; case (total_order_T x b); intro.
287
assert (H5 : a <= x <= b).
288
split; [ assumption | left; assumption ].
289
assert (H6 := H _ H5); elim H6; clear H6; intros;
294
match Rle_dec x b with
296
| right _ => F1 x + (F0 b - F1 b)
298
unfold derivable_pt_lim in |- *; assert (H7 : derive_pt F0 x x0 = f x).
299
symmetry in |- *; assumption.
300
assert (H8 := derive_pt_eq_1 F0 x (f x) x0 H7); unfold derivable_pt_lim in H8;
301
intros; elim (H8 _ H9); intros; set (D := Rmin x1 (b - x)).
302
assert (H11 : 0 < D).
303
unfold D in |- *; unfold Rmin in |- *; case (Rle_dec x1 (b - x)); intro.
305
apply Rlt_Rminus; assumption.
306
exists (mkposreal _ H11); intros; case (Rle_dec x b); intro.
307
case (Rle_dec (x + h) b); intro.
310
apply Rlt_le_trans with D; [ assumption | unfold D in |- *; apply Rmin_l ].
311
elim n; left; apply Rlt_le_trans with (x + D).
312
apply Rplus_lt_compat_l; apply Rle_lt_trans with (Rabs h).
315
apply Rplus_le_reg_l with (- x); rewrite <- Rplus_assoc; rewrite Rplus_opp_l;
316
rewrite Rplus_0_l; rewrite Rplus_comm; unfold D in |- *;
318
elim n; left; assumption.
323
match Rle_dec x b with
325
| right _ => F1 x + (F0 b - F1 b)
327
unfold derivable_pt in |- *; exists (f x); apply H7.
328
exists H8; symmetry in |- *; apply derive_pt_eq_0; apply H7.
329
assert (H5 : a <= x <= b).
330
split; [ assumption | right; assumption ].
331
assert (H6 : b <= x <= c).
332
split; [ right; symmetry in |- *; assumption | assumption ].
333
elim (H _ H5); elim (H0 _ H6); intros; assert (H9 : derive_pt F0 x x1 = f x).
334
symmetry in |- *; assumption.
335
assert (H10 : derive_pt F1 x x0 = f x).
336
symmetry in |- *; assumption.
337
assert (H11 := derive_pt_eq_1 F0 x (f x) x1 H9);
338
assert (H12 := derive_pt_eq_1 F1 x (f x) x0 H10);
343
match Rle_dec x b with
345
| right _ => F1 x + (F0 b - F1 b)
347
unfold derivable_pt_lim in |- *; unfold derivable_pt_lim in H11, H12; intros;
348
elim (H11 _ H13); elim (H12 _ H13); intros; set (D := Rmin x2 x3);
349
assert (H16 : 0 < D).
350
unfold D in |- *; unfold Rmin in |- *; case (Rle_dec x2 x3); intro.
353
exists (mkposreal _ H16); intros; case (Rle_dec x b); intro.
354
case (Rle_dec (x + h) b); intro.
357
apply Rlt_le_trans with D; [ assumption | unfold D in |- *; apply Rmin_r ].
358
replace (F1 (x + h) + (F0 b - F1 b) - F0 x) with (F1 (x + h) - F1 x).
361
apply Rlt_le_trans with D; [ assumption | unfold D in |- *; apply Rmin_l ].
363
elim n; right; assumption.
368
match Rle_dec x b with
370
| right _ => F1 x + (F0 b - F1 b)
372
unfold derivable_pt in |- *; exists (f x); apply H13.
373
exists H14; symmetry in |- *; apply derive_pt_eq_0; apply H13.
374
assert (H5 : b <= x <= c).
375
split; [ left; assumption | assumption ].
376
assert (H6 := H0 _ H5); elim H6; clear H6; intros;
381
match Rle_dec x b with
383
| right _ => F1 x + (F0 b - F1 b)
385
unfold derivable_pt_lim in |- *; assert (H7 : derive_pt F1 x x0 = f x).
386
symmetry in |- *; assumption.
387
assert (H8 := derive_pt_eq_1 F1 x (f x) x0 H7); unfold derivable_pt_lim in H8;
388
intros; elim (H8 _ H9); intros; set (D := Rmin x1 (x - b));
389
assert (H11 : 0 < D).
390
unfold D in |- *; unfold Rmin in |- *; case (Rle_dec x1 (x - b)); intro.
392
apply Rlt_Rminus; assumption.
393
exists (mkposreal _ H11); intros; case (Rle_dec x b); intro.
394
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r0 r)).
395
case (Rle_dec (x + h) b); intro.
397
intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r0 H14)).
398
apply Rplus_lt_reg_r with (- h - b); replace (- h - b + b) with (- h);
399
[ idtac | ring ]; replace (- h - b + (x + h)) with (x - b);
400
[ idtac | ring ]; apply Rle_lt_trans with (Rabs h).
401
rewrite <- Rabs_Ropp; apply RRle_abs.
402
apply Rlt_le_trans with D.
404
unfold D in |- *; apply Rmin_r.
405
replace (F1 (x + h) + (F0 b - F1 b) - (F1 x + (F0 b - F1 b))) with
406
(F1 (x + h) - F1 x); [ idtac | ring ]; apply H10.
408
apply Rlt_le_trans with D.
410
unfold D in |- *; apply Rmin_l.
415
match Rle_dec x b with
417
| right _ => F1 x + (F0 b - F1 b)
419
unfold derivable_pt in |- *; exists (f x); apply H7.
420
exists H8; symmetry in |- *; apply derive_pt_eq_0; apply H7.
423
Lemma antiderivative_P3 :
424
forall (f F0 F1:R -> R) (a b c:R),
425
antiderivative f F0 a b ->
426
antiderivative f F1 c b ->
427
antiderivative f F1 c a \/ antiderivative f F0 a c.
429
intros; unfold antiderivative in H, H0; elim H; clear H; elim H0; clear H0;
430
intros; case (total_order_T a c); intro.
432
right; unfold antiderivative in |- *; split.
433
intros; apply H1; elim H3; intros; split;
434
[ assumption | apply Rle_trans with c; assumption ].
436
right; unfold antiderivative in |- *; split.
437
intros; apply H1; elim H3; intros; split;
438
[ assumption | apply Rle_trans with c; assumption ].
440
left; unfold antiderivative in |- *; split.
441
intros; apply H; elim H3; intros; split;
442
[ assumption | apply Rle_trans with a; assumption ].
446
Lemma antiderivative_P4 :
447
forall (f F0 F1:R -> R) (a b c:R),
448
antiderivative f F0 a b ->
449
antiderivative f F1 a c ->
450
antiderivative f F1 b c \/ antiderivative f F0 c b.
452
intros; unfold antiderivative in H, H0; elim H; clear H; elim H0; clear H0;
453
intros; case (total_order_T c b); intro.
455
right; unfold antiderivative in |- *; split.
456
intros; apply H1; elim H3; intros; split;
457
[ apply Rle_trans with c; assumption | assumption ].
459
right; unfold antiderivative in |- *; split.
460
intros; apply H1; elim H3; intros; split;
461
[ apply Rle_trans with c; assumption | assumption ].
463
left; unfold antiderivative in |- *; split.
464
intros; apply H; elim H3; intros; split;
465
[ apply Rle_trans with b; assumption | assumption ].
470
forall (f:R -> R) (a b c:R),
473
Newton_integrable f a b ->
474
Newton_integrable f b c -> Newton_integrable f a c.
476
unfold Newton_integrable in |- *; intros f a b c Hab Hbc X X0; elim X;
477
clear X; intros F0 H0; elim X0; clear X0; intros F1 H1;
481
match Rle_dec x b with
483
| right _ => F1 x + (F0 b - F1 b)
484
end); exists g; left; unfold g in |- *;
485
apply antiderivative_P2.
488
unfold antiderivative in H; elim H; clear H; intros;
489
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 Hab)).
492
unfold antiderivative in H; elim H; clear H; intros;
493
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 Hbc)).
497
forall (f:R -> R) (a b c:R),
498
Newton_integrable f a b ->
499
Newton_integrable f b c -> Newton_integrable f a c.
502
elim X; intros F0 H0.
503
elim X0; intros F1 H1.
504
case (total_order_T a b); intro.
506
case (total_order_T b c); intro.
509
unfold Newton_integrable in |- *;
512
match Rle_dec x b with
514
| right _ => F1 x + (F0 b - F1 b)
518
left; apply antiderivative_P2; assumption.
519
unfold antiderivative in H2; elim H2; clear H2; intros _ H2.
520
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 a1)).
521
unfold antiderivative in H; elim H; clear H; intros _ H.
522
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H a0)).
524
rewrite b0 in X; apply X.
526
case (total_order_T a c); intro.
528
unfold Newton_integrable in |- *; exists F0.
531
unfold antiderivative in H; elim H; clear H; intros _ H.
532
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)).
534
assert (H3 := antiderivative_P3 f F0 F1 a b c H2 H).
536
unfold antiderivative in H4; elim H4; clear H4; intros _ H4.
537
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 a1)).
539
unfold antiderivative in H2; elim H2; clear H2; intros _ H2.
540
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 a0)).
541
rewrite b0; apply NewtonInt_P1.
542
unfold Newton_integrable in |- *; exists F1.
545
unfold antiderivative in H; elim H; clear H; intros _ H.
546
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)).
548
assert (H3 := antiderivative_P3 f F0 F1 a b c H2 H).
551
unfold antiderivative in H4; elim H4; clear H4; intros _ H4.
552
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 r0)).
553
unfold antiderivative in H2; elim H2; clear H2; intros _ H2.
554
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 a0)).
556
rewrite b0; apply X0.
557
case (total_order_T b c); intro.
560
case (total_order_T a c); intro.
562
unfold Newton_integrable in |- *; exists F1.
567
unfold antiderivative in H2; elim H2; clear H2; intros _ H2.
568
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 r)).
569
assert (H3 := antiderivative_P4 f F0 F1 b a c H2 H).
572
unfold antiderivative in H4; elim H4; clear H4; intros _ H4.
573
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 a1)).
574
unfold antiderivative in H; elim H; clear H; intros _ H.
575
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H a0)).
576
rewrite b0; apply NewtonInt_P1.
577
unfold Newton_integrable in |- *; exists F0.
580
unfold antiderivative in H; elim H; clear H; intros _ H.
581
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)).
583
assert (H3 := antiderivative_P4 f F0 F1 b a c H H2).
585
unfold antiderivative in H4; elim H4; clear H4; intros _ H4.
586
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 r0)).
588
unfold antiderivative in H2; elim H2; clear H2; intros _ H2.
589
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 a0)).
591
rewrite b0 in X; apply X.
593
assert (X1 := NewtonInt_P3 f a b X).
594
assert (X2 := NewtonInt_P3 f b c X0).
596
apply NewtonInt_P7 with b; assumption.
599
(* Chasles' relation *)
601
forall (f:R -> R) (a b c:R) (pr1:Newton_integrable f a b)
602
(pr2:Newton_integrable f b c),
603
NewtonInt f a c (NewtonInt_P8 f a b c pr1 pr2) =
604
NewtonInt f a b pr1 + NewtonInt f b c pr2.
606
intros; unfold NewtonInt in |- *.
607
case (NewtonInt_P8 f a b c pr1 pr2); intros.
610
case (total_order_T a b); intro.
612
case (total_order_T b c); intro.
618
assert (H2 := antiderivative_P2 f x0 x1 a b c H H0).
621
antiderivative_Ucte f x
623
match Rle_dec x b with
625
| right _ => x1 x + (x0 b - x1 b)
628
assert (H5 : a <= a <= c).
629
split; [ right; reflexivity | left; apply Rlt_trans with b; assumption ].
630
assert (H6 : a <= c <= c).
631
split; [ left; apply Rlt_trans with b; assumption | right; reflexivity ].
632
rewrite (H4 _ H5); rewrite (H4 _ H6).
633
case (Rle_dec a b); intro.
634
case (Rle_dec c b); intro.
635
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r0 a1)).
637
elim n; left; assumption.
638
unfold antiderivative in H1; elim H1; clear H1; intros _ H1.
639
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 (Rlt_trans _ _ _ a0 a1))).
640
unfold antiderivative in H0; elim H0; clear H0; intros _ H0.
641
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 a1)).
642
unfold antiderivative in H; elim H; clear H; intros _ H.
643
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H a0)).
646
unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rplus_0_r.
650
assert (H1 := antiderivative_Ucte f x x0 a b H0 H).
655
split; [ right; reflexivity | left; assumption ].
656
split; [ left; assumption | right; reflexivity ].
657
unfold antiderivative in H0; elim H0; clear H0; intros _ H0.
658
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 a0)).
659
unfold antiderivative in H; elim H; clear H; intros _ H.
660
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H a0)).
663
unfold antiderivative in H; elim H; clear H; intros _ H.
664
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)).
667
assert (H2 := antiderivative_P2 f x x1 a c b H1 H).
668
assert (H3 := antiderivative_Ucte _ _ _ a b H0 H2).
672
case (Rle_dec b c); intro.
673
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r0 r)).
674
case (Rle_dec a c); intro.
676
elim n0; unfold antiderivative in H1; elim H1; intros; assumption.
677
split; [ left; assumption | right; reflexivity ].
678
split; [ right; reflexivity | left; assumption ].
679
assert (H2 := antiderivative_P2 _ _ _ _ _ _ H1 H0).
680
assert (H3 := antiderivative_Ucte _ _ _ c b H H2).
684
case (Rle_dec b a); intro.
685
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r0 a0)).
686
case (Rle_dec c a); intro.
688
elim n0; unfold antiderivative in H1; elim H1; intros; assumption.
689
split; [ left; assumption | right; reflexivity ].
690
split; [ right; reflexivity | left; assumption ].
691
unfold antiderivative in H0; elim H0; clear H0; intros _ H0.
692
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 a0)).
694
rewrite b0 in o; rewrite b0.
697
assert (H1 := antiderivative_Ucte _ _ _ b c H H0).
699
assert (H3 : b <= c).
700
unfold antiderivative in H; elim H; intros; assumption.
704
split; [ assumption | right; reflexivity ].
705
split; [ right; reflexivity | assumption ].
707
unfold antiderivative in H, H0; elim H; elim H0; intros; apply Rle_antisym;
712
unfold antiderivative in H, H0; elim H; elim H0; intros; apply Rle_antisym;
715
assert (H1 := antiderivative_Ucte _ _ _ c b H H0).
717
assert (H3 : c <= b).
718
unfold antiderivative in H; elim H; intros; assumption.
722
split; [ assumption | right; reflexivity ].
723
split; [ right; reflexivity | assumption ].
725
case (total_order_T b c); intro.
728
unfold antiderivative in H; elim H; clear H; intros _ H.
729
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)).
732
assert (H2 := antiderivative_P2 _ _ _ _ _ _ H H1).
733
assert (H3 := antiderivative_Ucte _ _ _ b c H0 H2).
737
case (Rle_dec b a); intro.
738
case (Rle_dec c a); intro.
740
unfold antiderivative in H1; elim H1; intros; apply Rle_antisym; assumption.
743
elim n; left; assumption.
744
split; [ left; assumption | right; reflexivity ].
745
split; [ right; reflexivity | left; assumption ].
746
assert (H2 := antiderivative_P2 _ _ _ _ _ _ H0 H1).
747
assert (H3 := antiderivative_Ucte _ _ _ b a H H2).
751
case (Rle_dec b c); intro.
752
case (Rle_dec a c); intro.
754
unfold antiderivative in H1; elim H1; intros; apply Rle_antisym; assumption.
757
elim n; left; assumption.
758
split; [ right; reflexivity | left; assumption ].
759
split; [ left; assumption | right; reflexivity ].
760
unfold antiderivative in H0; elim H0; clear H0; intros _ H0.
761
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 a0)).
764
unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rplus_0_r.
767
unfold antiderivative in H; elim H; clear H; intros _ H.
768
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)).
770
unfold antiderivative in H0; elim H0; clear H0; intros _ H0.
771
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 r)).
772
assert (H1 := antiderivative_Ucte f x x0 b a H0 H).
777
split; [ left; assumption | right; reflexivity ].
778
split; [ right; reflexivity | left; assumption ].
781
unfold antiderivative in H; elim H; clear H; intros _ H.
782
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)).
784
unfold antiderivative in H0; elim H0; clear H0; intros _ H0.
785
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 r0)).
787
unfold antiderivative in H1; elim H1; clear H1; intros _ H1.
788
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 (Rlt_trans _ _ _ r0 r))).
789
assert (H2 := antiderivative_P2 _ _ _ _ _ _ H0 H).
790
assert (H3 := antiderivative_Ucte _ _ _ c a H1 H2).
792
assert (H5 : c <= a).
793
unfold antiderivative in H1; elim H1; intros; assumption.
796
case (Rle_dec a b); intro.
797
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r1 r)).
798
case (Rle_dec c b); intro.
800
elim n0; left; assumption.
801
split; [ assumption | right; reflexivity ].
802
split; [ right; reflexivity | assumption ].
added
removed
theories/Reals/NewtonInt.v
