-
Notifications
You must be signed in to change notification settings - Fork 49
/
Copy pathlebesgue_measure.v
2598 lines (2358 loc) · 111 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 archimedean.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality fsbigop.
Require Import reals ereal signed topology numfun normedtype function_spaces.
From HB Require Import structures.
Require Import sequences esum measure real_interval realfun exp.
Require Export lebesgue_stieltjes_measure.
(**md**************************************************************************)
(* # Lebesgue Measure *)
(* *)
(* This file contains a formalization of the Lebesgue measure using the *)
(* Measure Extension theorem from measure.v, further develops the theory of *)
(* of measurable functions, and prove properties of the Lebesgue measure *)
(* such as Vitali's covering lemma (infinite case), i.e., given a Vitali *)
(* cover $V$ of $A$, there exists a countable subcollection $D \subseteq V$ *)
(* of pairwise disjoint closed balls such that *)
(* $\lambda(A \setminus \bigcup_k D_k) = 0$. *)
(* *)
(* Main references: *)
(* - Daniel Li, Intégration et applications, 2016 *)
(* - Achim Klenke, Probability Theory 2nd edition, 2014 *)
(* *)
(* ``` *)
(* lebesgue_measure == the Lebesgue measure *)
(* completed_lebesgue_measure == the completed Lebesgue measure *)
(* completed_algebra_gen == generator of the completed Lebesgue *)
(* sigma-algebra *)
(* 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. *)
(* *)
(* ``` *)
(* vitali_cover A B V == V is a Vitali cover of A, here B is a *)
(* collection of non-empty closed balls *)
(* ``` *)
(* *)
(******************************************************************************)
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.
(* This module contains a direct construction of the Lebesgue measure that is
kept here for archival purpose. The Lebesgue measure is actually defined as
an instance of the Lebesgue-Stieltjes measure. *)
Module LebesgueMeasure.
Section hlength.
Context {R : realType}.
Local Open Scope ereal_scope.
Implicit Types i j : interval R.
Definition hlength (A : set (ocitv_type R)) : \bar R :=
let i := Rhull A in (i.2 : \bar R) - 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 : \bar R) - 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_hlength_itv 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 infinite_hlength_itv 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 move=> i2gtNy; rewrite addey//; case: (i.2 : \bar R) i2gtNy.
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: leeB => /=.
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 lerNl 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 (is_true (0%R <= 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. *)
Section hlength_extension.
Context {R : realType}.
Notation hlength := (@hlength R).
Lemma hlength_semi_additive : measure.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_subadditive :
measurable_subset_sigma_subadditive (hlength : set (ocitv_type R) -> _).
Proof.
move=> I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE => -[a _ <-].
rewrite /subset_sigma_subadditive 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 -leeBlDr//.
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 R) :=
`](b i).1, (b i).2 + e%:num / 2 / (2 ^ i.+1)%:R[%classic.
pose Aoc i : set (ocitv_type R) :=
`](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 ltrDl.
apply: (subset_trans lebig); apply: subset_bigcup => i _; rewrite AE /Aoo/=.
move=> x /=; rewrite !in_itv /= => /andP[-> /le_lt_trans->]//=.
by rewrite ltrDl.
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 R) -> _] _ [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 lerD// subr_le0 leNgt.
Qed.
HB.instance Definition _ := Content_SigmaSubAdditive_isMeasure.Build _ _ _
hlength hlength_sigma_subadditive.
Lemma hlength_sigma_finite : sigma_finite setT (hlength : set (ocitv_type R) -> _).
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 hlength.
HB.instance Definition _ := Measure.on lebesgue_measure.
Let 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 hlength_extension.
End LebesgueMeasure.
Definition lebesgue_measure {R : realType} :
set [the measurableType _.-sigma of
g_sigma_algebraType R.-ocitv.-measurable] -> \bar R :=
[the measure _ _ of lebesgue_stieltjes_measure idfun].
HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R).
HB.instance Definition _ (R : realType) :=
SigmaFiniteMeasure.on (@lebesgue_measure R).
Definition completed_lebesgue_measure {R : realType} : set _ -> \bar R :=
[the measure _ _ of completed_lebesgue_stieltjes_measure idfun].
HB.instance Definition _ (R : realType) :=
Measure.on (@completed_lebesgue_measure R).
HB.instance Definition _ (R : realType) :=
SigmaFiniteMeasure.on (@completed_lebesgue_measure R).
Lemma completed_lebesgue_measure_is_complete {R : realType} :
measure_is_complete (@completed_lebesgue_measure R).
Proof. exact: measure_is_complete_caratheodory. Qed.
Definition completed_algebra_gen d {T : semiRingOfSetsType d} {R : realType}
(mu : set T -> \bar R) : set _ :=
[set A `|` N | A in d.-measurable & N in mu.-negligible].
(* the completed sigma-algebra is the same as the caratheodory sigma-algebra *)
Section completed_algebra_caratheodory.
Context {R : realType}.
Local Open Scope ereal_scope.
Notation hlength := (@wlength R idfun).
Notation mu := (@lebesgue_measure R).
Notation completed_mu := (@completed_lebesgue_measure R).
Let cara_sub_calgebra : hlength^*%mu.-cara.-measurable `<=`
(completed_algebra_gen mu).-sigma.-measurable.
Proof.
move=> E; wlog : E / completed_mu E < +oo.
move=> /= wlg.
have /sigma_finiteP[/= F [UFI ndF mF]] :=
measure_extension_sigma_finite (@wlength_sigma_finite R idfun).
move=> mE.
rewrite -(setIT E)/= UFI setI_bigcupr; apply: bigcupT_measurable => i.
apply: wlg.
- rewrite (le_lt_trans _ (mF i).2)//= le_measure// inE/=.
+ by apply: measurableI => //; apply: sub_caratheodory; exact: (mF i).1.
+ by apply: sub_caratheodory; exact: (mF i).1.
- by apply: measurableI => //; apply: sub_caratheodory; exact: (mF i).1.
move=> mEoo /= mE.
have inv0 n : (0 < n.+1%:R^-1 :> R)%R by rewrite invr_gt0.
set S := [set \sum_(0 <= k <oo) hlength (A k) | A in measurable_cover E].
have coverE s : (0 < s)%R ->
exists2 A, @measurable_cover _ (ocitv_type R) E A &
\sum_(0 <= k <oo) hlength (A k) < completed_mu E + s%:E.
move=> s0; have : mu E \is a fin_num by rewrite ge0_fin_numE.
by move/lb_ereal_inf_adherent => /(_ _ s0)[_/= [A EA] <-] ?; exists A.
pose A n := projT1 (cid2 (coverE _ (inv0 n))).
have mA k : @measurable_cover _ (ocitv_type R) E (A k).
by rewrite /A; case: cid2.
have mA_E n :
\sum_(0 <= k <oo) hlength (A n k) < completed_mu E + n.+1%:R^-1%:E.
by rewrite /A; case: cid2.
pose F_ n := \bigcup_m (A n m).
have EF_n n : E `<=` F_ n.
have [/= _] := mA n.
by move=> /subset_trans; apply; apply: subset_bigcup => i _.
have mF_ m : mu (F_ m) < completed_mu E + m.+1%:R^-1%:E.
apply: (le_lt_trans _ (mA_E m)).
apply: (le_trans (outer_measure_sigma_subadditive hlength^*%mu (A m))).
apply: lee_nneseries => // n _.
by rewrite -((measurable_mu_extE hlength) (A m n))//; have [/(_ n)] := mA m.
pose F := \bigcap_n (F_ n).
have FM : @measurable _ (g_sigma_algebraType R.-ocitv.-measurable) F.
apply: bigcapT_measurable => k; apply: bigcupT_measurable => i.
by apply: sub_sigma_algebra; have [/(_ i)] := mA k.
have EF : E `<=` F by exact: sub_bigcap.
have muEF : completed_mu E = mu F.
apply/eqP; rewrite eq_le le_outer_measure//=.
apply/lee_addgt0Pr => /= _/posnumP[e]; near \oo => n.
apply: (@le_trans _ _ (mu (F_ n))).
by apply: le_outer_measure; exact: bigcap_inf.
rewrite (le_trans (ltW (mF_ n)))// leeD// lee_fin ltW//.
by near: n; apply: near_infty_natSinv_lt.
have coverEF s : (0 < s)%R ->
exists2 A, @measurable_cover _ (ocitv_type R) (F `\` E) A &
\sum_(0 <= k <oo) hlength (A k) < completed_mu (F `\` E) + s%:E.
move=> s0.
have : mu (F `\` E) \is a fin_num.
rewrite ge0_fin_numE// (@le_lt_trans _ _ (mu F))//; last by rewrite -muEF.
by apply: le_outer_measure; exact: subDsetl.
by move/lb_ereal_inf_adherent => /(_ _ s0)[_/= [B FEB] <-] ?; exists B.
pose B n := projT1 (cid2 (coverEF _ (inv0 n))).
have mB k : @measurable_cover _ (ocitv_type R) (F `\` E) (B k).
by rewrite /B; case: cid2.
have mB_FE n :
\sum_(0 <= k <oo) hlength (B n k) < completed_mu (F `\` E) + n.+1%:R^-1%:E.
by rewrite /B; case: cid2.
pose G_ n := \bigcup_m (B n m).
have FEG_n n : F `\` E `<=` G_ n.
have [/= _] := mB n.
by move=> /subset_trans; apply; apply: subset_bigcup => i _.
have mG_ m : mu (G_ m) < completed_mu (F `\` E) + m.+1%:R^-1%:E.
apply: (le_lt_trans _ (mB_FE m)).
apply: (le_trans (outer_measure_sigma_subadditive hlength^*%mu (B m))).
apply: lee_nneseries => // n _.
by rewrite -((measurable_mu_extE hlength) (B m n))//; have [/(_ n)] := mB m.
pose G := \bigcap_n (G_ n).
have GM : @measurable _ (g_sigma_algebraType R.-ocitv.-measurable) G.
apply: bigcapT_measurable => k; apply: bigcupT_measurable => i.
by apply: sub_sigma_algebra; have [/(_ i)] := mB k.
have FEG : F `\` E `<=` G by exact: sub_bigcap.
have muG : mu G = 0.
transitivity (completed_mu (F `\` E)).
apply/eqP; rewrite eq_le; apply/andP; split; last exact: le_outer_measure.
apply/lee_addgt0Pr => _/posnumP[e].
near \oo => n.
apply: (@le_trans _ _ (mu (G_ n))).
by apply: le_outer_measure; exact: bigcap_inf.
rewrite (le_trans (ltW (mG_ n)))// leeD// lee_fin ltW//.
by near: n; apply: near_infty_natSinv_lt.
rewrite measureD//=.
+ by rewrite setIidr// muEF subee// ge0_fin_numE//; move: mEoo; rewrite muEF.
+ exact: sub_caratheodory.
+ by move: mEoo; rewrite muEF.
apply: sub_sigma_algebra; exists (F `\` G); first exact: measurableD.
exists (E `&` G).
by apply: (@negligibleS _ _ _ mu G _ (@subIsetr _ E G)); exists G; split.
apply/seteqP; split=> [/= x [[Fx Gx]|[]//]|x Ex].
- by rewrite -(notK (E x)) => Ex; apply: Gx; exact: FEG.
- have [|FGx] := pselect ((F `\` G) x); first by left.
right; split => //.
move/not_andP : FGx => [|].
by have := EF _ Ex.
by rewrite notK.
Unshelve. all: by end_near. Qed.
Lemma g_sigma_completed_algebra_genE :
(completed_algebra_gen mu).-sigma.-measurable = completed_algebra_gen mu.
Proof.
apply/seteqP; split; last first.
move=> _ [/= A /= mA [N neglN]] <-.
by apply: sub_sigma_algebra; exists A => //; exists N.
apply: smallest_sub => //=; split => /=.
- by exists set0 => //; exists set0; [exact: negligible_set0|rewrite setU0].
- move=> G [/= A mA [N negN ANG]]; case: negN => /= F [mF F0 NF].
have GANA : ~` G = ~` A `\` (N `&` ~` A).
by rewrite -ANG setCU setDE setCI setCK setIUr setICl setU0.
pose AA := ~` A `\` (F `&` ~` A).
pose NN := (F `&` ~` A) `\` (N `&` ~` A).
have GAANN : ~` G = AA `|` NN.
rewrite (_ : ~` G = ~` A `\` (N `&` ~` A))//.
by apply: setDU; [exact: setSI|exact: subIsetr].
exists AA.
apply: measurableI => //=; first exact: measurableC.
by apply: measurableC; apply: measurableI => //; exact: measurableC.
by exists NN; [exists F; split => // x [] []|rewrite setDE setTI].
- move=> F mF/=.
pose A n := projT1 (cid2 (mF n)).
pose N n := projT1 (cid2 (projT2 (cid2 (mF n))).2).
exists (\bigcup_k A k).
by apply: bigcupT_measurable => i; rewrite /A; case: cid2.
exists (\bigcup_k N k).
apply: negligible_bigcup => /= k.
by rewrite /N; case: (cid2 (mF k)) => //= *; case: cid2.
rewrite -bigcupU; apply: eq_bigcup => // i _.
by rewrite /A /N; case: (cid2 (mF i)) => //= *; case: cid2.
Qed.
Lemma negligible_sub_caratheodory :
completed_mu.-negligible `<=` hlength^*%mu.-cara.-measurable.
Proof.
move=> N /= [/= A] [mA A0 NA].
apply: le_caratheodory_measurable => /= X.
apply: (@le_trans _ _ (hlength^*%mu N + hlength^*%mu (X `&` ~` N))).
by rewrite leeD2r// le_outer_measure//; exact: subIsetr.
have -> : hlength^*%mu N = 0.
by apply/eqP; rewrite eq_le outer_measure_ge0//= andbT -A0 le_outer_measure.
by rewrite add0e// le_outer_measure//; exact: subIsetl.
Qed.
Let calgebra_sub_cara : (completed_algebra_gen mu).-sigma.-measurable `<=`
hlength^*%mu.-cara.-measurable.
Proof.
rewrite g_sigma_completed_algebra_genE => A -[/= X mX] [N negN] <-{A}.
apply: measurableU => //; first exact: sub_caratheodory.
apply: negligible_sub_caratheodory; case: negN => /= B [mB B0 NB].
by exists B; split => //=; exact: sub_caratheodory.
Qed.
Lemma completed_caratheodory_measurable :
(completed_algebra_gen mu).-sigma.-measurable =
hlength^*%mu.-cara.-measurable.
Proof.
by apply/seteqP; split; [exact: calgebra_sub_cara | exact: cara_sub_calgebra].
Qed.
End completed_algebra_caratheodory.
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 _ _
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 := g_sigma_algebraType (R.-ocitv.-measurable).
Definition measurableR : set (set R) :=
(R.-ocitv.-measurable).-sigma.-measurable.
HB.instance Definition _ := Pointed.on R.
HB.instance Definition R_isMeasurable :
isMeasurable default_measure_display R :=
@isMeasurable.Build _ measurableTypeR 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].
by apply: sub_sigma_algebra; apply: is_ocitv.
have mopoo (x : R) : measurable `]x, +oo[.
by rewrite itv_bnd_infty_bigcup; exact: bigcup_measurable.
have mnooc (x : R) : measurable `]-oo, x].
by rewrite -setCitvr; exact/measurableC.
have ooE (a b : R) : `]a, b[%classic = `]a, b] `\ 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[.
by rewrite ooE; exact: measurableD.
have mcc (a b : R) : measurable `[a, b].
case: (boolP (a <= b)) => ab; last by rewrite set_itv_ge.
by rewrite -setU1itv//; apply/measurableU.
have mco (a b : R) : measurable `[a, b[.
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] `\ 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 (only parsing).
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 (only parsing).
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 (only parsing).
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 (only parsing).
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 _ _ _ (@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 (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.2", note="use `emeasurable_itv` instead")]
Notation emeasurable_itv_ninfty_bnd := emeasurable_itv (only parsing).
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 (only parsing).
Section lebesgue_measure_itv.
Variable R : realType.
Let lebesgue_measure_itvoc (a b : R) :
(lebesgue_measure (`]a, b] : set R) =
wlength [the cumulative _ of idfun] `]a, b])%classic.
Proof.
rewrite /lebesgue_measure/= /lebesgue_stieltjes_measure/= /measure_extension/=.
by rewrite measurable_mu_extE//; exact: is_ocitv.
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 (limn (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 lerB// ler_pV2 ?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.
by rewrite invr1 subrr set_itvoc0 wlength0.
rewrite wlength_itv/= lte_fin ifT; last first.
by rewrite ler_ltB// 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 _ [the 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 wlength_itv lte_fin ltrBlDr ltrDl 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 ltrBlDr ltrDl.
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) =
wlength [the cumulative _ of idfun] `]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!wlength_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) =
wlength [the cumulative _ of idfun] `[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!wlength_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) =
wlength [the cumulative _ of idfun] `[a, b[)%classic.
Proof.