forked from AbsInt/CompCert
-
Notifications
You must be signed in to change notification settings - Fork 1
/
IteratedRInt.v
763 lines (683 loc) · 24.9 KB
/
IteratedRInt.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
(* Libray for Iterated Improper Integrals.
We define iterated integration two ways:
1) Vector based (is_IIRInt): The range of integration is specified as a vector of n intervals,
and the integrand is a function of type Vector.t R n -> R. This is defined inductively
as repeated nesting of IIRint.
2) List based (is_IIRInt_list): The range of integration is specified as a list of intervals, and
the integrand is a function of type list R -> R.
The former feels more "proper" in some sense, as the types rule out
a mismatch between the length of the arguments that the integrand
expects vs. the length of the variable of integration. On the other
hand, it means dealing with dependent types and vectors, which can
be frustrating.
*)
Require Import Utf8.
Inductive Forall3 {A B C : Type} (P : A → B → C → Prop) : list A → list B → list C → Prop :=
Forall3_nil : Forall3 P (nil) (nil) (nil)
| Forall3_cons : ∀ (x1 : A) (x2 : B) (x3 :C) (v1 : list A) (v2 : list B) (v3: list C),
P x1 x2 x3 → Forall3 P v1 v2 v3 →
Forall3 P (cons x1 v1) (cons x2 v2) (cons x3 v3).
Arguments Forall3 {A B C}%type_scope _%function_scope.
Arguments Forall3_nil {A B C}%type_scope _%function_scope.
Arguments Forall3_cons {A B C}%type_scope _%function_scope.
From Coq Require Import Reals Psatz ssreflect ssrbool Utf8 Vector.
From mathcomp Require Import eqtype seq.
Require Import Coq.Program.Equality.
From Coquelicot Require Import Markov Rcomplements Lub Lim_seq SF_seq Continuity Hierarchy RInt RInt_analysis Derive.
From Coquelicot Require Export Rbar.
Require Import RealsExt ImproperRInt.
Set Bullet Behavior "Strict Subproofs".
Set Default Goal Selector "!".
Ltac sigT_inj :=
repeat match goal with
| [ H: existT _ _ _ = existT _ _ _ |- _ ] =>
apply Classical_Prop.EqdepTheory.inj_pair2 in H; subst
end.
Record interval := mk_interval { interval_lb : Rbar; interval_ub : Rbar}.
Definition interval_subset (i1 i2: interval) :=
Rbar_le (interval_lb i2) (interval_lb i1) /\ Rbar_le (interval_ub i1) (interval_ub i2).
Definition rectangle n := Vector.t (interval) n.
Definition vsingle {A: Type} (a: A) :=
cons A a O (nil A).
Definition in_interval (x: R) (i: interval) :=
Rbar_lt (interval_lb i) x /\ Rbar_lt x (interval_ub i).
Definition in_rectangle {n: nat} (x: Vector.t _ n) (r: rectangle n) :=
Forall2 in_interval x r.
Definition rectangle_subset {n} (r1 r2: rectangle n) :=
Forall2 interval_subset r1 r2.
Definition wf_interval (i: interval) :=
Rbar_lt (interval_lb i) (interval_ub i).
Definition wf_rectangle (n: nat) (v: rectangle n) :=
VectorDef.Forall wf_interval v.
Definition wf_rectangle_list (v: list interval) :=
List.Forall wf_interval v.
Definition IIRInt (n: nat) (f: Vector.t R n -> R) (r: rectangle n) : R.
Proof.
destruct n as [| n].
- exact 0.
- induction n as [| n' IH].
{ inversion r.
exact (IRInt (λ x, f (vsingle x)) (interval_lb h) (interval_ub h)).
}
{ inversion r.
exact (IRInt (λ x, IH (λ xbar, f (cons _ x _ xbar)) H0) (interval_lb h) (interval_ub h)).
}
Defined.
Lemma IIRInt_unfold_nil f r :
IIRInt 0 f r = 0.
Proof. rewrite //=. Qed.
Lemma IIRInt_unfold_vsingle f i :
IIRInt 1 f (vsingle i) = IRInt (λ x, f (vsingle x)) (interval_lb i) (interval_ub i).
Proof. rewrite //=. Qed.
Lemma IIRInt_unfold_cons n (f : Vector.t R (S (S n)) -> R) i r:
IIRInt (S (S n)) f (cons _ i _ r) =
IRInt (λ x, IIRInt (S n) (λ xbar, f (cons _ x _ xbar)) r) (interval_lb i) (interval_ub i).
Proof. rewrite //=. Qed.
Opaque IIRInt.
Inductive is_IIRInt : forall n, (Vector.t R n -> R) -> rectangle n -> R -> Prop :=
| is_IIRint_1d (f: Vector.t R 1 -> R) (i: interval) (v : R) :
is_IRInt (λ x, f (vsingle x)) (interval_lb i) (interval_ub i) v ->
is_IIRInt 1 f (vsingle i) v
| is_IIRint_cons n (f : Vector.t R (S (S n)) -> R) (i: interval) (r: rectangle (S n)) (v : R) :
(∀ x, in_interval x i -> ∃ v', is_IIRInt (S n) (λ xbar, f (cons _ x _ xbar)) r v') ->
is_IRInt (λ x, IIRInt (S n) (λ xbar, f (cons _ x _ xbar)) r) (interval_lb i) (interval_ub i) v ->
is_IIRInt (S (S n)) f (cons _ i _ r) v.
Definition ex_IIRInt n f r :=
∃ v, is_IIRInt n f r v.
Lemma IIRInt_correct n f r :
ex_IIRInt n f r -> is_IIRInt n f r (IIRInt n f r).
Proof.
rewrite /ex_IIRInt. intros (v&His).
destruct n.
{ inversion His. }
induction n as [| n' IH]; inversion His; subst; sigT_inj.
- rewrite IIRInt_unfold_vsingle. econstructor.
apply IRInt_correct. eexists; eauto.
- rewrite IIRInt_unfold_cons. econstructor; eauto.
apply IRInt_correct. eexists; eauto.
Qed.
Lemma is_IIRInt_unique n f r v :
is_IIRInt n f r v -> IIRInt n f r = v.
Proof.
intros His.
destruct n.
{ inversion His. }
induction n as [| n' IH]; inversion His; subst; sigT_inj.
- rewrite IIRInt_unfold_vsingle. apply is_IRInt_unique; auto.
- rewrite IIRInt_unfold_cons. apply is_IRInt_unique; auto.
Qed.
Lemma is_IIRInt_ext:
∀ n f g r (v : R),
wf_rectangle n r →
(∀ x, in_rectangle x r → f x = g x) →
is_IIRInt n f r v → is_IIRInt n g r v.
Proof.
intros n.
destruct n.
{ intros ???? Hwf Hext His. inversion His. }
induction n as [| n' IH] => f g r v Hwf Hext His; inversion His; subst; sigT_inj.
- econstructor. eapply is_IRInt_ext; eauto.
{ inversion Hwf; sigT_inj; eauto. }
{ intros. apply Hext. rewrite /in_rectangle.
apply Forall2_cons; last apply Forall2_nil.
split; intuition.
}
- econstructor.
{ intros. edestruct H2 as (v'&Hv'); eauto. exists v'. eapply IH; eauto.
{ inversion Hwf; sigT_inj; eauto. }
intros. eapply Hext. econstructor; eauto.
}
eapply is_IRInt_ext.
{ inversion Hwf; sigT_inj; eauto. }
{ intros. symmetry. apply is_IIRInt_unique.
eapply IH.
{ inversion Hwf; sigT_inj; eauto. }
{ intros. eapply Hext. econstructor; eauto. }
eapply IIRInt_correct. edestruct (H2 x); eauto.
eexists; eauto.
}
eauto.
Qed.
Ltac nil_vect :=
repeat match goal with
| [ H : t ?A 0 |- _ ] =>
assert (H = @nil _) by (dependent induction H; auto); subst
end.
Lemma IIRInt_ext n f g r :
wf_rectangle n r →
(∀ x, in_rectangle x r → f x = g x) ->
IIRInt n f r = IIRInt n g r.
Proof.
revert f g r.
destruct n.
{ intros ??? Hwf Hext. rewrite ?IIRInt_nil //. }
induction n as [| n' IH] => f g r Hwf Hext.
- inversion Hwf. sigT_inj; nil_vect.
rewrite (IIRInt_unfold_vsingle).
rewrite (IIRInt_unfold_vsingle).
eapply IRInt_ext; eauto.
{ intros y Hlt. apply Hext. econstructor; eauto. econstructor. }
- inversion Hwf; sigT_inj.
rewrite IIRInt_unfold_cons.
rewrite IIRInt_unfold_cons.
eapply IRInt_ext; auto.
intros y Hlt. eapply IH; eauto.
intros. apply Hext. econstructor; eauto.
Qed.
Lemma is_IIRInt_scal:
∀ n f r k (v : R),
wf_rectangle n r →
is_IIRInt n f r v → is_IIRInt n (λ y, scal k (f y)) r (scal k v).
Proof.
intros n f r k v Hwf His.
destruct n.
{ inversion His. }
revert v His.
induction n as [| n' IH] => v His; inversion His; subst; sigT_inj.
- econstructor. eapply is_IRInt_scal; auto.
rewrite /wf_rectangle in Hwf. inversion Hwf; subst; sigT_inj; eauto.
- econstructor.
{ intros y Hin. edestruct (H2 y) as (v'&Hv'); eauto. eexists.
eapply IH; eauto.
{ inversion Hwf; sigT_inj; eauto. }
}
eapply (is_IRInt_ext (λ x, scal k (IIRInt _ (λ xbar, f (cons R x (S n') xbar)) _))).
{ inversion Hwf; eauto. }
{ intros. symmetry. apply is_IIRInt_unique.
eapply IH.
{ inversion Hwf; sigT_inj; eauto. }
eapply IIRInt_correct. edestruct (H2 x); eauto.
eexists; eauto.
}
eapply is_IRInt_scal; eauto.
{ inversion Hwf; eauto. }
Qed.
Lemma IIRInt_scal:
∀ n f r k,
wf_rectangle n r →
ex_IIRInt n f r →
IIRInt n (λ y, scal k (f y)) r =
scal k (IIRInt n f r).
Proof.
intros n f r k Hwf Hex.
apply is_IIRInt_unique, is_IIRInt_scal; auto.
apply IIRInt_correct; auto.
Qed.
Definition strict_monotone_on_interval (i: interval) (f: R -> R) :=
(∀ (x y : R), Rbar_lt (interval_lb i) x /\ x < y /\ Rbar_lt y (interval_ub i) ->
f x < f y).
Inductive VectorForall3 {A B C : Type} (P : A → B → C → Prop) : ∀ n : nat, t A n → t B n → t C n → Prop :=
VectorForall3_nil : VectorForall3 P _ (nil A) (nil B) (nil C)
| VectorForall3_cons : ∀ (m : nat) (x1 : A) (x2 : B) (x3 :C) (v1 : t A m) (v2 : t B m) (v3: t C m),
P x1 x2 x3 → VectorForall3 P _ v1 v2 v3 →
VectorForall3 P _ (cons A x1 m v1) (cons B x2 m v2) (cons C x3 m v3).
Arguments VectorForall3 {A B C}%type_scope _%function_scope {n}%nat_scope.
Arguments VectorForall3_nil {A B C}%type_scope _%function_scope.
Arguments VectorForall3_cons {A B C}%type_scope _%function_scope {m}%nat_scope.
Definition continuous_derive_on_interval (i: interval) (g: R -> R) (dg: R -> R) :=
(∀ (x : R), Rbar_lt (interval_lb i) x /\ Rbar_lt x (interval_ub i) →
is_derive g x (dg x) ∧ continuous dg x).
Definition is_interval_image (g: R -> R) (i i': interval) :=
(∀ (x : R), Rbar_lt (interval_lb i) x /\ Rbar_lt x (interval_ub i) →
Rbar_lt (interval_lb i') (g x) /\ Rbar_lt (g x) (interval_ub i')) /\
is_right_lim g (interval_lb i) (interval_lb i') /\
is_left_lim g (interval_ub i) (interval_ub i').
Definition vector_apply {A B n} (fs: Vector.t (A -> B) n) (xs: Vector.t A n) : Vector.t B n :=
VectorDef.map2 (λ f x, f x) fs xs.
Definition vector_mult {n} (xs: Vector.t R n) : R :=
VectorDef.fold_right (Rmult) xs 1.
Lemma is_interval_image_spec f i1 i2 x:
is_interval_image f i1 i2 →
in_interval x i1 →
in_interval (f x) i2.
Proof.
intros (Hrange&_). apply Hrange.
Qed.
Lemma is_IIRInt_comp_noncont n (f : Vector.t R n → R)
(gs dgs : Vector.t (R → R) n) (r r': rectangle n) :
wf_rectangle n r ->
Forall2 strict_monotone_on_interval r gs ->
VectorForall3 is_interval_image gs r r' ->
VectorForall3 continuous_derive_on_interval r gs dgs ->
ex_IIRInt n f r' ->
is_IIRInt n (fun y => vector_mult (vector_apply dgs y) * (f (vector_apply gs y))) r (IIRInt n f r').
Proof.
revert r r' f gs dgs.
destruct n as [| n].
{ intros r r' f gs dgs Hwf Hmono Himage Hderive Hex. destruct Hex as (?&His). inversion His. }
induction n as [| n' IH].
- intros r r' f gs dgs Hwf Hmono Himage Hderive Hex.
inversion Hwf; sigT_inj; eauto.
inversion Himage. subst; sigT_inj.
nil_vect. econstructor.
dependent destruction dgs; nil_vect.
simpl. rewrite /vector_mult. simpl.
inversion Hderive; subst. sigT_inj.
rewrite IIRInt_unfold_vsingle.
eapply is_IRInt_ext; last first.
{ eapply is_IRInt_comp_noncont_strict; eauto; try eapply H6.
{ inversion Hmono; sigT_inj; eauto. }
destruct Hex as (?&His). inversion His; sigT_inj. eexists; eauto. }
{ intros. simpl. rewrite /vsingle/scal//=/mult/=. nra. }
{ eauto. }
- intros r r' f gs dgs Hwf Hmono Himage Hderive Hex.
inversion Hwf; sigT_inj; eauto.
inversion Himage. subst; sigT_inj.
econstructor.
{ intros. destruct Hex as (v'&His).
inversion His; sigT_inj.
assert (Hin: in_interval (x1 x0) x3).
{
eapply is_interval_image_spec; eauto.
}
edestruct (H8 _ Hin) as (vsub&Hvsub).
inversion Hderive; sigT_inj.
eexists.
simpl.
rewrite /vector_mult /=.
eapply is_IIRInt_ext; first eauto.
{ intros. rewrite Rmult_assoc. reflexivity. }
eapply (is_IIRInt_scal (S n')); eauto.
{ eapply (IH _ _ (λ y, f (cons _ (x1 x0) _ y))); eauto.
{ inversion Hmono; sigT_inj; eauto. }
{ eexists; eauto. }
}
}
inversion Hderive; sigT_inj.
simpl.
eapply (is_IRInt_ext (λ x, (scal (x4 x) (IIRInt _ (λ xbar, f (cons _ (x1 x) _ xbar)) _)))); first eauto.
{ intros. simpl.
inversion Hderive; sigT_inj.
rewrite /vector_mult /=.
symmetry.
erewrite IIRInt_ext; last first.
{ intros. rewrite Rmult_assoc. reflexivity. }
{ eauto. }
rewrite IIRInt_scal; eauto.
{
f_equal.
apply is_IIRInt_unique.
assert (Hin: in_interval (x1 x0) x3).
{
eapply is_interval_image_spec; eauto.
}
eapply (IH _ _ (λ y, f (cons _ (x1 x0) _ y))); eauto.
{ inversion Hmono; sigT_inj; eauto. }
{ destruct Hex as (?&His).
inversion His; subst; sigT_inj.
{ edestruct H11; eauto. eexists; eauto. }
}
}
{
assert (Hin: in_interval (x1 x0) x3).
{
eapply is_interval_image_spec; eauto.
}
destruct Hex as (?&His).
inversion His; subst; sigT_inj.
eexists.
eapply (IH _ _ (λ y, f (cons _ (x1 x0) _ y))); eauto.
{ inversion Hmono; sigT_inj; eauto. }
{ edestruct H11; eauto. eexists; eauto. }
}
}
rewrite IIRInt_unfold_cons.
eapply (is_IRInt_comp_noncont_strict (λ x0, IIRInt (S n') (λ y, f (cons _ x0 _ y)) v3)); eauto.
{ inversion Hmono; eauto. }
{ inversion Himage; eauto; sigT_inj; eapply H8. }
{ inversion Himage; eauto; sigT_inj; eapply H8. }
{ inversion Himage; eauto; sigT_inj; eapply H8. }
destruct Hex as (?&His). inversion His; sigT_inj. eexists; eauto.
Qed.
Section marginal.
Variable (V: Type).
Definition is_marginalized_to (f : V -> R -> R) (int: interval) (g: V -> R) :=
(∀ v, is_IRInt (f v) (interval_lb int) (interval_ub int) (g v)).
Definition Marginal f int (v : V) :=
IRInt (f v) (interval_lb int) (interval_ub int).
End marginal.
(* The same theory as IIRInt using lists instead of vectors *)
Import List.
Section IIRInt_list.
Definition rectangle_list := list (interval).
Definition in_list_rectangle (x: list R) (r: rectangle_list) :=
List.Forall2 in_interval x r.
Definition rectangle_list_subset (r1 r2: rectangle_list) :=
List.Forall2 interval_subset r1 r2.
Lemma interval_subset_trans i1 i2 i3 :
interval_subset i1 i2 ->
interval_subset i2 i3 ->
interval_subset i1 i3.
Proof.
destruct 1.
destruct 1.
split; etransitivity; eauto.
Qed.
Lemma rectangle_list_subset_trans r1 r2 r3 :
rectangle_list_subset r1 r2 ->
rectangle_list_subset r2 r3 ->
rectangle_list_subset r1 r3.
Proof.
intros Hsub1.
revert r3.
induction Hsub1.
{ inversion 1; econstructor. }
{ inversion 1; subst. inversion H0; subst. econstructor; last first.
{ eapply IHHsub1. eauto. }
eapply interval_subset_trans; eauto.
}
Qed.
Lemma rectangle_list_subset_refl r:
rectangle_list_subset r r.
Proof.
induction r.
- econstructor.
- econstructor.
{ split; reflexivity. }
{ eauto. }
Qed.
Lemma wf_rectangle_list_subset r1 r2 :
wf_rectangle_list r1 ->
rectangle_list_subset r1 r2 ->
wf_rectangle_list r2.
Proof.
rewrite /wf_rectangle_list/wf_interval/rectangle_list_subset/interval_subset.
intros Hwf Hrect. revert Hwf. induction Hrect; auto.
inversion 1; subst. econstructor; last first.
{ eapply IHHrect. eauto. }
eapply Rbar_le_lt_trans.
{ intuition eauto. }
eapply Rbar_lt_le_trans.
{ intuition eauto. }
{ intuition eauto. }
Qed.
Lemma in_list_rectangle_wf_rectangle p l :
in_list_rectangle p l ->
wf_rectangle_list l.
Proof.
induction 1.
- econstructor.
- econstructor; eauto.
destruct H. eapply Rbar_lt_trans; eauto.
Qed.
Fixpoint IIRInt_list (f: list R -> R) (r: rectangle_list) : R :=
match r with
| nil => 0
| i :: nil =>
IRInt (λ x, f (x :: nil)) (interval_lb i) (interval_ub i)
| i :: r' =>
IRInt (λ x, IIRInt_list (λ xbar, f (x :: xbar)) r') (interval_lb i) (interval_ub i)
end.
Lemma IIRInt_list_unfold_nil f :
IIRInt_list f nil = 0.
Proof. rewrite //=. Qed.
Lemma IIRInt_list_unfold_single f i :
IIRInt_list f (i :: nil) = IRInt (λ x, f (x :: nil)) (interval_lb i) (interval_ub i).
Proof. rewrite //=. Qed.
Lemma IIRInt_list_unfold_cons f i r:
r <> nil ->
IIRInt_list f (i :: r) =
IRInt (λ x, IIRInt_list (λ xbar, f (x :: xbar)) r) (interval_lb i) (interval_ub i).
Proof.
intros Hneq.
destruct r; first try congruence.
auto.
Qed.
Inductive is_IIRInt_list : (list R -> R) -> rectangle_list -> R -> Prop :=
| is_IIRint_list_1d (f: list R -> R) (i: interval) (v : R) :
is_IRInt (λ x, f (x :: nil)) (interval_lb i) (interval_ub i) v ->
is_IIRInt_list f (i :: nil) v
| is_IIRint_list_cons (f : list R -> R) (i: interval) (r: rectangle_list) (v : R) :
r <> nil ->
(∀ x, in_interval x i -> ∃ v', is_IIRInt_list (λ xbar, f (x :: xbar)) r v') ->
is_IRInt (λ x, IIRInt_list (λ xbar, f (x :: xbar)) r) (interval_lb i) (interval_ub i) v ->
is_IIRInt_list f (i :: r) v.
Definition ex_IIRInt_list f r :=
∃ v, is_IIRInt_list f r v.
Lemma IIRInt_list_correct f r :
ex_IIRInt_list f r -> is_IIRInt_list f r (IIRInt_list f r).
Proof.
rewrite /ex_IIRInt. intros (v&His).
induction His.
- econstructor; rewrite IIRInt_list_unfold_single. apply IRInt_correct. eexists; eauto.
- econstructor; eauto. rewrite IIRInt_list_unfold_cons; eauto.
apply IRInt_correct. eexists; eauto.
Qed.
Lemma is_IIRInt_list_unique f r v :
is_IIRInt_list f r v -> IIRInt_list f r = v.
Proof.
intros His.
induction His.
- rewrite IIRInt_list_unfold_single. apply is_IRInt_unique; auto.
- rewrite IIRInt_list_unfold_cons; auto. apply is_IRInt_unique; auto.
Qed.
Lemma IIRInt_list_IIRInt1 f r :
wf_rectangle _ (Vector.of_list r) ->
IIRInt_list f r =
IIRInt _ (λ x, f (Vector.to_list x)) (Vector.of_list r).
Proof.
revert f.
induction r; intros f Hwf.
- rewrite //=.
- destruct r.
* rewrite //=.
* rewrite IIRInt_unfold_cons. rewrite IIRInt_list_unfold_cons; last done. eapply IRInt_ext.
{ inversion Hwf. subst. sigT_inj. eauto. }
intros x Hlt.
rewrite IHr; last first.
{ inversion Hwf. subst. sigT_inj. eauto. }
simpl.
eapply IIRInt_ext.
{ inversion Hwf; subst. sigT_inj; eauto. }
intros. rewrite //=.
Qed.
Lemma IIRInt_list_ext f g r :
wf_rectangle_list r →
(∀ x, in_list_rectangle x r → f x = g x) ->
IIRInt_list f r = IIRInt_list g r.
Proof.
revert f g.
destruct r as [| i1 r].
{ rewrite //=. }
revert i1.
induction r as [| i2 r' IH] => i1 f g Hwf Hext.
- inversion Hwf; sigT_inj; nil_vect.
rewrite (IIRInt_list_unfold_single).
rewrite (IIRInt_list_unfold_single).
eapply IRInt_ext; eauto.
{ intros y Hlt. apply Hext. econstructor; eauto. }
- inversion Hwf; sigT_inj.
rewrite IIRInt_list_unfold_cons; last done.
rewrite IIRInt_list_unfold_cons; last done.
eapply IRInt_ext; auto.
intros y Hlt. eapply IH; eauto.
intros. apply Hext. econstructor; eauto.
Qed.
Lemma is_IIRInt_list_ext:
∀ f g r (v : R),
wf_rectangle_list r →
(∀ x, in_list_rectangle x r → f x = g x) →
is_IIRInt_list f r v → is_IIRInt_list g r v.
Proof.
intros f g r.
revert f g.
destruct r as [| i1 r]; intros f g v Hwf Hext His.
{ inversion His. }
revert i1 v f g Hwf Hext His.
induction r as [| i2 r' IH] => i1 v f g Hwf Hext His.
- inversion His; subst; last by congruence.
econstructor.
eapply is_IRInt_ext; eauto.
{ inversion Hwf; eauto. }
intros. eapply Hext. econstructor; eauto.
- inversion His; subst.
econstructor; first congruence.
{ intros. edestruct H3; eauto. eexists. eapply IH; eauto.
{ inversion Hwf; eauto. }
{ intros. eapply Hext. econstructor; eauto. }
}
eapply is_IRInt_ext; eauto.
{ inversion Hwf; eauto. }
{ intros. eapply IIRInt_list_ext; eauto.
{ inversion Hwf; eauto. }
intros. eapply Hext. econstructor; eauto.
}
Qed.
Lemma is_IIRInt_list_scal:
∀ f r k (v : R),
wf_rectangle_list r →
is_IIRInt_list f r v → is_IIRInt_list (λ y, scal k (f y)) r (scal k v).
Proof.
intros f r k v Hwf His.
destruct r as [| i1 r].
{ inversion His. }
revert i1 f v Hwf His.
induction r as [| i2 r' IH] => i1 f v Hwf His; inversion His; subst; try congruence.
- econstructor. eapply is_IRInt_scal; auto.
inversion Hwf; subst; sigT_inj; eauto.
- econstructor; eauto.
{ intros y Hin. edestruct (H3 y) as (v'&Hv'); eauto. eexists.
eapply IH; eauto.
{ inversion Hwf; sigT_inj; eauto. }
}
eapply (is_IRInt_ext (λ x, scal k (IIRInt_list (λ xbar, f (x :: xbar)) _))).
{ inversion Hwf; eauto. }
{ intros. symmetry. apply is_IIRInt_list_unique.
eapply IH.
{ inversion Hwf; sigT_inj; eauto. }
eapply IIRInt_list_correct. edestruct (H3 x); eauto.
eexists; eauto.
}
eapply is_IRInt_scal; eauto.
{ inversion Hwf; eauto. }
Qed.
Lemma IIRInt_list_scal:
∀ f r k,
wf_rectangle_list r →
ex_IIRInt_list f r →
IIRInt_list (λ y, scal k (f y)) r =
scal k (IIRInt_list f r).
Proof.
intros f r k Hwf Hex.
apply is_IIRInt_list_unique, is_IIRInt_list_scal; auto.
apply IIRInt_list_correct; auto.
Qed.
Definition list_apply {A B} (fs: list (A -> B)) (xs: list A) : list B :=
List.map (λ fx, (fst fx) (snd fx)) (List.combine fs xs).
Definition list_plus (xs: list R) : R :=
List.fold_right (Rplus) 0 xs.
Definition list_mult (xs: list R) : R :=
List.fold_right (Rmult) 1 xs.
Lemma is_IIRInt_list_comp_noncont (f : list R → R)
(gs dgs : list (R → R)) (r r': rectangle_list) :
wf_rectangle_list r ->
List.Forall2 strict_monotone_on_interval r gs ->
Forall3 is_interval_image gs r r' ->
Forall3 continuous_derive_on_interval r gs dgs ->
ex_IIRInt_list f r' ->
is_IIRInt_list (fun y => list_mult (list_apply dgs y) * (f (list_apply gs y))) r (IIRInt_list f r').
Proof.
revert r' f gs dgs.
destruct r as [| i1 r].
{ intros r' f gs dgs Hwf Hmono Himage Hderive Hex. destruct Hex as (?&His).
assert (r' = nil).
{ inversion Himage. eauto. }
{ subst. inversion His. }
}
revert i1.
induction r as [|i2 r IH].
- intros i1 r' f gs dgs Hwf Hmono Himage Hderive Hex.
inversion Hwf; sigT_inj; eauto.
inversion Himage. subst; sigT_inj.
econstructor.
dependent destruction dgs; nil_vect.
{ inversion Hderive. }
simpl. rewrite /list_mult. simpl.
inversion Hderive; subst. sigT_inj.
inversion H10. subst. simpl.
inversion H8. subst.
eapply is_IRInt_ext; last first.
{ eapply is_IRInt_comp_noncont_strict; eauto; try eapply H6.
{ inversion Hmono; sigT_inj; eauto. }
destruct Hex as (?&His). inversion His; sigT_inj; subst.
{ eexists; eauto. }
congruence.
}
{ intros. simpl. rewrite /vsingle/scal//=/mult/=. rewrite /list_apply//=. nra. }
{ eauto. }
- intros i1 r' f gs dgs Hwf Hmono Himage Hderive Hex.
inversion Hwf; sigT_inj; eauto.
inversion Himage. subst; sigT_inj.
rewrite IIRInt_list_unfold_cons; last first.
{ inversion H8. subst. congruence. }
econstructor; eauto.
{ congruence. }
{ intros. destruct Hex as (v'&His); eauto.
inversion H8; subst.
inversion His; sigT_inj; subst.
assert (Hin: in_interval (x1 x) x3).
{
eapply is_interval_image_spec; eauto.
}
edestruct (H10 _ Hin) as (vsub&Hvsub).
inversion Hderive; sigT_inj.
eexists.
simpl.
rewrite /vector_mult /=.
eapply is_IIRInt_list_ext; first eauto.
{ intros. rewrite Rmult_assoc. reflexivity. }
eapply (is_IIRInt_list_scal ); eauto.
{ eapply (IH _ _ (λ y, f (cons (x1 x) y))); eauto.
{ inversion Hmono; sigT_inj; eauto. }
{ eexists; eauto. }
}
}
inversion Hderive; sigT_inj. subst.
eapply (is_IRInt_ext (λ x, (scal (x4 x) (IIRInt_list (λ xbar, f (cons (x1 x) xbar)) _)))); first eauto.
{
intros.
symmetry.
transitivity
(scal (x4 x)
(IIRInt_list (λ xbar, list_mult (list_apply v4 xbar) * f (list_apply (x1 :: v1) (x :: xbar))) (i2 :: r))).
{
rewrite -IIRInt_list_scal; eauto.
{ eapply IIRInt_list_ext; eauto.
intros. rewrite //=. rewrite Rmult_assoc. reflexivity. }
{ eexists.
eapply (IH _ _ (λ y, f (cons (x1 x) y))); eauto.
{ inversion Hmono; sigT_inj; eauto. }
{ destruct Hex as (?&His).
assert (Hin: in_interval (x1 x) x3).
{
eapply is_interval_image_spec; eauto.
}
inversion H8. subst.
inversion His; subst; sigT_inj.
edestruct H12; eauto. eexists; eauto.
}
}
}
f_equal.
eapply is_IIRInt_list_unique.
assert (Hin: in_interval (x1 x) x3).
{
eapply is_interval_image_spec; eauto.
}
eapply (IH _ _ (λ y, f (cons (x1 x) y))); eauto.
{ inversion Hmono; sigT_inj; eauto. }
{ destruct Hex as (?&His).
inversion H8. subst.
inversion His; subst; sigT_inj.
{ edestruct H12; eauto. eexists; eauto. }
}
}
inversion H8. subst.
eapply (is_IRInt_comp_noncont_strict (λ x0, IIRInt_list (λ y, f (cons x0 y)) (x5 :: v5))); eauto.
{ inversion Hmono; eauto. }
{ inversion Himage; eauto; sigT_inj; eapply H6. }
{ inversion Himage; eauto; sigT_inj; eapply H6. }
{ inversion Himage; eauto; sigT_inj; eapply H6. }
destruct Hex as (?&His). inversion His; sigT_inj. eexists; eauto.
Qed.
End IIRInt_list.