From 4080012c50a87142bf233ef50b4c0f28684d6636 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 30 Aug 2021 19:32:02 +0900 Subject: [PATCH] measurable_fun and generated sigma-algebras --- _CoqProject | 2 +- .../{measure_wip.v => lebesgue_measure.v} | 672 ++++++++++-------- 2 files changed, 366 insertions(+), 308 deletions(-) rename theories/{measure_wip.v => lebesgue_measure.v} (92%) diff --git a/_CoqProject b/_CoqProject index ee5ab22a46..76f9522d86 100644 --- a/_CoqProject +++ b/_CoqProject @@ -22,7 +22,7 @@ theories/normedtype.v theories/sequences.v theories/cardinality.v theories/csum.v -theories/measure_wip.v +theories/lebesgue_measure.v theories/forms.v theories/derive.v theories/measure.v diff --git a/theories/measure_wip.v b/theories/lebesgue_measure.v similarity index 92% rename from theories/measure_wip.v rename to theories/lebesgue_measure.v index 67aa1a8055..fc5d383614 100644 --- a/theories/measure_wip.v +++ b/theories/lebesgue_measure.v @@ -8,9 +8,10 @@ From HB Require Import structures. Require Import sequences measure csum cardinality. (******************************************************************************) -(* Lebesgue measure *) +(* Lebesgue Measure (WIP) *) (* *) -(* To be integrated into measure.v *) +(* This file contains a tentative formalization of the Lebesgue measure using *) +(* the Caratheodory's theorem available in measure.v. *) (* *) (* s<< G >> == sigma-algebra generated by G *) (* dynkin S == S is a Dynkin system *) @@ -35,14 +36,13 @@ Require Import sequences measure csum cardinality. (* hlength A == length of the hull of the set of real numbers A *) (* Lemma hlengthUitv == hlength is additive on intervals *) (* *) -(* slength X == measure of the set X when it is a simple set, and 0 o.w. *) -(* ccitv n == [-n, n] interval *) +(* slength X == measure of the set X when it is a simple set, and 0 o.w. *) +(* ccitv n == [-n, n] interval *) (* slength_sigma_finite == slength is sigma-finite *) (* *) (* Section slength_additive: *) (* This section establishes that slength is additive on simple sets. *) -(* Lemma: *) -(* slength_additive *) +(* Lemma: slength_additive *) (* Section slength_sigma_additive_on_intervals: *) (* This section established that slength is sigma-additive on intervals *) (* seen as simple sets. Lemmas: *) @@ -87,6 +87,9 @@ rewrite [LHS]big_nat_cond [RHS]big_nat_cond; apply eq_bigr => i. by rewrite andbT => /nim fi; rewrite -EFin_real_of_extended. Qed. +Lemma EFin_inj (R : numDomainType) : injective (@EFin R). +Proof. by move=> a b; case. Qed. + Lemma telescope_sume (R : numDomainType) n m (f : (\bar R)^nat) : (forall i, (n <= i <= m)%N -> f i \is a fin_num) -> (n <= m)%N -> @@ -237,17 +240,17 @@ Qed. Section generated_salgebra. Variables (U : Type). -Implicit Types M : set (set U). +Implicit Types M G : set (set U). -Inductive g_salgebra M : set (set U) := -| g_salgebra_self : forall A, M A -> s<< M >> A -| g_salgebra_set0 : s<< M >> set0 -| g_salgebra_setC : forall A, s<< M >> A -> s<< M >> (~` A) -| g_salgebra_bigcup : forall A : (set U)^nat, (forall i, s<< M >> (A i)) -> - s<< M >> (\bigcup_i (A i)) where "'s<<' M '>>'" := (g_salgebra M). +Inductive g_salgebra G : set (set U) := +| g_salgebra_self : forall A, G A -> s<< G >> A +| g_salgebra_set0 : s<< G >> set0 +| g_salgebra_setC : forall A, s<< G >> A -> s<< G >> (~` A) +| g_salgebra_bigcup : forall A : (set U)^nat, (forall i, s<< G >> (A i)) -> + s<< G >> (\bigcup_i (A i)) where "'s<<' G '>>'" := (g_salgebra G). -Lemma g_salgebraE M : - s<< M >> = \bigcap_(A in [set T : set (set U) | measurableP T /\ M `<=` T]) A. +Lemma g_salgebraE G : + s<< G >> = \bigcap_(A in [set M | measurableP M /\ G `<=` M]) A. Proof. rewrite predeqE => A; split => [|]. elim=> [ {}A ? N [?] | {}A [[]]| {}A ? MA N [[? NC ?] ?] | {}A ? MA N [[? ? NI] ?]]; @@ -256,15 +259,15 @@ apply; split; [split|]; [exact: g_salgebra_set0 | exact: g_salgebra_setC | exact: g_salgebra_bigcup | by move=> B MB; apply g_salgebra_self]. Qed. -Lemma measurableP_g_salgebra M : measurableP (g_salgebra M). +Lemma measurableP_g_salgebra G : measurableP (g_salgebra G). Proof. by rewrite g_salgebraE; apply measurableP_bigcap => /= ? [?]. Qed. -Lemma g_salgebra_smallest M : - forall T : set (set U), measurableP T -> M `<=` T -> g_salgebra M `<=` T. -Proof. by move=> T mT MT t; rewrite g_salgebraE; exact. Qed. +Lemma g_salgebra_smallest G M : + measurableP M -> G `<=` M -> g_salgebra G `<=` M. +Proof. by move=> mM GM A; rewrite g_salgebraE; exact. Qed. End generated_salgebra. -Notation "'s<<' M '>>'" := (g_salgebra M). +Notation "'s<<' G '>>'" := (g_salgebra G). Definition g_measurable (U : Type) (C : set (set U)) := U. @@ -275,12 +278,20 @@ HB.instance Definition g_salgebra_mixin := @isMeasurable.Build (g_measurable C) (g_salgebra C) (@g_salgebra_set0 _ C) (@g_salgebra_setC _ C) (@g_salgebra_bigcup _ C). -Definition g_salgebra_measurableType := [the measurableType of g_measurable C]. +Definition g_measurableType := [the measurableType of g_measurable C]. End generated_salgebra_instance. +Lemma measurable_g_measurableTypeE (T : Type) (G : set (set T)) : + measurableP G -> @measurable (g_measurableType G) = G. +Proof. +move=> mM; rewrite eqEsubset; split; first exact: g_salgebra_smallest. +by move=> A MA; apply g_salgebra_self. +Qed. + +(* TODO: move *) Section measure_setD. -Variables (R : realType) (T : ringOfSetsType). +Variables (R : realFieldType) (T : ringOfSetsType). Variables m : {measure set T -> \bar R}. Lemma measure_setDI A B : measurable A -> measurable B -> @@ -288,11 +299,11 @@ Lemma measure_setDI A B : measurable A -> measurable B -> Proof. move=> mA mB. rewrite -[in LHS](SetOrder.Internal.joinIB A B) measure_semi_additive2. -by rewrite addeC. -exact: measurableI. -exact: measurableD. -by apply: measurableU; [exact: measurableI |exact: measurableD]. -by rewrite setDE setICA -setIA setICr 2!setI0. +- by rewrite addeC. +- exact: measurableI. +- exact: measurableD. +- by apply: measurableU; [exact: measurableI |exact: measurableD]. +- by rewrite setDE setICA -setIA setICr 2!setI0. Qed. Lemma measure_setD A B : measurable A -> measurable B -> @@ -303,67 +314,13 @@ rewrite (measure_setDI mA mB) addeK // fin_numE; apply/andP; split. rewrite gt_eqF// (lt_le_trans _ (measure_ge0 _ _))// ?lte_ninfty//. exact: measurableI. rewrite lt_eqF// (le_lt_trans _ mAoo)// le_measure //. -by rewrite inE /=; exact: measurableI. -by rewrite inE. -by apply: subIset; left. +- by rewrite inE /=; exact: measurableI. +- by rewrite inE. +- by apply: subIset; left. Qed. End measure_setD. -(* NB: PR in progress *) -Definition seqDU T (F : (set T)^nat) n := F n `\` (\big[setU/set0]_(m < n) F m). - -Lemma seqDUE T (F : (set T)^nat) : nondecreasing_seq F -> seqDU F = seqD F. -Proof. -move=> ndF; rewrite funeqE => -[|n] /=; first by rewrite /seqDU big_ord0 setD0. -rewrite /seqDU big_ord_recr /= setUC; congr (_ `\` _); apply/setUidPl. -by rewrite bigcup_ord => + [k /= kn]; exact/subsetPset/ndF/ltnW. -Qed. - -Lemma trivIset_seqDU T (F : (set T)^nat) : trivIset setT (seqDU F). -Proof. -move=> i j _ _; wlog ij : i j / (i < j)%N => [/(_ _ _ _) tB|]. - by have [ij /tB->|ij|] := ltngtP i j; rewrite //setIC => /tB->. -move=> /set0P; apply: contraNeq => _; apply/eqP. -rewrite /seqDU 2!setDE !setIA setIC (bigD1 (Ordinal ij)) //=. -by rewrite setCU setIAC !setIA setICl !set0I. -Qed. - -Lemma trivIset_seqD_new T (A : (set T) ^nat) : - nondecreasing_seq A -> trivIset setT (seqD A). -Proof. -by move=> ndF; rewrite -seqDUE //; exact: trivIset_seqDU. -Qed. - -Lemma bigsetU_seqDU T (F : (set T)^nat) n : - \big[setU/set0]_(m < n) F m = \big[setU/set0]_(m < n) seqDU F m. -Proof. -elim: n => [|n ih]; first by rewrite 2!big_ord0. -rewrite !big_ord_recr /= predeqE => t; split=> [[Ft|Fnt]|[Ft|[Fnt Ft]]]. -- by left; rewrite -ih. -- have [?|?] := pselect ((\big[setU/set0]_(i < n) seqDU F i) t); first by left. - by right; split => //; rewrite ih. -- by left; rewrite ih. -- by right. -Qed. - -Lemma seqDU_bigcup_eq T (F : (set T)^nat) : \bigcup_m (F m) = \bigcup_m (seqDU F m). -Proof. -rewrite /seqDU predeqE=> t; split=> [[i _ Fit]|[i _]]; last first. - by rewrite setDE => -[Fit _]; exists i. -have [X|X] := pselect ((\big[setU/set0]_(k < i) F k) t); last by exists i. -suff [j [Fjt Fijt]] : exists j, F j t /\ forall k, (k < j)%N -> ~ F k t. - by exists j => //; split => //; rewrite bigcup_ord => -[k /= kj]; exact: Fijt. -move: X; rewrite bigcup_ord => -[/= k ki Fkt]; clear Fit ki i. -have [n ni] := ubnP k; elim: n => // n ih in t k Fkt ni *. -case: k => [|k] in Fkt ni *; first by exists O. -rewrite ltnS in ni. -have [?|] := pselect (forall k0 : nat, (k0 < k.+1)%N -> ~ F k0 t); first by exists k.+1. -move=> /existsNP[i] /not_implyP[ik1] /contrapT Fit; apply (ih t i) => //. -by rewrite ltnS in ik1; rewrite (leq_ltn_trans ik1). -Qed. -(* /end PR in progress *) - Lemma lim_mkord (R : realType) (f : (\bar R)^nat) : lim (fun n => \sum_(k < n) f k)%E = \sum_(k _) = (fun n => \sum_(0 <= k < n) f k)%E) // funeqE => k. by rewrite big_mkord. Qed. -(* TODO: move *) -Lemma add_ltoo (R : realDomainType) (x y : \bar R) : x < +oo -> y < +oo -> x + y < +oo. +(* TODO: PR 422 in progress *) +Lemma nondecreasing_seqP' (d : unit) (T : porderType d) (u_ : T ^nat) : + (forall n, u_ n <= u_ n.+1)%O <-> nondecreasing_seq u_. +Proof. by split=> [|h n]; [exact: homo_leq le_trans | exact: h]. Qed. +(* /TODO: PR 422 in progress *) + +(* TODO: PR *) +Lemma lte_add_pinfty (R : realDomainType) (x y : \bar R) : x < +oo -> y < +oo -> x + y < +oo. Proof. by move: x y => -[r [r'| |]| |] // ? ?; rewrite -addEFin lte_pinfty. Qed. -(* TODO: generalize *) Lemma lte_sum_pinfty (R : realDomainType) T (s : seq T) (P : pred T) (f : T -> \bar R) : (forall x, P x -> f x < +oo) -> \sum_(i <- s | P i) f i < +oo. Proof. elim/big_ind : _ => [_|x y xoo yoo foo|i ?]; [exact: lte_pinfty| |exact]. -by apply: add_ltoo; [exact: xoo| exact: yoo]. +by apply: lte_add_pinfty; [exact: xoo| exact: yoo]. Qed. -(* TODO: move *) Section sigma_finite_lemma. Variables (R : realFieldType) (T : ringOfSetsType) (A : set T) (mu : {additive_measure set T -> \bar R}). Lemma sigma_finiteP : sigma_finite A mu -> - exists2 F : (set T)^nat, - A = \bigcup_i F i & - (forall i, F i `<=` F i.+1) /\ - forall i, measurable (F i) /\ mu (F i) < +oo. + exists2 F, A = \bigcup_i F i & + nondecreasing_seq F /\ forall i, measurable (F i) /\ mu (F i) < +oo. Proof. -move=> [S AS moo]. -exists (fun n => \big[setU/set0]_(i < n.+1) S i). +move=> [S AS moo]; exists (fun n => \big[setU/set0]_(i < n.+1) S i). rewrite AS predeqE => t; split => [[i _ Sit]|[i _]]. - by exists i => //; rewrite big_ord_recr /=; right. + by exists i => //; rewrite big_ord_recr /=; right. by rewrite bigcup_ord => -[j /= ji Sjt]; exists j. -split => i. - by rewrite [in X in _ `<=` X]big_ord_recr /=; left. split. - by apply: bigsetU_measurable => j _; exact: (moo j).1. + apply/nondecreasing_seqP' => i. + rewrite [in X in (_ <= X)%O]big_ord_recr /=. + by apply/subsetPset; left. +move=> i; split; first by apply: bigsetU_measurable => j _; exact: (moo j).1. rewrite (@le_lt_trans _ _ (\sum_(j < i.+1) mu (S j))) //. by apply: Boole_inequality => j; exact: (moo j).1. by apply/lte_sum_pinfty => j _; exact: (moo j).2. @@ -539,7 +498,7 @@ Hypothesis GI : forall A B, G A -> G B -> G (A `&` B). (* existence of an exhausting sequence *) Variable g : (set T)^nat. Hypothesis Gg : forall i, G (g i). -Hypothesis gnondecr : forall k, g k `<=` g k.+1. +Hypothesis nd_g : nondecreasing_seq g. Hypothesis gfull : \bigcup_k (g k) = setT. Variables m m' : {measure set T -> \bar R}. Hypothesis mm' : forall A, G A -> m A = m' A. @@ -586,8 +545,7 @@ transitivity (lim (fun n => m (g n `&` E))). - by move=> i; apply: measurableI => //; rewrite TG; exact/g_salgebra_self/Gg. - apply/measurable_bigcup => i; apply/measurableI => //. by rewrite TG; exact/g_salgebra_self/Gg. - - move=> p q pq; apply: setSI; apply/subsetPset. - by apply/nondecreasing_seqP => // n; exact/subsetPset/gnondecr. + - by move=> p q pq; apply/subsetPset; apply: setSI; apply/subsetPset/nd_g. transitivity (lim (fun n => m' (g n `&` E))). rewrite (_ : (fun n => _) = (fun n => m' (g n `&` E))) //. by rewrite funeqE => i; rewrite mm'g. @@ -595,8 +553,7 @@ rewrite -[in RHS](gE E) //; apply/cvg_lim/cvg_mu_inc => //. - by move=> i; apply: measurableI => //; rewrite TG; exact/g_salgebra_self/Gg. - apply/measurable_bigcup => i; apply/measurableI => //. by rewrite TG; exact/g_salgebra_self/Gg. -- move=> p q pq; apply: setSI; apply/subsetPset. - by apply/nondecreasing_seqP => // n; exact/subsetPset/gnondecr. +- by move=> p q pq; apply/subsetPset; apply: setSI; apply/subsetPset/nd_g. Qed. End measure_unique. @@ -668,7 +625,7 @@ near=> n; apply: lee_sum => i _; rewrite -measure_semi_additive2. - by rewrite setIACA setICr setI0. Grab Existential Variables. all: end_near. Qed. -Let I : measurableType := g_salgebra_measurableType (@measurable T). +Let I : measurableType := g_measurableType (@measurable T). Definition Hahn_ext' : set I -> \bar R := mu_ext mu. Definition Hahn_ext : {measure set I -> \bar R}. @@ -1022,17 +979,17 @@ Definition set_of_itvE := (set_of_itv_open_open, set_of_itv_closed_closed, set_of_itv_ninfty_closed, set_of_itv_ninfty_ninfty, set_of_itv_pinfty_ninfty, set_of_itv_pinfty_pinfty, set_of_itv_infty_set0). -Section punctured_interval. +Section puncture_interval. -Lemma open_closed_set1 x y : x < y -> +Lemma punct_itv_oc x y : x < y -> set_of_itv `]x, y] = set_of_itv `]x, y[ `|` [set y]. Proof. -move=> ab; rewrite !set_of_itvE predeqE => r; split=>[/andP[xr]|]. - by rewrite le_eqVlt => /orP[/eqP->|ry]; [by right|left; rewrite xr]. +move=> ab; rewrite !set_of_itvE predeqE => r; split=> [/andP[xr]|]. + by rewrite le_eqVlt => /orP[/eqP->|ry]; [right|left; rewrite xr]. by case=> [/andP[ar /ltW ->]|->]; [rewrite andbT|rewrite ab lexx]. Qed. -Lemma closed_open_set1 x y : x < y -> +Lemma punct_itv_co x y : x < y -> set_of_itv `[x, y[ = [set x] `|` set_of_itv `]x, y[. Proof. move=> xy; rewrite !set_of_itvE predeqE => r; split=> [/andP[]|]. @@ -1040,7 +997,7 @@ move=> xy; rewrite !set_of_itvE predeqE => r; split=> [/andP[]|]. by case=> [->|/andP[/ltW -> -> //]]; rewrite lexx. Qed. -Lemma closed_closed_set1l x y : x <= y -> +Lemma punct_itv_ccL x y : x <= y -> set_of_itv `[x, y] = [set x] `|` set_of_itv `]x, y]. Proof. move=> ab; rewrite !set_of_itvE predeqE => r; split=> [/andP[]|]. @@ -1048,7 +1005,7 @@ move=> ab; rewrite !set_of_itvE predeqE => r; split=> [/andP[]|]. by case=> [->|/andP[/ltW -> -> //]]; rewrite lexx. Qed. -Lemma closed_closed_set1r x y : x <= y -> +Lemma punct_itv_ccR x y : x <= y -> set_of_itv `[x, y] = set_of_itv `[x, y[ `|` [set y]. Proof. move=> xy; rewrite !set_of_itvE predeqE => r; split=> [/andP[xr]|]. @@ -1056,19 +1013,19 @@ move=> xy; rewrite !set_of_itvE predeqE => r; split=> [/andP[xr]|]. by case=> [/andP[-> /ltW //]|->]; rewrite lexx xy. Qed. -Lemma closed_pinfty_set1 x : set_of_itv `[x, +oo[ = [set x] `|` set_of_itv `]x, +oo[. +Lemma punct_itv_coo x : set_of_itv `[x, +oo[ = [set x] `|` set_of_itv `]x, +oo[. Proof. rewrite predeqE => r; rewrite !set_of_itvE; split; last by case=> [->//|/ltW]. by rewrite le_eqVlt => /orP[/eqP ->|?]; [left|right]. Qed. -Lemma ninfty_closed_set1 x : set_of_itv `]-oo, x] = set_of_itv `]-oo, x[ `|` [set x]. +Lemma punct_itv_ooc x : set_of_itv `]-oo, x] = set_of_itv `]-oo, x[ `|` [set x]. Proof. rewrite predeqE => r; rewrite !set_of_itvE; split => [|[/ltW //|-> //=]]. by rewrite le_eqVlt => /orP[/eqP ->|xr]; [right|left]. Qed. -End punctured_interval. +End puncture_interval. End set_of_itv. Arguments set_of_itv {R}. @@ -1235,8 +1192,7 @@ Implicit Types x y : R. Lemma sup_ninfty x b : sup (set_of_itv (Interval -oo%O (BSide b x))) = x. Proof. -case: b; last first. - by rewrite ninfty_closed_set1 sup_setU ?sup1 // => ? ? ? ->; exact/ltW. +case: b; last by rewrite punct_itv_ooc sup_setU ?sup1// => ? ? ? ->; exact/ltW. set s := sup _; apply/eqP; rewrite eq_le; apply/andP; split. - apply sup_le_ub; last by move=> ? /ltW. by exists (x - 1); rewrite !set_of_itvE ltr_subl_addr ltr_addl. @@ -1248,14 +1204,14 @@ Qed. Lemma inf_pinfty x b : inf (set_of_itv (Interval (BSide b x) +oo%O)) = x. Proof. case: b; last by rewrite /inf minus_bside_pinfty sup_ninfty opprK. -by rewrite closed_pinfty_set1 inf_setU ?inf1 // => _ b->; rewrite !set_of_itvE => /ltW. +by rewrite punct_itv_coo inf_setU ?inf1// => _ b->; rewrite !set_of_itvE => /ltW. Qed. Let sup_open_bside x y b : x < y -> sup (set_of_itv (Interval (BRight x) (BSide b y))) = y. Proof. case: b => xy; last first. - by rewrite open_closed_set1 // sup_setU ?sup1 // => ? ? /andP[? /ltW ?] ->. + by rewrite punct_itv_oc// sup_setU ?sup1// => ? ? /andP[? /ltW ?] ->. set B := set_of_itv _; set A := set_of_itv `]-oo, x]. rewrite -(@sup_setU _ A B) //. - rewrite -(sup_ninfty y true); congr sup. @@ -1270,21 +1226,20 @@ Lemma sup_bounded x y a b : x < y -> Proof. case: a => xy; last exact: sup_open_bside. case: b. - by rewrite closed_open_set1 // sup_setU ?sup_open_bside // => ? ? -> /andP[/ltW]. -rewrite closed_closed_set1r; last exact/ltW. -by rewrite sup_setU ?sup1// => ? ? /andP[_ /ltW ? ->]. + by rewrite punct_itv_co// sup_setU ?sup_open_bside// => ? ? -> /andP[/ltW]. +by rewrite (punct_itv_ccR (ltW _))// sup_setU ?sup1// => ? ? /andP[_ /ltW ? ->]. Qed. Lemma sup_closed_closed x y : x <= y -> sup (set_of_itv `[x, y]) = y. Proof. -by move=> xy; rewrite closed_closed_set1r // sup_setU ?sup1 // => ? ? /andP[_ /ltW ? ->]. +by move=> ?; rewrite punct_itv_ccR// sup_setU ?sup1// => ? ? /andP[_ /ltW ? ->]. Qed. Let inf_bside_open x y b : x < y -> inf (set_of_itv (Interval (BSide b x) (BLeft y))) = x. Proof. case: b => xy. - by rewrite closed_open_set1// inf_setU ?inf1 // => _ ? -> /andP[/ltW]. + by rewrite punct_itv_co// inf_setU ?inf1// => _ ? -> /andP[/ltW]. by rewrite /inf minus_open_open sup_open_bside ?opprK // ltr_oppl opprK. Qed. @@ -1293,14 +1248,13 @@ Lemma inf_bounded x y a b : x < y -> Proof. case: b => xy; first exact: inf_bside_open. case: a. - rewrite closed_closed_set1l; last exact: ltW. - by rewrite inf_setU ?inf1 // => ? ? -> /andP[/ltW]. -by rewrite open_closed_set1 // inf_setU ?inf_bside_open // => ? ? /andP[? /ltW ?] ->. + by rewrite (punct_itv_ccL (ltW _))// inf_setU ?inf1// => ? ? -> /andP[/ltW]. +by rewrite punct_itv_oc// inf_setU ?inf_bside_open// => ? ? /andP[? /ltW ?] ->. Qed. Lemma inf_closed_closed x y : x <= y -> inf (set_of_itv `[x, y]) = x. Proof. -by move=> ?; rewrite closed_closed_set1l // inf_setU ?inf1 // => ? ? -> /andP[/ltW]. +by move=> ?; rewrite punct_itv_ccL// inf_setU ?inf1 // => ? ? -> /andP[/ltW]. Qed. End interval_sup_inf. @@ -2662,7 +2616,7 @@ Section ring_of_sets_instance. Variable R : realType. HB.instance Definition sset_algebraOfSets := @isAlgebraOfSets.Build (Real.sort R) - (@is_sset R) (@is_sset0 R) (@is_ssetU R) (@is_ssetC R). + (@is_sset R) (@is_sset0 R) (@is_ssetU R) (@is_ssetC R). Definition sset_algebraOfSetsType := [the algebraOfSetsType of (Real.sort R)]. @@ -4377,22 +4331,21 @@ End intervals_are_measurable. Section lebesgue_measure. Variable R : realType. Let ssets := @measurable (@sset_algebraOfSetsType R). -Let gssets := g_salgebra_measurableType ssets. +Let gssets := g_measurableType ssets. Definition lebesgue_measure : {measure set gssets -> \bar R} := Hahn_ext (@slength_measure R). -Lemma lebesgue_measure_unique : - forall mu : {measure set gssets -> \bar R}, - (forall X, ssets X -> mu X = slength X) -> - (forall X, measurable X -> lebesgue_measure X = mu X). +Lemma lebesgue_measure_unique (mu : {measure set gssets -> \bar R}) : + (forall X, ssets X -> mu X = slength X) -> + forall X, measurable X -> lebesgue_measure X = mu X. Proof. -move=> mu muslength X mX; apply: Hahn_ext_unique => //. -exact: slength_sigma_finite. +by move=> ssetsmu X mX; apply: Hahn_ext_unique => //; exact: slength_sigma_finite. Qed. End lebesgue_measure. +(* TODO: PR? *) Lemma bigcup_setU (T I : Type) (P : set I) (F G : I -> set T) : \bigcup_(i in P) (F i `|` G i) = (\bigcup_(i in P) F i) `|` (\bigcup_(i in P) G i). Proof. @@ -4400,11 +4353,7 @@ rewrite predeqE => x; split=> [[i Pi [Fix|Gix]]|[[i Pi Fix]|[i Pi Gix]]]; by [left; exists i | right; exists i | exists i => //; left | exists i => //; right]. Qed. -(* NB: PR in progress *) -Lemma orA : associative or. -Proof. by move=> P Q R; rewrite propeqE; split=> [|]; tauto. Qed. -(* /NB: PR in progress *) - +(* TODO: PR along subset_set1? *) Lemma subset_set2 T (A : set T) a b : A `<=` [set a; b] -> A = set0 \/ A = [set a] \/ A = [set b] \/ A = [set a; b]. Proof. @@ -4423,60 +4372,40 @@ have <- : z = b by apply: contrapT => zb; move/Aab : Az => [|]. by move=> _ [|] ->. Qed. -Lemma EFin_inj (R : numDomainType) : injective (@EFin R). -Proof. by move=> a b; case. Qed. - -Section sigma_algebra_R_Rbar. -Variable R : realType. - -Fail Check forall (T : measurableType) (f : T -> R), measurable_fun setT f. - -Let measurableTypeR := - g_salgebra_measurableType (@measurable (@sset_algebraOfSetsType R)). - -Definition measurableR : set (set R) := @measurable measurableTypeR. - -Definition R_isMeasurable : isMeasurable R := - isMeasurable.Build measurableTypeR - measurable0 (@measurableC _) (@measurable_bigcup _). - -HB.instance (Real.sort R) R_isMeasurable. - -Check forall (T : measurableType) (f : T -> R), measurable_fun setT f. +(* construction of a sigma-algebra for \bar R given a generated sigma-algebra for R *) +Section salgebra_Rbar. +Variables (R : realType) (G : set (set R)). +Let measurableTypeR := g_measurableType G. +Let measurableR : set (set R) := @measurable measurableTypeR. -Lemma measurable_itv (i : interval R) : measurable (set_of_itv i). -Proof. exact/g_salgebra_self/measurable_sset_itv. Qed. - -(* powerset to extend the sigma-algebra for R *) -Definition PSoo : set (set \bar R) := +(* powerset *) +Definition ps_infty_def : set (set \bar R) := [set set0; [set -oo]; [set +oo]; [set -oo; +oo]]%E. -Inductive PSoo' : set \bar R -> Prop := -| PS0 : PSoo' set0 -| PSnoo : PSoo' [set -oo]%E -| PSpoo : PSoo' [set +oo]%E -| PSnpoo : PSoo' [set -oo; +oo]%E. +Inductive ps_infty : set \bar R -> Prop := +| ps_infty0 : ps_infty set0 +| ps_ninfty : ps_infty [set -oo]%E +| ps_pinfty : ps_infty [set +oo]%E +| ps_inftys : ps_infty [set -oo; +oo]%E. -Lemma PSoo'P (A : set \bar R) : PSoo' A <-> A `<=` [set -oo; +oo]%E. +Lemma ps_inftyP (A : set \bar R) : ps_infty A <-> A `<=` [set -oo; +oo]%E. Proof. split => [[]//|Aoo]; [by left|by right| ]. by have [|[|[|]]] := subset_set2 Aoo; move=> ->; constructor. Qed. Definition measurableRbar : set (set \bar R) := - [set (@EFin _ @` A) `|` B | A in measurableR & B in PSoo']. + [set (@EFin _ @` A) `|` B | A in measurableR & B in ps_infty]. Lemma measurableRbar0 : measurableRbar set0. Proof. -exists set0; first exact: measurable0. -by exists set0; rewrite ?setU0// ?image_set0//; constructor. +by exists set0; [exact: measurable0|exists set0; rewrite ?setU0// ?image_set0//; constructor]. Qed. -Lemma setCU_R_Rbar (A : set R) (B : set \bar R) : PSoo' B -> - ~` ([set x%:E | x in A] `|` B) = - [set x%:E | x in ~` A] `|` [set -oo%E; +oo%E] `&` ~` B. +Lemma setCU_R_Rbar (A : set R) (B : set \bar R) : ps_infty B -> + ~` ([set x%:E | x in A] `|` B) = [set x%:E | x in ~` A] `|` [set -oo%E; +oo%E] `&` ~` B. Proof. -move=> PSoo'B; rewrite setCU. +move=> ps_inftyB; rewrite setCU. have -> : ~` [set x%:E | x in A] = [set x%:E | x in ~` A] `|` [set -oo; +oo]%E. rewrite predeqE => -[x| |]; split. - by move=> Ax; left; exists x => //; apply: contra_not Ax => Ax; exists x. @@ -4488,42 +4417,36 @@ have -> : ~` [set x%:E | x in A] = [set x%:E | x in ~` A] `|` [set -oo; +oo]%E. rewrite setIUl; congr (_ `|` _). rewrite predeqE => -[x| |]; split; try by case. move=> [] x' Ax' [] <-{x}; split; first by exists x'. -by case: PSoo'B => // -[]. +by case: ps_inftyB => // -[]. Qed. -Lemma measurableRbarC (X : set \bar R) : - measurableRbar X -> measurableRbar (~` X). +Lemma measurableRbarC (X : set \bar R) : measurableRbar X -> measurableRbar (~` X). Proof. move => -[A mA] [B PooB <-]; rewrite setCU_R_Rbar //. -exists (~` A); first exact: measurableC. -exists ([set -oo%E; +oo%E] `&` ~` B) => //. +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]. - by constructor. + 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]. - by constructor. + have [_ ->] := @setDidPl (\bar R) [set -oo%E] [set +oo%E]; first by constructor. by rewrite predeqE => x; split => // -[->]. - by rewrite setICr; constructor. Qed. Lemma measurableRbar_bigcup (F : (set \bar R)^nat) : - (forall i, measurableRbar (F i)) -> - measurableRbar (\bigcup_i (F i)). + (forall i, measurableRbar (F i)) -> measurableRbar (\bigcup_i (F i)). Proof. -move=> mF. -pose P := fun i j => measurable j.1 /\ PSoo' j.2 /\ - F i = [set x%:E | x in j.1] `|` j.2. +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: measurable_bigcup => i; exact: (fi i).1. exists (\bigcup_i (f i).2). - apply/PSoo'P => x [n _] fn2x. - have /PSoo'P : PSoo' (f n).2 by have [_ []] := fi n. + apply/ps_inftyP => x [n _] fn2x. + have /ps_inftyP : ps_infty(f n).2 by have [_ []] := fi n. exact. rewrite [RHS](@eqbigcup_r _ _ _ _ (fun i => [set x%:E | x in (f i).1] `|` (f i).2)); last first. @@ -4536,146 +4459,150 @@ Qed. Definition Rbar_isMeasurable : isMeasurable \bar R := isMeasurable.Build _ measurableRbar0 measurableRbarC measurableRbar_bigcup. -HB.instance (\bar (Real.sort R)) Rbar_isMeasurable. +End salgebra_Rbar. + +Section puncture_ereal_itv. +Variable R : realDomainType. + +Lemma punct_eitv_coo (y : R) : + [set x | (y%:E <= x)%E] = [set x%:E | x in set_of_itv `[y, +oo[] `|` [set +oo%E]. +Proof. +rewrite predeqE => x; split => [|[[z /set_of_itv_mem /itvP yz] <-{x}|->]]/=. + move: x => []; [move=>x yx|by right|by []]. + by left => /=; exists x => //; apply/set_of_itv_mem; rewrite in_itv /= andbT -lee_fin. +by rewrite lee_fin yz. +by rewrite lee_pinfty. +Qed. + +End puncture_ereal_itv. + +Section salgebra_R_ssets. +Variable R : realType. + +Fail Check forall (T : measurableType) (f : T -> R), measurable_fun setT f. + +Definition measurableTypeR := + g_measurableType (@measurable (@sset_algebraOfSetsType R)). + +Definition measurableR : set (set R) := @measurable measurableTypeR. + +HB.instance Definition R_isMeasurable : isMeasurable R := + isMeasurable.Build measurableTypeR + measurable0 (@measurableC _) (@measurable_bigcup _). +(*HB.instance (Real.sort R) R_isMeasurable.*) + +Check forall (T : measurableType) (f : T -> R), measurable_fun setT f. + +Lemma measurable_set1 (r : R) : measurable [set r]. +Proof. +apply: g_salgebra_self => /=; exists [:: `[r, r]] => //=. +rewrite /sset /= big_cons /= big_nil setU0 /= set_of_itv_closed_closed //. +rewrite predeqE => t; split => [<-|]. + by rewrite lexx. +by rewrite -eq_le => /eqP <-. +Qed. + +Lemma measurable_itv (i : interval R) : measurable (set_of_itv i). +Proof. exact/g_salgebra_self/measurable_sset_itv. Qed. + +HB.instance Definition _ := Rbar_isMeasurable (@measurable (@sset_algebraOfSetsType R)). +(*HB.instance (\bar (Real.sort R)) (Rbar_isMeasurable (@measurable (@sset_algebraOfSetsType R))).*) Check forall (T : measurableType) (f : T -> \bar R), measurable_fun setT f. -Lemma measurable_EFin (A : set R) : measurable A -> measurable (@EFin _ @` A). +Lemma measurable_EFin (A : set R) : measurableR A -> measurable (@EFin _ @` A). Proof. -move=> mA. -exists A => //. -exists set0. +move=> mA; exists A => //; exists set0. by constructor. by rewrite setU0. Qed. +Lemma measurable_Rbar_set1 (x : \bar R) : measurable [set x]. +Proof. +case: x => [r| |]. +- by rewrite -image_set1; exact/measurable_EFin/measurable_set1. +- exists set0; [exact: measurable0|exists [set +oo%E]; [by constructor|]]. + by rewrite image_set0 set0U. +- exists set0; [exact: measurable0|exists [set -oo%E]; [by constructor|]]. + by rewrite image_set0 set0U. +Qed. + Lemma measurable_coo (y : \bar R) : measurable [set x | (y <= x)%E]. Proof. move: y => [y| |]. - exists (set_of_itv `[y, +oo[). - exact: measurable_itv. - exists [set +oo%E]. - by constructor. - (* TODO: lemma? *) - rewrite predeqE => x; split => [[[z /set_of_itv_mem /itvP yz] <-{x}|->]|]/=. - by rewrite lee_fin yz. - by rewrite lee_pinfty. - move: x => [x yx|_|//]. - by left => /=; exists x => //; apply/set_of_itv_mem; rewrite in_itv /= andbT -lee_fin. - by right. -(* TODO: lemma? *) -rewrite [X in measurable X](_ : _ = [set +oo]%E). - (* TODO: lemma? *) - rewrite /measurable /= /measurableRbar /=. - exists set0. - exact: measurable0. - exists [set +oo%E]. - by constructor. - by rewrite image_set0 set0U. -rewrite predeqE => t; split => /=. - by rewrite lee_pinfty_eq => /eqP ->. -by move=> <-. -rewrite [X in measurable X](_ : _ = setT). +- exists (set_of_itv `[y, +oo[); first exact: measurable_itv. + by exists [set +oo%E]; [constructor|rewrite -punct_eitv_coo]. +- rewrite [X in measurable X](_ : _ = [set +oo]%E); last first. + by rewrite predeqE => t; split => /= [|<-//]; rewrite lee_pinfty_eq => /eqP ->. + exact: measurable_Rbar_set1. +- rewrite [X in measurable X](_ : _ = setT); last first. + by rewrite predeqE => t; split => //= _; rewrite lee_ninfty. exact: measurableT. -rewrite predeqE => t; split => //= _. -by rewrite lee_ninfty. +Qed. + +Lemma measurable_ooo (y : \bar R) : measurable [set x | (x < y)%E]. +Proof. +rewrite [X in measurable X](_ : _ = ~` [set x | (y <= x)%E]); last first. + (* NB: lemma? *) + rewrite predeqE => x; split => [/= xy|/= /negP]; last by rewrite -ltNge. + by apply/negP; rewrite -ltNge. +exact/measurableC/measurable_coo. Qed. Definition ereal_lebesgue_measure' : set \bar R -> \bar R := fun S : set \bar R => lebesgue_measure R ((real_of_extended @` (S `\` [set -oo; +oo]%E))). Lemma ereal_lebesgue_measure'0 : ereal_lebesgue_measure' set0 = 0%E. -Proof. -by rewrite /ereal_lebesgue_measure' set0D image_set0 measure0. -Qed. +Proof. by rewrite /ereal_lebesgue_measure' set0D image_set0 measure0. Qed. -(* TODO: move *) -Lemma measurable_set1 (r : R) : measurable [set r]. +Lemma measurable_real_of_extended (X : set \bar R) : measurable X -> + measurable [set real_of_extended x | x in X `\` [set -oo%E; +oo%E]]. Proof. -apply: g_salgebra_self => /=. -exists [:: `[r, r]] => //=. -rewrite /sset /= big_cons /= big_nil setU0 /=. -rewrite set_of_itv_closed_closed // predeqE => t; split => [<-|]. - by rewrite lexx. -by rewrite -eq_le => /eqP <-. -Qed. - -Lemma ereal_lebesgue_measure'_ge0 : forall x, measurable x -> (0 <= ereal_lebesgue_measure' x)%E. -Proof. -move=> /= X mX; rewrite /ereal_lebesgue_measure'. -apply: measure_ge0. -case: mX => Y mY [_ []]. +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}/= _ <-//]]]. - move=> Yr; exists r%:E; split; last by case. - by exists r. -- move=> <-{X}. - rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. + 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). - move=> Yr; exists r%:E => //; split; last by case. - by left; exists r. -- move=> <-{X}. - rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. + 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). - move=> Yr; exists r%:E => //; split; last by case. - by left; exists r. -- move=> <-{X}. - rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. - move=> [x [[[x' Yx' <-{x} _ <-//]|]]]. - move=> [|] ->. - by rewrite not_orP => -[]/(_ erefl). - by rewrite not_orP => -[_]/(_ erefl). - move=> Yr; exists r%:E => //; split; last by case. - by left; exists r. + 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 ereal_lebesgue_measure'_ge0 X : measurable X -> (0 <= ereal_lebesgue_measure' X)%E. +Proof. by move=> /= mX; exact/measure_ge0/measurable_real_of_extended. Qed. + Lemma semi_sigma_additive_ereal_lebesgue_measure' : semi_sigma_additive ereal_lebesgue_measure'. Proof. move=> /= F mF tF mUF. rewrite /ereal_lebesgue_measure'. -pose tmp := \bigcup_n [set real_of_extended x | x in F n `\` [set -oo%E; +oo%E]]. -rewrite [X in lebesgue_measure _ X](_ : _ = tmp); last first. +rewrite [X in lebesgue_measure _ X](_ : _ = + \bigcup_n [set real_of_extended x | x in F n `\` [set -oo%E; +oo%E]]); last first. rewrite predeqE => r; split. - move=> [x [[n _ Fnx xoo <-]]]. - by exists n => //; exists x. - move=> [n _ [x [Fnx xoo <-{r}]]]. - by exists x => //; split => //; exists n. -have := @measure_semi_sigma_additive _ _ (@lebesgue_measure R) (fun n => real_of_extended @` (F n `\` [set -oo;+oo]%E)). -apply. + 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 => real_of_extended @` (F n `\` [set -oo;+oo]%E))). - move=> n. have := mF n. move=> [X mX [X' mX']] XX'Fn. - case: mX' XX'Fn => /=. - + rewrite setU0 => <-. - rewrite [X in measurable X](_ : _ = X) //. - rewrite predeqE => r; split. - by move=> -[x [[x' Xx' <-{x} _ <-//]]]. - move=> Xr; exists r%:E => //; split; last by case. - by exists r. - + move=> <-. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split. - move=> [x [[[x' Xx' <-{x} _ <- //]|]]]. - by move=> ->; rewrite not_orP => -[]/(_ erefl). - move=> Xr; exists r%:E => //; split; last by case. - by left; exists r. - - move=> <-. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split. - move=> [x [[[x' Xx' <-{x} _ <-//]|]]]. - by move=> ->; rewrite not_orP => -[_]/(_ erefl). - move=> Xr; exists r%:E; split; last by case. - by left; exists r. - - move=> <-. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split. - move=> [x [[[x' Xx' <-{x} _ <-//]|]]]. - move=> [|] ->; rewrite not_orP => -[]. - by move=> /(_ erefl). - by move=> _ => /(_ erefl). - move=> Xr; exists r%:E => //; split; last by case. - by left; exists r. + apply: measurable_real_of_extended. + rewrite -XX'Fn. + apply: measurableU. + exact: measurable_EFin. + case: mX'. + exact: measurable0. + exact: measurable_Rbar_set1. + exact: measurable_Rbar_set1. + by apply: measurableU; exact: measurable_Rbar_set1. - 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. @@ -4693,39 +4620,35 @@ apply. - move: mUF. rewrite {1}/measurable /= /measurableRbar => -[X mX [Y []]] {Y}. - rewrite setU0 => h. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split. + 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' <-]. - move=> Xr. 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. + rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. move=> -[n _ [x [Fnx xoo <-]]]. have : (\bigcup_n F n) x by exists n. rewrite -h => -[[x' Xx' <-//]|xoo']. by exfalso; apply xoo; left. - move=> Xr. have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r. by exists n => //; exists r%:E => //; split => //; case. - - (* TODO: almost the same as the previous one, factorize*) + - (* NB: almost the same as the previous one, factorize?*) move=> h. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split. + rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. move=> -[n _ [x [Fnx xoo <-]]]. have : (\bigcup_n F n) x by exists n. rewrite -h => -[[x' Xx' <-//]|xoo']. by exfalso; apply xoo; right. - move=> Xr. 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. + rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. move=> -[n _ [x [Fnx xoo <-]]]. have : (\bigcup_n F n) x by exists n. rewrite -h => -[[x' Xx' <-//]|xoo']. by exfalso; apply xoo; right. - move=> Xr. have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r. by exists n => //; exists r%:E => //; split => //; case. Qed. @@ -4738,4 +4661,139 @@ Definition ereal_lebesgue_measure_isMeasure : is_measure ereal_lebesgue_measure' Definition ereal_lebesgue_measure : {measure set \bar R -> \bar R} := Measure.Pack _ ereal_lebesgue_measure_isMeasure. -End sigma_algebra_R_Rbar. +(* NB: comes from simple_function.v *) +Lemma measurable_fcoo (T : measurableType) (f : T -> \bar R) + (y : \bar R) : + measurable_fun setT f -> measurable [set x | (y <= f x)%E]. +Proof. +move=> mf. +rewrite (_ : [set x | (y <= f x)%E] = f @^-1` [set x | (y <= x)%E]) //. +by rewrite -[X in measurable X]setIT; exact/mf/measurable_coo. +Qed. + +Lemma measurable_fooo (T : measurableType) (f : T -> \bar R) + (y : \bar R) : + measurable_fun setT f -> measurable [set x | (f x < y)%E]. +Proof. +move=> mf. +rewrite (_ : [set x | (f x < y)%E] = f @^-1` [set x | (x < y)%E]) //. +by rewrite -[X in measurable X]setIT; exact/mf/measurable_ooo. +Qed. + +End salgebra_R_ssets. + +(* NB : move? *) +Lemma open_lt_lt (R : realType) (a b : R) : open (fun x : [topologicalType of R^o] => a < x < b). +Proof. +have [ab|ba] := ltP a b. + rewrite (_ : (fun _ => _) = [set x | a < x] `&` [set x | x < b]). + by apply openI; [exact: open_gt|exact: open_lt]. + by rewrite predeqE => x; split=> [/andP[ax xb] //|[-> ->]]. +rewrite (_ : (fun _ => _) = set0) // predeqE => x; split => // /andP[ax xb]. +by have := lt_trans ax xb; rewrite ltNge ba. +Qed. + +(* theorem 3.5, lemmas 3.6, 3.7, 3.8 *) +Arguments preimage : simpl never. + +Section measurability. + +Lemma subset_g_salgebra (aT : Type) (A B : set (set aT)) : A `<=` B -> + s<< A >> `<=` s<< B >>. +Proof. +move=> AB; apply: g_salgebra_smallest; first exact: measurableP_g_salgebra. +by move=> C AC; exact/g_salgebra_self/AB. +Qed. + +Definition preimage_class (aT rT : Type) (f : aT -> rT) (CC : set (set rT)) : set (set aT) := + [set f @^-1` C | C in CC]. + +Lemma preimage_class_is_salgebra (aT : Type) (rT : measurableType) (f : aT -> rT) : + measurableP (preimage_class f (@measurable rT)). +Proof. +split. +- by exists set0 => //; exact: measurable0. +- move=> A; rewrite /preimage_class /= => -[B mB <-{A}]. + exists (~` B). + exact: measurableC. + by rewrite preimage_setC. +- move=> F; rewrite /preimage_class /= => mF. + have {}mF : forall n : nat, exists x : set rT, Builders_10.Super.measurable x /\ f @^-1` x = F n. + by move=> n; have := mF n => -[B mB <-]; by exists B. + have [G mG] := @choice _ _ (fun x y => measurable y /\ f @^-1` y = F x) mF. + exists (\bigcup_k (G k)). + apply: measurable_bigcup => n. + exact: (mG n).1. + rewrite preimage_bigcup; apply eqbigcup_r => i _. + exact: (mG i).2. +Qed. + +Definition sigma_fun (aT : Type) (rT : Type) (f : aT -> rT) (CC : set (set aT)) : set (set rT) := + [set B : set rT | (s<< CC >>) (f @^-1` B) ]. + +Lemma fun_generated_salgebra (aT : Type) (rT : Type) (f : aT -> rT) + (CC : set (set aT)) : measurableP CC -> measurableP (sigma_fun f CC). +Proof. +move=> [H1 H2 H3]; split; rewrite /sigma_fun. +- by rewrite /= preimage_set0; apply g_salgebra_set0. +- by move=> A /= CCfA; rewrite -preimage_setC; exact: g_salgebra_setC. +- by move=> F /= mF; rewrite preimage_bigcup; exact: g_salgebra_bigcup. +Qed. + +Lemma transfer (aT : Type) (rT : measurableType) (f : aT -> rT) (CC : set (set rT)) : + @measurable (g_measurableType CC) = @measurable rT -> + @measurable (g_measurableType (preimage_class f CC)) = + preimage_class f (@measurable (g_measurableType CC)). +Proof. +move=> CC_rT. +rewrite eqEsubset; split. + have H1 : measurableP (preimage_class f (@measurable (g_measurableType CC))). + rewrite CC_rT. (*NB: blind rewrite*) + by apply: preimage_class_is_salgebra. + have H2 : preimage_class f CC `<=` preimage_class f (@measurable (g_measurableType CC)). + move=> A [B CCB <-{A}]. + exists B => //. + by apply g_salgebra_self. + have : @measurable (g_measurableType (preimage_class f CC)) `<=` + preimage_class f (@measurable (g_measurableType CC)). + by apply: g_salgebra_smallest. + exact. +set If := sigma_fun f (@measurable (g_measurableType (preimage_class f CC))). +have mPIf : measurableP If. + apply: fun_generated_salgebra. + exact: measurableP_g_salgebra. +have H2 : CC `<=` If. + move=> A' CCA'. + apply: g_salgebra_self. + apply: g_salgebra_self. + by exists A'. +have H3 : s<< CC >> `<=` If. + exact: g_salgebra_smallest. +move=> A [B mV <-{A}]. +rewrite /measurable /= in mV. +rewrite /measurable /=. +(* TODO: lemma *) +have := H3 _ mV; rewrite /If /sigma_fun /= => fB. +rewrite g_salgebraE => AA /= [mAA fCCAA]. +rewrite g_salgebraE in fB; apply: fB => //=; split => //. +by apply: g_salgebra_smallest. +Qed. + +Lemma measurability (aT rT : measurableType) (f : aT -> rT) (CC : set (set rT)) : + CC `<=` @measurable rT -> + s<< CC >> = @measurable rT -> + (preimage_class f CC `<=` @measurable aT) -> + measurable_fun setT f. +Proof. +move=> CC_rT sCC_rT fCC_aT. +suff H1 : preimage_class f (@measurable rT) `<=` @measurable aT. + by move=> A mA; rewrite setIT; apply H1; exists A. +rewrite -[in X in X `<=` _]sCC_rT. +rewrite -[in X in X `<=` _]transfer; last first. + by rewrite -sCC_rT. +rewrite -[X in _ `<=` X]measurable_g_measurableTypeE //; last first. + exact: measurableP_measurable. +exact: subset_g_salgebra. +Qed. + +End measurability.