-
Notifications
You must be signed in to change notification settings - Fork 49
/
Copy pathlebesgue_measure.v
2173 lines (1940 loc) · 91 KB
/
lebesgue_measure.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
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
From mathcomp Require Import finmap fingroup perm rat.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality fsbigop.
Require Import reals ereal signed topology numfun normedtype.
From HB Require Import structures.
Require Import sequences esum measure real_interval realfun exp.
(******************************************************************************)
(* Lebesgue Measure *)
(* *)
(* This file contains a formalization of the Lebesgue measure using the *)
(* Caratheodory's theorem available in measure.v and further develops the *)
(* theory of measurable functions. *)
(* *)
(* Main reference: *)
(* - Daniel Li, Intégration et applications, 2016 *)
(* - Achim Klenke, Probability Theory 2nd edition, 2014 *)
(* *)
(* hlength A == length of the hull of the set of real numbers A *)
(* ocitv == set of open-closed intervals ]x, y] where *)
(* x and y are real numbers *)
(* lebesgue_measure == the Lebesgue measure *)
(* *)
(* ps_infty == inductive definition of the powerset *)
(* {0, {-oo}, {+oo}, {-oo,+oo}} *)
(* emeasurable G == sigma-algebra over \bar R built out of the *)
(* measurables G of a sigma-algebra over R *)
(* elebesgue_measure == the Lebesgue measure extended to \bar R *)
(* *)
(* The modules RGenOInfty, RGenInftyO, RGenCInfty, RGenOpens provide proofs *)
(* of equivalence between the sigma-algebra generated by list of intervals *)
(* and the sigma-algebras generated by open rays, closed rays, and open *)
(* intervals. *)
(* *)
(* The modules ErealGenOInfty, ErealGenCInfty, ErealGenInftyO provide proofs *)
(* of equivalence between emeasurable and the sigma-algebras generated open *)
(* rays and closed rays. *)
(* *)
(******************************************************************************)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Reserved Notation "R .-ocitv" (at level 1, format "R .-ocitv").
Reserved Notation "R .-ocitv.-measurable"
(at level 2, format "R .-ocitv.-measurable").
Section itv_semiRingOfSets.
Variable R : realType.
Implicit Types (I J K : set R).
Definition ocitv_type : Type := R.
Definition ocitv := [set `]x.1, x.2]%classic | x in [set: R * R]].
Lemma is_ocitv a b : ocitv `]a, b]%classic.
Proof. by exists (a, b); split => //=; rewrite in_itv/= andbT. Qed.
Hint Extern 0 (ocitv _) => solve [apply: is_ocitv] : core.
Lemma ocitv0 : ocitv set0.
Proof. by exists (1, 0); rewrite //= set_itv_ge ?bnd_simp//= ltr10. Qed.
Hint Resolve ocitv0 : core.
Lemma ocitvP X : ocitv X <-> X = set0 \/ exists2 x, x.1 < x.2 & X = `]x.1, x.2]%classic.
Proof.
split=> [[x _ <-]|[->//|[x xlt ->]]]//.
case: (boolP (x.1 < x.2)) => x12; first by right; exists x.
by left; rewrite set_itv_ge.
Qed.
Lemma ocitvD : semi_setD_closed ocitv.
Proof.
move=> _ _ [a _ <-] /ocitvP[|[b ltb]] ->.
rewrite setD0; exists [set `]a.1, a.2]%classic].
by split=> [//|? ->//||? ? -> ->//]; rewrite bigcup_set1.
rewrite setDE setCitv/= setIUr -!set_itvI.
rewrite /Order.meet/= /Order.meet/= /Order.join/=
?(andbF, orbF)/= ?(meetEtotal, joinEtotal).
rewrite -negb_or le_total/=; set c := minr _ _; set d := maxr _ _.
have inside : a.1 < c -> d < a.2 -> `]a.1, c] `&` `]d, a.2] = set0.
rewrite -subset0 lt_minr lt_maxl => /andP[a12 ab1] /andP[_ ba2] x /= [].
have b1a2 : b.1 <= a.2 by rewrite ltW// (lt_trans ltb).
have a1b2 : a.1 <= b.2 by rewrite ltW// (lt_trans _ ltb).
rewrite /c /d (min_idPr _)// (max_idPr _)// !in_itv /=.
move=> /andP[a1x xb1] /andP[b2x xa2].
by have := lt_le_trans b2x xb1; case: ltgtP ltb.
exists ((if a.1 < c then [set `]a.1, c]%classic] else set0) `|`
(if d < a.2 then [set `]d, a.2]%classic] else set0)); split.
- by rewrite finite_setU; do! case: ifP.
- by move=> ? []; case: ifP => ? // ->//=.
- by rewrite bigcup_setU; congr (_ `|` _);
case: ifPn => ?; rewrite ?bigcup_set1 ?bigcup_set0// set_itv_ge.
- move=> I J/=; case: ifP => //= ac; case: ifP => //= da [] // -> []// ->.
by rewrite inside// => -[].
by rewrite setIC inside// => -[].
Qed.
Lemma ocitvI : setI_closed ocitv.
Proof.
move=> _ _ [a _ <-] [b _ <-]; rewrite -set_itvI/=.
rewrite /Order.meet/= /Order.meet /Order.join/=
?(andbF, orbF)/= ?(meetEtotal, joinEtotal).
by rewrite -negb_or le_total/=.
Qed.
Definition ocitv_display : Type -> measure_display. Proof. exact. Qed.
HB.instance Definition _ :=
@isSemiRingOfSets.Build (ocitv_display R)
ocitv_type (Pointed.class R) ocitv ocitv0 ocitvI ocitvD.
Notation "R .-ocitv" := (ocitv_display R) : measure_display_scope.
Notation "R .-ocitv.-measurable" := (measurable : set (set (ocitv_type))) :
classical_set_scope.
Section hlength.
Local Open Scope ereal_scope.
Implicit Types i j : interval R.
Definition hlength (A : set ocitv_type) : \bar R := let i := Rhull A in i.2 - i.1.
Lemma hlength0 : hlength (set0 : set R) = 0.
Proof. by rewrite /hlength Rhull0 /= subee. Qed.
Lemma hlength_singleton (r : R) : hlength `[r, r] = 0.
Proof.
rewrite /hlength /= asboolT// sup_itvcc//= asboolT//.
by rewrite asboolT inf_itvcc//= ?subee// inE.
Qed.
Lemma hlength_setT : hlength setT = +oo%E :> \bar R.
Proof. by rewrite /hlength RhullT. Qed.
Lemma hlength_itv i : hlength [set` i] = if i.2 > i.1 then i.2 - i.1 else 0.
Proof.
case: ltP => [/lt_ereal_bnd/neitvP i12|]; first by rewrite /hlength set_itvK.
rewrite le_eqVlt => /orP[|/lt_ereal_bnd i12]; last first.
rewrite (_ : [set` i] = set0) ?hlength0//.
by apply/eqP/negPn; rewrite -/(neitv _) neitvE -leNgt (ltW i12).
case: i => -[ba a|[|]] [bb b|[|]] //=.
- rewrite /= => /eqP[->{b}]; move: ba bb => -[] []; try
by rewrite set_itvE hlength0.
by rewrite hlength_singleton.
- by move=> _; rewrite set_itvE hlength0.
- by move=> _; rewrite set_itvE hlength0.
Qed.
Lemma hlength_finite_fin_num i : neitv i -> hlength [set` i] < +oo ->
((i.1 : \bar R) \is a fin_num) /\ ((i.2 : \bar R) \is a fin_num).
Proof.
move: i => [[ba a|[]] [bb b|[]]] /neitvP //=; do ?by rewrite ?set_itvE ?eqxx.
by move=> _; rewrite hlength_itv /= ltry.
by move=> _; rewrite hlength_itv /= ltNyr.
by move=> _; rewrite hlength_itv.
Qed.
Lemma finite_hlengthE i : neitv i -> hlength [set` i] < +oo ->
hlength [set` i] = (fine i.2)%:E - (fine i.1)%:E.
Proof.
move=> i0 ioo; have [ri1 ri2] := hlength_finite_fin_num i0 ioo.
rewrite !fineK// hlength_itv; case: ifPn => //.
rewrite -leNgt le_eqVlt => /predU1P[->|]; first by rewrite subee.
by move/lt_ereal_bnd/ltW; rewrite leNgt; move: i0 => /neitvP => ->.
Qed.
Lemma hlength_infty_bnd b r :
hlength [set` Interval -oo%O (BSide b r)] = +oo :> \bar R.
Proof. by rewrite hlength_itv /= ltNyr. Qed.
Lemma hlength_bnd_infty b r :
hlength [set` Interval (BSide b r) +oo%O] = +oo :> \bar R.
Proof. by rewrite hlength_itv /= ltry. Qed.
Lemma pinfty_hlength i : hlength [set` i] = +oo ->
(exists s r, i = Interval -oo%O (BSide s r) \/ i = Interval (BSide s r) +oo%O)
\/ i = `]-oo, +oo[.
Proof.
rewrite hlength_itv; case: i => -[ba a|[]] [bb b|[]] //= => [|_|_|].
- by case: ifPn.
- by left; exists ba, a; right.
- by left; exists bb, b; left.
- by right.
Qed.
Lemma hlength_itv_ge0 i : 0 <= hlength [set` i].
Proof.
rewrite hlength_itv; case: ifPn => //; case: (i.1 : \bar _) => [r| |].
- by rewrite suber_ge0//; exact: ltW.
- by rewrite ltNge leey.
- by case: (i.2 : \bar _) => //= [r _]; rewrite leey.
Qed.
Lemma hlength_Rhull (A : set R) : hlength [set` Rhull A] = hlength A.
Proof. by rewrite /hlength Rhull_involutive. Qed.
Lemma le_hlength_itv i j : {subset i <= j} -> hlength [set` i] <= hlength [set` j].
Proof.
set I := [set` i]; set J := [set` j].
have [->|/set0P I0] := eqVneq I set0; first by rewrite hlength0 hlength_itv_ge0.
have [J0|/set0P J0] := eqVneq J set0.
by move/subset_itvP; rewrite -/J J0 subset0 -/I => ->.
move=> /subset_itvP ij; apply: lee_sub => /=.
have [ui|ui] := asboolP (has_ubound I).
have [uj /=|uj] := asboolP (has_ubound J); last by rewrite leey.
by rewrite lee_fin le_sup // => r Ir; exists r; split => //; apply: ij.
have [uj /=|//] := asboolP (has_ubound J).
by move: ui; have := subset_has_ubound ij uj.
have [lj /=|lj] := asboolP (has_lbound J); last by rewrite leNye.
have [li /=|li] := asboolP (has_lbound I); last first.
by move: li; have := subset_has_lbound ij lj.
rewrite lee_fin ler_oppl opprK le_sup// ?has_inf_supN//; last exact/nonemptyN.
move=> r [r' Ir' <-{r}]; exists (- r')%R.
by split => //; exists r' => //; apply: ij.
Qed.
Lemma le_hlength : {homo hlength : A B / (A `<=` B) >-> A <= B}.
Proof.
move=> a b /le_Rhull /le_hlength_itv.
by rewrite (hlength_Rhull a) (hlength_Rhull b).
Qed.
Lemma hlength_ge0 I : (0 <= hlength I)%E.
Proof. by rewrite -hlength0 le_hlength. Qed.
End hlength.
#[local] Hint Extern 0 (0%:E <= hlength _) => solve[apply: hlength_ge0] : core.
(* Unused *)
(* Lemma hlength_semi_additive2 : semi_additive2 hlength. *)
(* Proof. *)
(* move=> I J /ocitvP[|[a a12]] ->; first by rewrite set0U hlength0 add0e. *)
(* move=> /ocitvP[|[b b12]] ->; first by rewrite setU0 hlength0 adde0. *)
(* rewrite -subset0 => + ab0 => /ocitvP[|[x x12] abx]. *)
(* by rewrite setU_eq0 => -[-> ->]; rewrite setU0 hlength0 adde0. *)
(* rewrite abx !hlength_itv//= ?lte_fin a12 b12 x12/= -!EFinB -EFinD. *)
(* wlog ab1 : a a12 b b12 ab0 abx / a.1 <= b.1 => [hwlog|]. *)
(* have /orP[ab1|ba1] := le_total a.1 b.1; first by apply: hwlog. *)
(* by rewrite [in RHS]addrC; apply: hwlog => //; rewrite (setIC, setUC). *)
(* have := ab0; rewrite subset0 -set_itv_meet/=. *)
(* rewrite /Order.join /Order.meet/= ?(andbF, orbF)/= ?(meetEtotal, joinEtotal). *)
(* rewrite -negb_or le_total/=; set c := minr _ _; set d := maxr _ _. *)
(* move=> /eqP/neitvP/=; rewrite bnd_simp/= /d/c (max_idPr _)// => /negP. *)
(* rewrite -leNgt le_minl orbC lt_geF//= => {c} {d} a2b1. *)
(* have ab i j : i \in `]a.1, a.2] -> j \in `]b.1, b.2] -> i <= j. *)
(* by move=> ia jb; rewrite (le_le_trans _ _ a2b1) ?(itvP ia) ?(itvP jb). *)
(* have /(congr1 sup) := abx; rewrite sup_setU// ?sup_itv_bounded// => bx. *)
(* have /(congr1 inf) := abx; rewrite inf_setU// ?inf_itv_bounded// => ax. *)
(* rewrite -{}ax -{x}bx in abx x12 *. *)
(* case: ltgtP a2b1 => // a2b1 _; last first. *)
(* by rewrite a2b1 [in RHS]addrC subrKA. *)
(* exfalso; pose c := (a.2 + b.1) / 2%:R. *)
(* have /predeqP/(_ c)[_ /(_ _)/Box[]] := abx. *)
(* apply: subset_itv_oo_oc; have := mid_in_itvoo a2b1. *)
(* by apply/subitvP; rewrite subitvE ?bnd_simp/= ?ltW. *)
(* apply/not_orP; rewrite /= !in_itv/=. *)
(* by rewrite lt_geF ?midf_lt//= andbF le_gtF ?midf_le//= ltW. *)
(* Qed. *)
Lemma hlength_semi_additive : semi_additive hlength.
Proof.
move=> /= I n /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym-/funext {I}->.
move=> Itriv [[/= a1 a2] _] /esym /[dup] + ->.
rewrite hlength_itv ?lte_fin/= -EFinB.
case: ifPn => a12; last first.
pose I i := `](b i).1, (b i).2]%classic.
rewrite set_itv_ge//= -(bigcup_mkord _ I) /I => /bigcup0P I0.
by under eq_bigr => i _ do rewrite I0//= hlength0; rewrite big1.
set A := `]a1, a2]%classic.
rewrite -bigcup_pred; set P := xpredT; rewrite (eq_bigl P)//.
move: P => P; have [p] := ubnP #|P|; elim: p => // p IHp in P a2 a12 A *.
rewrite ltnS => cP /esym AE.
have : A a2 by rewrite /A /= in_itv/= lexx andbT.
rewrite AE/= => -[i /= Pi] a2bi.
case: (boolP ((b i).1 < (b i).2)) => bi; last by rewrite itv_ge in a2bi.
have {}a2bi : a2 = (b i).2.
apply/eqP; rewrite eq_le (itvP a2bi)/=.
suff: A (b i).2 by move=> /itvP->.
by rewrite AE; exists i=> //=; rewrite in_itv/= lexx andbT.
rewrite {a2}a2bi in a12 A AE *.
rewrite (bigD1 i)//= hlength_itv ?lte_fin/= bi !EFinD -addeA.
congr (_ + _)%E; apply/eqP; rewrite addeC -sube_eq// 1?adde_defC//.
rewrite ?EFinN oppeK addeC; apply/eqP.
case: (eqVneq a1 (b i).1) => a1bi.
rewrite {a1}a1bi in a12 A AE {IHp} *; rewrite subee ?big1// => j.
move=> /andP[Pj Nji]; rewrite hlength_itv ?lte_fin/=; case: ifPn => bj//.
exfalso; have /trivIsetP/(_ j i I I Nji) := Itriv.
pose m := ((b j).1 + (b j).2) / 2%:R.
have mbj : `](b j).1, (b j).2]%classic m.
by rewrite /= !in_itv/= ?(midf_lt, midf_le)//= ltW.
rewrite -subset0 => /(_ m); apply; split=> //.
by suff: A m by []; rewrite AE; exists j => //.
have a1b2 j : P j -> (b j).1 < (b j).2 -> a1 <= (b j).2.
move=> Pj bj; suff /itvP-> : A (b j).2 by [].
by rewrite AE; exists j => //=; rewrite ?in_itv/= bj//=.
have a1b j : P j -> (b j).1 < (b j).2 -> a1 <= (b j).1.
move=> Pj bj; case: ltP=> // bj1a.
suff : A a1 by rewrite /A/= in_itv/= ltxx.
by rewrite AE; exists j; rewrite //= in_itv/= bj1a//= a1b2.
have bbi2 j : P j -> (b j).1 < (b j).2 -> (b j).2 <= (b i).2.
move=> Pj bj; suff /itvP-> : A (b j).2 by [].
by rewrite AE; exists j => //=; rewrite ?in_itv/= bj//=.
apply/IHp.
- by rewrite lt_neqAle a1bi/= a1b.
- rewrite (leq_trans _ cP)// -(cardID (pred1 i) P).
rewrite [X in (_ < X + _)%N](@eq_card _ _ (pred1 i)); last first.
by move=> j; rewrite !inE andbC; case: eqVneq => // ->.
rewrite ?card1 ?ltnS// subset_leq_card//.
by apply/fintype.subsetP => j; rewrite -topredE/= !inE andbC.
apply/seteqP; split=> /= [x [j/= /andP[Pj Nji]]|x/= xabi].
case: (boolP ((b j).1 < (b j).2)) => bj; last by rewrite itv_ge.
apply: subitvP; rewrite subitvE ?bnd_simp a1b//= leNgt.
have /trivIsetP/(_ j i I I Nji) := Itriv.
rewrite -subset0 => /(_ (b j).2); apply: contra_notN => /= bi1j2.
by rewrite !in_itv/= bj !lexx bi1j2 bbi2.
have: A x.
rewrite /A/= in_itv/= (itvP xabi)/= ltW//.
by rewrite (le_lt_trans _ bi) ?(itvP xabi).
rewrite AE => -[j /= Pj xbj].
exists j => //=.
apply/andP; split=> //; apply: contraTneq xbj => ->.
by rewrite in_itv/= le_gtF// (itvP xabi).
Qed.
HB.instance Definition _ := isContent.Build _ _ R
hlength hlength_ge0 hlength_semi_additive.
Hint Extern 0 ((_ .-ocitv).-measurable _) => solve [apply: is_ocitv] : core.
Lemma hlength_sigma_sub_additive :
sigma_sub_additive (hlength : set ocitv_type -> _).
Proof.
move=> I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE.
move=> [a _ <-]; rewrite hlength_itv ?lte_fin/= -EFinB => lebig.
case: ifPn => a12; last by rewrite nneseries_esum// esum_ge0.
apply/lee_addgt0Pr => _ /posnumP[e].
rewrite [e%:num]splitr [in leRHS]EFinD addeA -lee_subl_addr//.
apply: le_trans (epsilon_trick _ _ _) => //=.
have eVn_gt0 n : 0 < e%:num / 2 / (2 ^ n.+1)%:R.
by rewrite divr_gt0// ltr0n// expn_gt0.
have eVn_ge0 n := ltW (eVn_gt0 n).
pose Aoo i : set ocitv_type :=
`](b i).1, (b i).2 + e%:num / 2 / (2 ^ i.+1)%:R[%classic.
pose Aoc i : set ocitv_type :=
`](b i).1, (b i).2 + e%:num / 2 / (2 ^ i.+1)%:R]%classic.
have: `[a.1 + e%:num / 2, a.2] `<=` \bigcup_i Aoo i.
apply: (@subset_trans _ `]a.1, a.2]).
move=> x; rewrite /= !in_itv /= => /andP[+ -> //].
by move=> /lt_le_trans-> //; rewrite ltr_addl.
apply: (subset_trans lebig); apply: subset_bigcup => i _; rewrite AE /Aoo/=.
move=> x /=; rewrite !in_itv /= => /andP[-> /le_lt_trans->]//=.
by rewrite ltr_addl.
have := @segment_compact _ (a.1 + e%:num / 2) a.2; rewrite compact_cover.
move=> /[apply]-[i _|X _ Xc]; first exact: interval_open.
have: `](a.1 + e%:num / 2), a.2] `<=` \bigcup_(i in [set` X]) Aoc i.
move=> x /subset_itv_oc_cc /Xc [i /= Xi] Aooix.
by exists i => //; apply: subset_itv_oo_oc Aooix.
have /[apply] := @content_sub_fsum _ _ _
[the content _ _ of hlength : set ocitv_type -> _] _ [set` X].
move=> /(_ _ _ _)/Box[]//=; apply: le_le_trans.
rewrite hlength_itv ?lte_fin -?EFinD/= -addrA -opprD.
by case: ltP => //; rewrite lee_fin subr_le0.
rewrite nneseries_esum//; last by move=> *; rewrite adde_ge0//= ?lee_fin.
rewrite esum_ge//; exists [set` X] => //; rewrite fsbig_finite// ?set_fsetK//=.
rewrite fsbig_finite//= set_fsetK//.
rewrite lee_sum // => i _; rewrite ?AE// !hlength_itv/= ?lte_fin -?EFinD/=.
do !case: ifPn => //= ?; do ?by rewrite ?adde_ge0 ?lee_fin// ?subr_ge0// ?ltW.
by rewrite addrAC.
by rewrite addrAC lee_fin ler_add// subr_le0 leNgt.
Qed.
HB.instance Definition _ := Content_SubSigmaAdditive_isMeasure.Build _ _ _
hlength hlength_sigma_sub_additive.
Lemma hlength_sigma_finite : sigma_finite setT (hlength : set ocitv_type -> _).
Proof.
exists (fun k : nat => `] (- k%:R)%R, k%:R]%classic); first by rewrite bigcup_itvT.
by move=> k; split => //; rewrite hlength_itv/= -EFinB; case: ifP; rewrite ltry.
Qed.
Definition lebesgue_measure := measure_extension [the measure _ _ of hlength].
HB.instance Definition _ := Measure.on lebesgue_measure.
(* TODO: this ought to be turned into a Let but older version of mathcomp/coq
does not seem to allow, try to change asap *)
Local Lemma sigmaT_finite_lebesgue_measure : sigma_finite setT lebesgue_measure.
Proof. exact/measure_extension_sigma_finite/hlength_sigma_finite. Qed.
HB.instance Definition _ := @isSigmaFinite.Build _ _ _
lebesgue_measure sigmaT_finite_lebesgue_measure.
End itv_semiRingOfSets.
Arguments hlength {R}.
#[global] Hint Extern 0 (0%:E <= hlength _) => solve[apply: hlength_ge0] : core.
Arguments lebesgue_measure {R}.
Notation "R .-ocitv" := (ocitv_display R) : measure_display_scope.
Notation "R .-ocitv.-measurable" := (measurable : set (set (ocitv_type R))) :
classical_set_scope.
Section lebesgue_measure.
Variable R : realType.
Let gitvs := [the measurableType _ of salgebraType (@ocitv R)].
Lemma lebesgue_measure_unique (mu : {measure set gitvs -> \bar R}) :
(forall X, ocitv X -> hlength X = mu X) ->
forall X, measurable X -> lebesgue_measure X = mu X.
Proof.
move=> muE X mX; apply: measure_extension_unique => //.
exact: hlength_sigma_finite.
Qed.
End lebesgue_measure.
Section ps_infty.
Context {T : Type}.
Local Open Scope ereal_scope.
Inductive ps_infty : set \bar T -> Prop :=
| ps_infty0 : ps_infty set0
| ps_ninfty : ps_infty [set -oo]
| ps_pinfty : ps_infty [set +oo]
| ps_inftys : ps_infty [set -oo; +oo].
Lemma ps_inftyP (A : set \bar T) : ps_infty A <-> A `<=` [set -oo; +oo].
Proof.
split => [[]//|Aoo].
by have [] := subset_set2 Aoo; move=> ->; constructor.
Qed.
Lemma setCU_Efin (A : set T) (B : set \bar T) : ps_infty B ->
~` (EFin @` A) `&` ~` B = (EFin @` ~` A) `|` ([set -oo%E; +oo%E] `&` ~` B).
Proof.
move=> ps_inftyB.
have -> : ~` (EFin @` A) = EFin @` (~` A) `|` [set -oo; +oo]%E.
by rewrite EFin_setC setDKU // => x [|] -> -[].
rewrite setIUl; congr (_ `|` _); rewrite predeqE => -[x| |]; split; try by case.
by move=> [] x' Ax' [] <-{x}; split; [exists x'|case: ps_inftyB => // -[]].
Qed.
End ps_infty.
Section salgebra_ereal.
Variables (R : realType) (G : set (set R)).
Let measurableR : set (set R) := G.-sigma.-measurable.
Definition emeasurable : set (set \bar R) :=
[set EFin @` A `|` B | A in measurableR & B in ps_infty].
Lemma emeasurable0 : emeasurable set0.
Proof.
exists set0; first exact: measurable0.
by exists set0; rewrite ?setU0// ?image_set0//; constructor.
Qed.
Lemma emeasurableC (X : set \bar R) : emeasurable X -> emeasurable (~` X).
Proof.
move => -[A mA] [B PooB <-]; rewrite setCU setCU_Efin //.
exists (~` A); [exact: measurableC | exists ([set -oo%E; +oo%E] `&` ~` B) => //].
case: PooB.
- by rewrite setC0 setIT; constructor.
- rewrite setIUl setICr set0U -setDE.
have [_ ->] := @setDidPl (\bar R) [set +oo%E] [set -oo%E]; first by constructor.
by rewrite predeqE => x; split => // -[->].
- rewrite setIUl setICr setU0 -setDE.
have [_ ->] := @setDidPl (\bar R) [set -oo%E] [set +oo%E]; first by constructor.
by rewrite predeqE => x; split => // -[->].
- by rewrite setICr; constructor.
Qed.
Lemma bigcupT_emeasurable (F : (set \bar R)^nat) :
(forall i, emeasurable (F i)) -> emeasurable (\bigcup_i (F i)).
Proof.
move=> mF; pose P := fun i j => measurableR j.1 /\ ps_infty j.2 /\
F i = [set x%:E | x in j.1] `|` j.2.
have [f fi] : {f : nat -> (set R) * (set \bar R) & forall i, P i (f i) }.
by apply: choice => i; have [x mx [y PSoo'y] xy] := mF i; exists (x, y).
exists (\bigcup_i (f i).1).
by apply: bigcupT_measurable => i; exact: (fi i).1.
exists (\bigcup_i (f i).2).
apply/ps_inftyP => x [n _] fn2x.
have /ps_inftyP : ps_infty(f n).2 by have [_ []] := fi n.
exact.
rewrite [RHS](@eq_bigcupr _ _ _ _
(fun i => [set x%:E | x in (f i).1] `|` (f i).2)); last first.
by move=> i; have [_ []] := fi i.
rewrite bigcupU; congr (_ `|` _).
rewrite predeqE => i /=; split=> [[r [n _ fn1r <-{i}]]|[n _ [r fn1r <-{i}]]];
by [exists n => //; exists r | exists r => //; exists n].
Qed.
Definition ereal_isMeasurable :
isMeasurable default_measure_display (\bar R) :=
isMeasurable.Build _ _ (Pointed.class _)
emeasurable0 emeasurableC bigcupT_emeasurable.
End salgebra_ereal.
Section puncture_ereal_itv.
Variable R : realDomainType.
Implicit Types (y : R) (b : bool).
Local Open Scope ereal_scope.
Lemma punct_eitv_bndy b y : [set` Interval (BSide b y%:E) +oo%O] =
EFin @` [set` Interval (BSide b y) +oo%O] `|` [set +oo].
Proof.
rewrite predeqE => x; split; rewrite /= in_itv andbT.
- move: x => [x| |] yxb; [|by right|by case: b yxb].
by left; exists x => //; rewrite in_itv /= andbT; case: b yxb.
- move=> [[r]|->].
+ by rewrite in_itv /= andbT => yxb <-; case: b yxb.
+ by case: b => /=; rewrite ?(ltry, leey).
Qed.
Lemma punct_eitv_Nybnd b y : [set` Interval -oo%O (BSide b y%:E)] =
[set -oo%E] `|` EFin @` [set x | x \in Interval -oo%O (BSide b y)].
Proof.
rewrite predeqE => x; split; rewrite /= in_itv.
- move: x => [x| |] yxb; [|by case: b yxb|by left].
by right; exists x => //; rewrite in_itv /= andbT; case: b yxb.
- move=> [->|[r]].
+ by case: b => /=; rewrite ?(ltNyr, leNye).
+ by rewrite in_itv /= => yxb <-; case: b yxb.
Qed.
Lemma punct_eitv_setTR : range (@EFin R) `|` [set +oo] = [set~ -oo].
Proof.
rewrite eqEsubset; split => [a [[a' _ <-]|->]|] //.
by move=> [x| |] //= _; [left; exists x|right].
Qed.
Lemma punct_eitv_setTL : range (@EFin R) `|` [set -oo] = [set~ +oo].
Proof.
rewrite eqEsubset; split => [a [[a' _ <-]|->]|] //.
by move=> [x| |] //= _; [left; exists x|right].
Qed.
End puncture_ereal_itv.
Section salgebra_R_ssets.
Variable R : realType.
Definition measurableTypeR := salgebraType (R.-ocitv.-measurable).
Definition measurableR : set (set R) :=
(R.-ocitv.-measurable).-sigma.-measurable.
HB.instance Definition R_isMeasurable :
isMeasurable default_measure_display R :=
@isMeasurable.Build _ measurableTypeR (Pointed.class R) measurableR
measurable0 (@measurableC _ _) (@bigcupT_measurable _ _).
(*HB.instance (Real.sort R) R_isMeasurable.*)
Lemma measurable_set1 (r : R) : measurable [set r].
Proof.
rewrite set1_bigcap_oc; apply: bigcap_measurable => k // _.
by apply: sub_sigma_algebra; exact/is_ocitv.
Qed.
#[local] Hint Resolve measurable_set1 : core.
Lemma measurable_itv (i : interval R) : measurable [set` i].
Proof.
have moc (a b : R) : measurable `]a, b]%classic.
by apply: sub_sigma_algebra; apply: is_ocitv.
have mopoo (x : R) : measurable `]x, +oo[%classic.
by rewrite itv_bnd_infty_bigcup; exact: bigcup_measurable.
have mnooc (x : R) : measurable `]-oo, x]%classic.
by rewrite -setCitvr; exact/measurableC.
have ooE (a b : R) : `]a, b[%classic = `]a, b]%classic `\ b.
case: (boolP (a < b)) => ab; last by rewrite !set_itv_ge ?set0D.
by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx andbF.
have moo (a b : R) : measurable `]a, b[%classic.
by rewrite ooE; exact: measurableD.
have mcc (a b : R) : measurable `[a, b]%classic.
case: (boolP (a <= b)) => ab; last by rewrite set_itv_ge.
by rewrite -setU1itv//; apply/measurableU.
have mco (a b : R) : measurable `[a, b[%classic.
case: (boolP (a < b)) => ab; last by rewrite set_itv_ge.
by rewrite -setU1itv//; apply/measurableU.
have oooE (b : R) : `]-oo, b[%classic = `]-oo, b]%classic `\ b.
by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx.
case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge.
- by rewrite -setU1itv//; exact/measurableU.
- by rewrite oooE; exact/measurableD.
- by rewrite set_itv_infty_infty.
Qed.
HB.instance Definition _ :=
(ereal_isMeasurable (R.-ocitv.-measurable)).
(* NB: Until we dropped support for Coq 8.12, we were using
HB.instance (\bar (Real.sort R))
(ereal_isMeasurable (@measurable (@itvs_semiRingOfSets R))).
This was producing a warning but the alternative was failing with Coq 8.12 with
the following message (according to the CI):
# [redundant-canonical-projection,typechecker]
# forall (T : measurableType) (f : T -> R), measurable_fun setT f
# : Prop
# File "./theories/lebesgue_measure.v", line 4508, characters 0-88:
# Error: Anomaly "Uncaught exception Failure("sep_last")."
# Please report at http://coq.inria.fr/bugs/.
*)
Lemma measurable_image_EFin (A : set R) : measurableR A -> measurable (EFin @` A).
Proof.
by move=> mA; exists A => //; exists set0; [constructor|rewrite setU0].
Qed.
Lemma emeasurable_set1 (x : \bar R) : measurable [set x].
Proof.
case: x => [r| |].
- by rewrite -image_set1; apply: measurable_image_EFin; apply: measurable_set1.
- exists set0 => //; [exists [set +oo%E]; [by constructor|]].
by rewrite image_set0 set0U.
- exists set0 => //; [exists [set -oo%E]; [by constructor|]].
by rewrite image_set0 set0U.
Qed.
#[local] Hint Resolve emeasurable_set1 : core.
Lemma __deprecated__itv_cpinfty_pinfty : `[+oo%E, +oo[%classic = [set +oo%E] :> set (\bar R).
Proof. by rewrite itv_cyy. Qed.
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_cyy`")]
Notation itv_cpinfty_pinfty := __deprecated__itv_cpinfty_pinfty.
Lemma __deprecated__itv_opinfty_pinfty : `]+oo%E, +oo[%classic = set0 :> set (\bar R).
Proof. by rewrite itv_oyy. Qed.
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_oyy`")]
Notation itv_opinfty_pinfty := __deprecated__itv_opinfty_pinfty.
Lemma __deprecated__itv_cninfty_pinfty : `[-oo%E, +oo[%classic = setT :> set (\bar R).
Proof. by rewrite itv_cNyy. Qed.
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_cNyy`")]
Notation itv_cninfty_pinfty := __deprecated__itv_cninfty_pinfty.
Lemma __deprecated__itv_oninfty_pinfty :
`]-oo%E, +oo[%classic = ~` [set -oo]%E :> set (\bar R).
Proof. by rewrite itv_oNyy. Qed.
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_oNyy`")]
Notation itv_oninfty_pinfty := __deprecated__itv_oninfty_pinfty.
Let emeasurable_itv_bndy b (y : \bar R) :
measurable [set` Interval (BSide b y) +oo%O].
Proof.
move: y => [y| |].
- exists [set` Interval (BSide b y) +oo%O]; first exact: measurable_itv.
by exists [set +oo%E]; [constructor|rewrite -punct_eitv_bndy].
- by case: b; rewrite ?itv_oyy ?itv_cyy.
- case: b; first by rewrite itv_cNyy.
by rewrite itv_oNyy; exact/measurableC.
Qed.
Let emeasurable_itv_Nybnd b (y : \bar R) :
measurable [set` Interval -oo%O (BSide b y)].
Proof. by rewrite -setCitvr; exact/measurableC/emeasurable_itv_bndy. Qed.
Lemma emeasurable_itv (i : interval (\bar R)) :
measurable ([set` i]%classic : set \bar R).
Proof.
rewrite -[X in measurable X]setCK; apply: measurableC.
rewrite set_interval.setCitv /=; apply: measurableU => [|].
- by move: i => [[b1 i1|[|]] i2] /=; rewrite ?set_interval.set_itvE.
- by move: i => [i1 [b2 i2|[|]]] /=; rewrite ?set_interval.set_itvE.
Qed.
Definition elebesgue_measure : set \bar R -> \bar R :=
fun S => lebesgue_measure (fine @` (S `\` [set -oo; +oo]%E)).
Lemma elebesgue_measure0 : elebesgue_measure set0 = 0%E.
Proof. by rewrite /elebesgue_measure set0D image_set0 measure0. Qed.
Lemma measurable_image_fine (X : set \bar R) : measurable X ->
measurable [set fine x | x in X `\` [set -oo; +oo]%E].
Proof.
case => Y mY [X' [ | <-{X} | <-{X} | <-{X} ]].
- rewrite setU0 => <-{X}.
rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split.
by move=> [x [[x' Yx' <-{x}/= _ <-//]]].
by move=> Yr; exists r%:E; split => [|[]//]; exists r.
- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split.
move=> [x [[[x' Yx' <- _ <-//]|]]].
by move=> <-; rewrite not_orP => -[]/(_ erefl).
by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r.
- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split.
move=> [x [[[x' Yx' <-{x} _ <-//]|]]].
by move=> ->; rewrite not_orP => -[_]/(_ erefl).
by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r.
- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split.
by rewrite setDUl setDv setU0 => -[_ [[x' Yx' <-]] _ <-].
by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r.
Qed.
Lemma elebesgue_measure_ge0 X : (0 <= elebesgue_measure X)%E.
Proof. exact/measure_ge0. Qed.
Lemma semi_sigma_additive_elebesgue_measure :
semi_sigma_additive elebesgue_measure.
Proof.
move=> /= F mF tF mUF; rewrite /elebesgue_measure.
rewrite [X in lebesgue_measure X](_ : _ =
\bigcup_n (fine @` (F n `\` [set -oo; +oo]%E))); last first.
rewrite predeqE => r; split.
by move=> [x [[n _ Fnx xoo <-]]]; exists n => //; exists x.
by move=> [n _ [x [Fnx xoo <-{r}]]]; exists x => //; split => //; exists n.
apply: (@measure_semi_sigma_additive _ _ _ [the measure _ _ of (@lebesgue_measure R)]
(fun n => fine @` (F n `\` [set -oo; +oo]%E))).
- move=> n; have := mF n.
move=> [X mX [X' mX']] XX'Fn.
apply: measurable_image_fine.
rewrite -XX'Fn.
apply: measurableU; first exact: measurable_image_EFin.
by case: mX' => //; exact: measurableU.
- move=> i j _ _ [x [[a [Fia aoo ax] [b [Fjb boo] bx]]]].
move: tF => /(_ i j Logic.I Logic.I); apply.
suff ab : a = b by exists a; split => //; rewrite ab.
move: a b {Fia Fjb} aoo boo ax bx.
move=> [a| |] [b| |] /=.
+ by move=> _ _ -> ->.
+ by move=> _; rewrite not_orP => -[_]/(_ erefl).
+ by move=> _; rewrite not_orP => -[]/(_ erefl).
+ by rewrite not_orP => -[_]/(_ erefl).
+ by rewrite not_orP => -[_]/(_ erefl).
+ by rewrite not_orP => -[_]/(_ erefl).
+ by rewrite not_orP => -[]/(_ erefl).
+ by rewrite not_orP => -[]/(_ erefl).
+ by rewrite not_orP => -[]/(_ erefl).
- move: mUF.
rewrite {1}/measurable /emeasurable /= => -[X mX [Y []]] {Y}.
- rewrite setU0 => h.
rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr].
move=> -[n _ [x [Fnx xoo <-{r}]]].
have : (\bigcup_n F n) x by exists n.
by rewrite -h => -[x' Xx' <-].
have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; exists r.
by exists n => //; exists r%:E => //; split => //; case.
- move=> h.
rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr].
move=> -[n _ [x [Fnx xoo <-]]].
have : (\bigcup_n F n) x by exists n.
by rewrite -h => -[[x' Xx' <-//]|xoo']; move/not_orP : xoo => -[].
have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r.
by exists n => //; exists r%:E => //; split => //; case.
- (* NB: almost the same as the previous one, factorize?*)
move=> h.
rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr].
move=> -[n _ [x [Fnx xoo <-]]].
have : (\bigcup_n F n) x by exists n.
by rewrite -h => -[[x' Xx' <-//]|xoo']; move/not_orP : xoo => -[].
have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r.
by exists n => //; exists r%:E => //; split => //; case.
- move=> h.
rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr].
move=> -[n _ [x [Fnx xoo <-]]].
have : (\bigcup_n F n) x by exists n.
by rewrite -h => -[[x' Xx' <-//]|].
have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r.
by exists n => //; exists r%:E => //; split => //; case.
Qed.
HB.instance Definition _ := isMeasure.Build _ _ _ elebesgue_measure
elebesgue_measure0 elebesgue_measure_ge0
semi_sigma_additive_elebesgue_measure.
End salgebra_R_ssets.
#[global]
Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1|
apply: emeasurable_set1] : core.
#[global]
Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core.
#[deprecated(since="mathcomp-analysis 0.6.2", note="use `emeasurable_itv` instead")]
Notation emeasurable_itv_bnd_pinfty := emeasurable_itv.
#[deprecated(since="mathcomp-analysis 0.6.2", note="use `emeasurable_itv` instead")]
Notation emeasurable_itv_ninfty_bnd := emeasurable_itv.
Lemma measurable_fine (R : realType) (D : set (\bar R)) : measurable D ->
measurable_fun D fine.
Proof.
move=> mD _ /= B mB; rewrite [X in measurable X](_ : _ `&` _ = if 0%R \in B then
D `&` ((EFin @` B) `|` [set -oo; +oo]%E) else D `&` EFin @` B); last first.
apply/seteqP; split=> [[r [Dr Br]|[Doo B0]|[Doo B0]]|[r| |]].
- by case: ifPn => _; split => //; left; exists r.
- by rewrite mem_set//; split => //; right; right.
- by rewrite mem_set//; split => //; right; left.
- by case: ifPn => [_ [Dr [[s + [sr]]|[]//]]|_ [Dr [s + [sr]]]]; rewrite sr.
- by case: ifPn => [/[!inE] B0 [Doo [[]//|]] [//|_]|B0 [Doo//] []].
- by case: ifPn => [/[!inE] B0 [Doo [[]//|]] [//|_]|B0 [Doo//] []].
case: ifPn => B0; apply/measurableI => //; last exact: measurable_image_EFin.
by apply: measurableU; [exact: measurable_image_EFin|exact: measurableU].
Qed.
#[global] Hint Extern 0 (measurable_fun _ fine) =>
solve [exact: measurable_fine] : core.
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_fine` instead")]
Notation measurable_fun_fine := measurable_fine.
Section lebesgue_measure_itv.
Variable R : realType.
Let lebesgue_measure_itvoc (a b : R) :
(lebesgue_measure (`]a, b] : set R) = hlength `]a, b])%classic.
Proof.
rewrite /lebesgue_measure/= /measure_extension measurable_mu_extE//.
by exists (a, b).
Qed.
Let lebesgue_measure_itvoo_subr1 (a : R) :
lebesgue_measure (`]a - 1, a[%classic : set R) = 1%E.
Proof.
rewrite itv_bnd_open_bigcup//; transitivity (lim (lebesgue_measure \o
(fun k => `]a - 1, a - k.+1%:R^-1]%classic : set R))).
apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu.
- by move=> ?; exact: measurable_itv.
- by apply: bigcup_measurable => k _; exact: measurable_itv.
- move=> n m nm; apply/subsetPset => x /=; rewrite !in_itv/= => /andP[->/=].
by move/le_trans; apply; rewrite ler_sub// ler_pinv ?ler_nat//;
rewrite inE ltr0n andbT unitfE.
rewrite (_ : _ \o _ = (fun n => (1 - n.+1%:R^-1)%:E)); last first.
apply/funext => n /=; rewrite lebesgue_measure_itvoc.
have [->|n0] := eqVneq n 0%N; first by rewrite invr1 subrr set_itvoc0.
rewrite hlength_itv/= lte_fin ifT; last first.
by rewrite ler_lt_sub// invr_lt1 ?unitfE// ltr1n ltnS lt0n.
by rewrite !(EFinB,EFinN) fin_num_oppeB// addeAC addeA subee// add0e.
apply/cvg_lim => //=; apply/fine_cvgP; split => /=; first exact: nearW.
apply/(@cvgrPdist_lt _ [pseudoMetricNormedZmodType R of R^o]) => _/posnumP[e].
near=> n; rewrite opprB addrCA subrr addr0 ger0_norm//.
by near: n; exact: near_infty_natSinv_lt.
Unshelve. all: by end_near. Qed.
Lemma lebesgue_measure_set1 (a : R) : lebesgue_measure [set a] = 0%E.
Proof.
suff : (lebesgue_measure (`]a - 1, a]%classic%R : set R) =
lebesgue_measure (`]a - 1, a[%classic%R : set R) +
lebesgue_measure [set a])%E.
rewrite lebesgue_measure_itvoo_subr1 lebesgue_measure_itvoc => /eqP.
rewrite hlength_itv lte_fin ltr_subl_addr ltr_addl ltr01.
rewrite [in X in X == _]/= EFinN EFinB fin_num_oppeB// addeA subee// add0e.
by rewrite addeC -sube_eq ?fin_num_adde_defl// subee// => /eqP.
rewrite -setUitv1// ?bnd_simp; last by rewrite ltr_subl_addr ltr_addl.
rewrite measureU //; apply/seteqP; split => // x []/=.
by rewrite in_itv/= => + xa; rewrite xa ltxx andbF.
Qed.
Let lebesgue_measure_itvoo (a b : R) :
(lebesgue_measure (`]a, b[ : set R) = hlength `]a, b[)%classic.
Proof.
have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0// -leNgt.
have := lebesgue_measure_itvoc a b.
rewrite 2!hlength_itv => <-; rewrite -setUitv1// measureU//.
- by have /= -> := lebesgue_measure_set1 b; rewrite adde0.
- by apply/seteqP; split => // x [/= + xb]; rewrite in_itv/= xb ltxx andbF.
Qed.
Let lebesgue_measure_itvcc (a b : R) :
(lebesgue_measure (`[a, b] : set R) = hlength `[a, b])%classic.
Proof.
have [ab|ba] := leP a b; last by rewrite set_itv_ge ?measure0// -leNgt.
have := lebesgue_measure_itvoc a b.
rewrite 2!hlength_itv => <-; rewrite -setU1itv// measureU//.
- by have /= -> := lebesgue_measure_set1 a; rewrite add0e.
- by apply/seteqP; split => // x [/= ->]; rewrite in_itv/= ltxx.
Qed.
Let lebesgue_measure_itvco (a b : R) :
(lebesgue_measure (`[a, b[ : set R) = hlength `[a, b[)%classic.
Proof.
have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0// -leNgt.
have := lebesgue_measure_itvoo a b.
rewrite 2!hlength_itv => <-; rewrite -setU1itv// measureU//.
- by have /= -> := lebesgue_measure_set1 a; rewrite add0e.
- by apply/seteqP; split => // x [/= ->]; rewrite in_itv/= ltxx.
Qed.
Let lebesgue_measure_itv_bnd (x y : bool) (a b : R) :
lebesgue_measure ([set` Interval (BSide x a) (BSide y b)] : set R) =
hlength [set` Interval (BSide x a) (BSide y b)].
Proof.
by move: x y => [|] [|]; [exact: lebesgue_measure_itvco |
exact: lebesgue_measure_itvcc | exact: lebesgue_measure_itvoo |
exact: lebesgue_measure_itvoc].
Qed.
Let limnatR : lim (fun k => (k%:R)%:E : \bar R) = +oo%E.
Proof. by apply/cvg_lim => //; apply/cvgenyP. Qed.
Let lebesgue_measure_itv_bnd_infty x (a : R) :
lebesgue_measure ([set` Interval (BSide x a) +oo%O] : set R) = +oo%E.
Proof.
rewrite itv_bnd_infty_bigcup; transitivity (lim (lebesgue_measure \o
(fun k => [set` Interval (BSide x a) (BRight (a + k%:R))] : set R))).
apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu.
+ by move=> k; exact: measurable_itv.
+ by apply: bigcup_measurable => k _; exact: measurable_itv.
+ move=> m n mn; apply/subsetPset => r/=; rewrite !in_itv/= => /andP[->/=].
by move=> /le_trans; apply; rewrite ler_add// ler_nat.
rewrite (_ : _ \o _ = (fun k => k%:R%:E))//.
apply/funext => n /=; rewrite lebesgue_measure_itv_bnd hlength_itv/=.
rewrite lte_fin; have [->|n0] := eqVneq n 0%N; first by rewrite addr0 ltxx.
by rewrite ltr_addl ltr0n lt0n n0 EFinD addeAC EFinN subee ?add0e.
Qed.
Let lebesgue_measure_itv_infty_bnd y (b : R) :
lebesgue_measure ([set` Interval -oo%O (BSide y b)] : set R) = +oo%E.
Proof.
rewrite itv_infty_bnd_bigcup; transitivity (lim (lebesgue_measure \o
(fun k => [set` Interval (BLeft (b - k%:R)) (BSide y b)] : set R))).
apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu.
+ by move=> k; exact: measurable_itv.
+ by apply: bigcup_measurable => k _; exact: measurable_itv.
+ move=> m n mn; apply/subsetPset => r/=; rewrite !in_itv/= => /andP[+ ->].
by rewrite andbT; apply: le_trans; rewrite ler_sub// ler_nat.
rewrite (_ : _ \o _ = (fun k : nat => k%:R%:E))//.
apply/funext => n /=; rewrite lebesgue_measure_itv_bnd hlength_itv/= lte_fin.
have [->|n0] := eqVneq n 0%N; first by rewrite subr0 ltxx.
rewrite ltr_subl_addr ltr_addl ltr0n lt0n n0 EFinN EFinB fin_num_oppeB// addeA.
by rewrite subee// add0e.
Qed.
Lemma lebesgue_measure_itv (i : interval R) :
lebesgue_measure ([set` i] : set R) = hlength [set` i].
Proof.
move: i => [[x a|[|]]] [y b|[|]]; first exact: lebesgue_measure_itv_bnd.
- by rewrite set_itvE ?measure0.
- by rewrite lebesgue_measure_itv_bnd_infty hlength_bnd_infty.
- by rewrite lebesgue_measure_itv_infty_bnd hlength_infty_bnd.
- by rewrite set_itvE ?measure0.
- rewrite set_itvE hlength_setT.
rewrite (_ : setT = [set` `]-oo, 0[] `|` [set` `[0, +oo[]); last first.
by apply/seteqP; split=> // => x _; have [x0|x0] := leP 0 x; [right|left];
rewrite /= in_itv//= x0.
rewrite measureU//=; try exact: measurable_itv.
+ by rewrite lebesgue_measure_itv_infty_bnd lebesgue_measure_itv_bnd_infty.
+ by apply/seteqP; split => // x []/=; rewrite !in_itv/= andbT leNgt => ->.
- by rewrite set_itvE ?measure0.
- by rewrite set_itvE ?measure0.
- by rewrite set_itvE ?measure0.
Qed.
End lebesgue_measure_itv.
Lemma lebesgue_measure_rat (R : realType) :
lebesgue_measure (range ratr : set R) = 0%E.
Proof.
have /pcard_eqP/bijPex[f bijf] := card_rat; set f1 := 'pinv_(fun=> 0) setT f.
rewrite (_ : range _ = \bigcup_n [set ratr (f1 n)]); last first.
apply/seteqP; split => [_ [q _ <-]|_ [n _ /= ->]]; last by exists (f1 n).
exists (f q) => //=; rewrite /f1 pinvKV// ?in_setE// => x y _ _.
by apply: bij_inj; rewrite -setTT_bijective.
rewrite measure_bigcup//; last first.
apply/trivIsetP => i j _ _ ij; apply/seteqP; split => //= _ [/= ->].
move=> /fmorph_inj.
have /set_bij_inj /[apply] := bijpinv_bij (fun=> 0) bijf.
by rewrite in_setE => /(_ Logic.I Logic.I); exact/eqP.
by rewrite eseries0// => n _; exact: lebesgue_measure_set1.
Qed.
Section measurable_fun_measurable.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (D : set T) (f : T -> \bar R).
Hypotheses (mD : measurable D) (mf : measurable_fun D f).
Implicit Types y : \bar R.
Lemma emeasurable_fun_c_infty y : measurable (D `&` [set x | y <= f x]).
Proof. by rewrite -preimage_itv_c_infty; exact/mf/emeasurable_itv. Qed.
Lemma emeasurable_fun_o_infty y : measurable (D `&` [set x | y < f x]).
Proof. by rewrite -preimage_itv_o_infty; exact/mf/emeasurable_itv. Qed.
Lemma emeasurable_fun_infty_o y : measurable (D `&` [set x | f x < y]).
Proof. by rewrite -preimage_itv_infty_o; exact/mf/emeasurable_itv. Qed.
Lemma emeasurable_fun_infty_c y : measurable (D `&` [set x | f x <= y]).
Proof. by rewrite -preimage_itv_infty_c; exact/mf/emeasurable_itv. Qed.
Lemma emeasurable_fin_num : measurable (D `&` [set x | f x \is a fin_num]).
Proof.
rewrite [X in measurable X](_ : _ =
\bigcup_k (D `&` ([set x | - k%:R%:E <= f x] `&` [set x | f x <= k%:R%:E]))).
apply: bigcupT_measurable => k; rewrite -(setIid D) setIACA.
by apply: measurableI; [exact: emeasurable_fun_c_infty|
exact: emeasurable_fun_infty_c].
rewrite predeqE => t; split => [/= [Dt ft]|].
have [ft0|ft0] := leP 0%R (fine (f t)).
exists `|ceil (fine (f t))|%N => //=; split => //; split.
by rewrite -{2}(fineK ft)// lee_fin (le_trans _ ft0)// ler_oppl oppr0.
by rewrite natr_absz ger0_norm ?ceil_ge0// -(fineK ft) lee_fin ceil_ge.
exists `|floor (fine (f t))|%N => //=; split => //; split.
rewrite natr_absz ltr0_norm ?floor_lt0// EFinN.
by rewrite -{2}(fineK ft) lee_fin mulrNz opprK floor_le.
by rewrite -(fineK ft)// lee_fin (le_trans (ltW ft0)).
move=> [n _] [/= Dt [nft fnt]]; split => //; rewrite fin_numElt.
by rewrite (lt_le_trans _ nft) ?ltNyr//= (le_lt_trans fnt)// ltry.
Qed.
Lemma emeasurable_neq y : measurable (D `&` [set x | f x != y]).
Proof.
rewrite (_ : [set x | f x != y] = f @^-1` (setT `\ y)).
exact/mf/measurableD.