From 8d95107d2031aa99b4da8a09d864acbc5faae87d Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Wed, 5 Jun 2024 15:45:24 +0900 Subject: [PATCH] sigma-rings (#1222) sigma-rings Co-authored-by: @TheoWinterhalter Co-authored-by: @JeremyDubut Co-authored-by: @AkihisaYamada Co-authored-by: @proux01 --- CHANGELOG_UNRELEASED.md | 102 +++ classical/classical_sets.v | 25 + theories/charge.v | 11 +- theories/kernel.v | 2 +- theories/lebesgue_integral.v | 70 +- theories/lebesgue_measure.v | 50 +- theories/lebesgue_stieltjes_measure.v | 2 +- theories/measure.v | 878 +++++++++++++++++++------- theories/probability.v | 3 +- theories/sequences.v | 38 +- 10 files changed, 845 insertions(+), 336 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d263e8a11..72f18a1b0 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -33,6 +33,29 @@ - in `normedtype.v`: + lemma `not_near_at_leftP` +- in `classical_sets.v`: + + lemmas `setD_bigcup`, `nat_nonempty` + + hint `nat_nonempty` + +- in `measure.v`: + + structure `SigmaRing`, notation `sigmaRingType` + + factory `isSigmaRing` + + lemma `bigcap_measurable` for `sigmaRingType` + + lemma `setDI_semi_setD_closed` + + lemmas `powerset_lambda_system`, `lambda_system_smallest`, `sigmaRingType_lambda_system` + + definitions `niseq_closed`, `sigma_ring` (notation `<>`), + `monotone` (notation `<>`) + + lemmas `smallest_sigma_ring`, `sigma_ring_monotone`, `g_sigma_ring_monotone`, + `sub_g_sigma_ring`, `setring_monotone_sigma_ring`, `g_monotone_monotone`, + `g_monotone_setring`, `g_monotone_g_sigma_ring`, `monotone_setring_sub_g_sigma_ring` + +- in `classical_sets.v`: + + lemma `bigcup_bigsetU_bigcup` + + lemmas `setDUD`, `setIDAC` + +- in `measure.v`: + + lemmas `powerset_sigma_ring`, `g_sigma_ring_strace`, `setI_g_sigma_ring`, + `subset_strace` - in `lebesgue_measure.v`: + lemma `measurable_fun_ler` @@ -74,6 +97,9 @@ - in `Rstruct.v`: + lemma `IZRposE` +- in `measure.v`: + + lemma `strace_sigma_ring` + ### Changed - in `forms.v`: @@ -86,6 +112,28 @@ - in `measure.v`: + change the hypothesis of `measurable_fun_bool` + + mixin `AlgebraOfSets_isMeasurable` renamed to `hasMeasurableCountableUnion` + and made to inherit from `SemiRingOfSets` + +- in `measure.v`: + + rm hypo and variable in lemma `smallest_monotone_classE` + and rename to `smallest_lambda_system` + + rm hypo in lemma `monotone_class_g_salgebra` and renamed + to `g_salgebra_lambda_system` + + rm hypo in lemma `monotone_class_subset` and renamed to + `lambda_system_subset` + + notation `<>` changed to `<>`, + notation `<>` changed to `<>` + +- moved from `lebesgue_measure.v` to `measure.v`: + + definition `strace` + + lemma `sigma_algebra_strace` + +- in `sequences.v`: + + equality reversed in lemma `eq_bigcup_seqD` +- in `sequences.v`: + + `eq_bigsetU_seqD` renamed to `nondecreasing_bigsetU_seqD` + and equality reversed ### Renamed @@ -135,10 +183,23 @@ + `num_lte_maxl` -> `num_gte_max` + `num_lte_minr` -> `num_lte_min` + `num_lte_minl` -> `num_gte_min` +- in `measure.v`: + + `bigcap_measurable` -> `bigcap_measurableType` - in `lebesgue_integral.v`: + `integral_measure_add` -> `ge0_integral_measure_add` + `integral_pushforward` -> `ge0_integral_pushforward` +- in `measure.v`: + + `monotone_class` -> `lambda_system` + + `monotone_class_g_salgebra` -> `g_sigma_algebra_lambda_system` + + `smallest_monotone_classE` -> `smallest_lambda_system` + + `dynkin_monotone` -> `dynkin_lambda_system` + + `dynkin_g_dynkin` -> `g_dynkin_dynkin` + + `salgebraType` -> `g_sigma_algebraType` + + `g_salgebra_measure_unique_trace` -> `g_sigma_algebra_measure_unique_trace` + + `g_salgebra_measure_unique_cover` -> `g_sigma_algebra_measure_unique_cover` + + `g_salgebra_measure_unique` -> `g_sigma_algebra_measure_unique` + + `setI_closed_gdynkin_salgebra` -> `setI_closed_g_dynkin_g_sigma_algebra` ### Generalized @@ -165,6 +226,45 @@ - in `probability.v`: + lemma `markov` +- in `measure.v`: + + from `measurableType` to `sigmaRingType` + * lemmas `bigcup_measurable`, `bigcapT_measurable` + * definition `measurable_fun` + * lemmas `measurable_id`, `measurable_comp`, `eq_measurable_fun`, `measurable_cst`, + `measurable_fun_bigcup`, `measurable_funU`, `measurable_funS`, `measurable_fun_if` + * lemmas `semi_sigma_additiveE`, `sigma_additive_is_additive`, `measure_sigma_additive` + * definitions `pushforward`, `dirac` + * lemmas `diracE`, `dirac0`, `diracT`, `finite_card_sum`, `finite_card_dirac`, `infinite_card_dirac` + * definitions `msum`, `measure_add`, `mscale`, `mseries`, `mrestr` + * lemmas `msum_mzero`, `measure_addE` + * definition `sfinite_measure` + * mixin `isSFinite`, structure `SFiniteMeasure` + * structure `FiniteMeasure` + * factory `Measure_isSFinite` + * lemma `negligible_bigcup` + * definition `ae_eq` + * lemmas `ae_eq0`, `ae_eq_comp`, `ae_eq_funeposneg`, `ae_eq_refl`, `ae_eq_sym`, + `ae_eq_trans`, `ae_eq_sub`, `ae_eq_mul2r`, `ae_eq_mul2l`, `ae_eq_mul1l`, + `ae_eq_abse`, `ae_eq_subset` + + from `measurableType` to `sigmaRingType` and from `realType` to `realFieldType` + * definition `mzero` + + from `realType` to `realFieldType`: + * lemma `sigma_finite_mzero` + +- in `lebesgue_integral.v`: + + from `measurableType` to `sigmaRingType` + * mixin `isMeasurableFun` + * structure `SimpleFun` + * structure `NonNegSimpleFun` + * sections `fimfun_bin`, `mfun_pred`, `sfun_pred`, `simple_bounded` + * lemmas `nnfun_muleindic_ge0`, `mulemu_ge0`, `nnsfun_mulemu_ge0` + * section `sintegral_lemmas` + * lemma `eq_sintegral` + * section `sintegralrM` + +- in `lebesgue_measure.v`: + + from `measurableType` to `sigmaRingType` + * section `measurable_fun_measurable` ### Deprecated @@ -190,6 +290,8 @@ - in `reals.v` + lemma `inf_lower_bound` (use `inf_lb` instead) +- in `lebesgue_measure.v`: + + lemmas `stracexx`, `strace_measurable` ### Infrastructure diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 0e276a570..0360808c3 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -451,6 +451,10 @@ Notation "`] a , '+oo' [" := Notation "`] -oo , '+oo' [" := [set` Interval -oo%O +oo%O] : classical_set_scope. +Lemma nat_nonempty : [set: nat] !=set0. Proof. by exists 1%N. Qed. + +#[global] Hint Resolve nat_nonempty : core. + Lemma preimage_itv T d (rT : porderType d) (f : T -> rT) (i : interval rT) (x : T) : ((f @^-1` [set` i]) x) = (f x \in i). Proof. by rewrite inE. Qed. @@ -1028,6 +1032,9 @@ Proof. by move=> *; rewrite setUC setUKD. Qed. Lemma setIDA A B C : A `&` (B `\` C) = (A `&` B) `\` C. Proof. by rewrite !setDE setIA. Qed. +Lemma setIDAC A B C : (A `\` B) `&` C = A `&` (C `\` B). +Proof. by rewrite setIC !setIDA setIC. Qed. + Lemma setDD A B : A `\` (A `\` B) = A `&` B. Proof. by rewrite 2!setDE setCI setCK setIUr setICr set0U. Qed. @@ -1043,6 +1050,15 @@ Proof. by rewrite !setDE setCI setIUr. Qed. Lemma setUIDK A B : (A `&` B) `|` A `\` B = A. Proof. by rewrite setUC -setDDr setDv setD0. Qed. +Lemma setDUD A B C : (A `|` B) `\` C = A `\` C `|` B `\` C. +Proof. +apply/seteqP; split=> [x [[Ax|Bx] Cx]|x [[Ax]|[Bx] Cx]]. +- by left. +- by right. +- by split=> //; left. +- by split=> //; right. +Qed. + Lemma setM0 T' (A : set T) : A `*` set0 = set0 :> set (T * T'). Proof. by rewrite predeqE => -[t u]; split => // -[]. Qed. @@ -1922,6 +1938,15 @@ End bigop_lemmas. Arguments bigcup_setD1 {T I} x. Arguments bigcap_setD1 {T I} x. +Lemma setD_bigcup {T} (I : eqType) (F : I -> set T) (P : set I) (j : I) : P j -> + F j `\` \bigcup_(i in [set k | P k /\ k != j]) (F j `\` F i) = + \bigcap_(i in P) F i. +Proof. +move=> Pj; apply/seteqP; split => [t [Fjt UFt] i Pi|t UFt]. + by have [->//|ij] := eqVneq i j; apply: contra_notP UFt => Fit; exists i. +by split=> [|[k [Pk kj]] [Fjt]]; [|apply]; exact: UFt. +Qed. + Definition bigcup2 T (A B : set T) : nat -> set T := fun i => if i == 0 then A else if i == 1 then B else set0. Arguments bigcup2 T A B n /. diff --git a/theories/charge.v b/theories/charge.v index 780a4e063..090a26246 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1177,10 +1177,11 @@ rewrite is_max_approxRNE; apply: measurableI => /=. rewrite -[X in measurable X]setTI. by apply: emeasurable_fun_eq => //; [exact: measurable_max_approxRN_seq| exact: measurable_approxRN_seq]. -rewrite [T in measurable T](_ : _ = \bigcap_(k in `I_j) [set x | g_ k x < g_ j x])//. -apply: bigcap_measurable => k _. -rewrite -[X in measurable X]setTI; apply: emeasurable_fun_lt => //; -exact: measurable_approxRN_seq. +rewrite [T in measurable T](_ : _ = + \bigcap_(k in `I_j) [set x | g_ k x < g_ j x])//. +apply: bigcap_measurableType => k _. +by rewrite -[X in measurable X]setTI; apply: emeasurable_fun_lt => //; + exact: measurable_approxRN_seq. Qed. End approxRN_seq. @@ -1881,7 +1882,7 @@ rewrite -(ae_eq_integral _ _ _ _ _ - apply: emeasurable_funM => //; first exact: measurable_int mf. exact: measurable_funTS. rewrite [in LHS](funeposneg f). -under eq_integral => x xE. rewrite muleBl; last 2 first. +under [in LHS]eq_integral => x xE. rewrite muleBl; last 2 first. - exact: Radon_Nikodym_SigmaFinite.f_fin_num. - exact: add_def_funeposneg. over. diff --git a/theories/kernel.v b/theories/kernel.v index 88b70b7b7..d930e6ca9 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -457,7 +457,7 @@ have CXY : C `<=` XY. rewrite phiM. apply: emeasurable_funM => //; first exact/measurable_kernel/measurableI. by apply/EFin_measurable_fun; rewrite (_ : \1_ _ = mindic R mA). -suff monoB : monotone_class setT XY by exact: monotone_class_subset. +suff lsystemB : lambda_system setT XY by exact: lambda_system_subset. split => //; [exact: CXY| |exact: xsection_ndseq_closed]. move=> A B BA [mA mphiA] [mB mphiB]; split; first exact: measurableD. suff : phi (A `\` B) = (fun x => phi A x - phi B x). diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 239594f40..0670dfa84 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -100,9 +100,9 @@ Reserved Notation "m1 '\x^' m2" (at level 40, m2 at next level). #[global] Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core. -HB.mixin Record isMeasurableFun d (aT : measurableType d) (rT : realType) +HB.mixin Record isMeasurableFun d (aT : sigmaRingType d) (rT : realType) (f : aT -> rT) := { - measurable_funP : measurable_fun setT f + measurable_funP : measurable_fun [set: aT] f }. HB.structure Definition MeasurableFun d aT rT := {f of @isMeasurableFun d aT rT f}. @@ -119,9 +119,10 @@ Reserved Notation "[ 'mfun' 'of' f ]" (at level 0, format "[ 'mfun' 'of' f ]"). Notation "{ 'mfun' aT >-> T }" := (@MeasurableFun.type _ aT T) : form_scope. Notation "[ 'mfun' 'of' f ]" := [the {mfun _ >-> _} of f] : form_scope. -#[global] Hint Resolve measurable_funP : core. +#[global] Hint Extern 0 (measurable_fun [set: _] _) => + solve [apply: measurable_funP] : core. -HB.structure Definition SimpleFun d (aT : measurableType d) (rT : realType) := +HB.structure Definition SimpleFun d (aT : sigmaRingType d) (rT : realType) := (* HB.structure Definition SimpleFun d (aT (*rT*) : measurableType d) (rT : realType) := *) {f of @isMeasurableFun d aT rT f & @FiniteImage aT rT f}. Reserved Notation "{ 'sfun' aT >-> T }" @@ -135,7 +136,6 @@ Lemma measurable_sfunP {d} {aT : measurableType d} {rT : realType} (f : {mfun aT >-> rT}) (Y : set rT) : measurable Y -> measurable (f @^-1` Y). Proof. by move=> mY; rewrite -[f @^-1` _]setTI; exact: measurable_funP. Qed. - HB.mixin Record isNonNegFun (aT : Type) (rT : numDomainType) (f : aT -> rT) := { fun_ge0 : forall x, 0 <= f x }. @@ -151,7 +151,7 @@ Notation "[ 'nnfun' 'of' f ]" := [the {nnfun _ >-> _} of f] : form_scope. (* HB.structure Definition NonNegSimpleFun d (aT : measurableType d) (rT : realType) := *) HB.structure Definition NonNegSimpleFun - d (aT : measurableType d) (rT : realType) := + d (aT : sigmaRingType d) (rT : realType) := {f of @SimpleFun d _ _ f & @NonNegFun aT rT f}. Reserved Notation "{ 'nnsfun' aT >-> T }" (at level 0, format "{ 'nnsfun' aT >-> T }"). @@ -229,7 +229,7 @@ Lemma trivIset_preimage1_in {aT} {rT : choiceType} (D : set rT) (A : set aT) Proof. by move=> y z _ _ [x [[_ <-] [_ <-]]]. Qed. Section fimfun_bin. -Variables (d : measure_display) (T : measurableType d). +Variables (d : measure_display) (T : sigmaRingType d). Variables (R : numDomainType) (f g : {fimfun T >-> R}). Lemma max_fimfun_subproof : @FiniteImage T R (f \max g). @@ -252,7 +252,7 @@ HB.builders Context T R f of @FiniteDecomp T R f. HB.end. Section mfun_pred. -Context {d} {aT : measurableType d} {rT : realType}. +Context {d} {aT : sigmaRingType d} {rT : realType}. Definition mfun : {pred aT -> rT} := mem [set f | measurable_fun setT f]. Definition mfun_key : pred_key mfun. Proof. exact. Qed. Canonical mfun_keyed := KeyedPred mfun_key. @@ -301,7 +301,7 @@ HB.instance Definition _ := Lemma measurableT_comp_subproof (f : {mfun _ >-> rT}) (g : {mfun aT >-> rT}) : measurable_fun setT (f \o g). -Proof. apply: measurableT_comp. exact. apply: @measurable_funP _ _ _ g. Qed. +Proof. exact: measurableT_comp. Qed. HB.instance Definition _ (f : {mfun _ >-> rT}) (g : {mfun aT >-> rT}) := isMeasurableFun.Build _ _ _ (f \o g) (measurableT_comp_subproof _ _). @@ -388,7 +388,7 @@ Qed. Notation measurable_fun_indic := measurable_indic (only parsing). Section sfun_pred. -Context {d} {aT : measurableType d} {rT : realType}. +Context {d} {aT : sigmaRingType d} {rT : realType}. Definition sfun : {pred _ -> _} := [predI @mfun _ aT rT & fimfun]. Definition sfun_key : pred_key sfun. Proof. exact. Qed. Canonical sfun_keyed := KeyedPred sfun_key. @@ -535,7 +535,7 @@ by rewrite gzf -fxfy addrC subrK. Qed. Section simple_bounded. -Context d (T : measurableType d) (R : realType). +Context d (T : sigmaRingType d) (R : realType). Lemma simple_bounded (f : {sfun T >-> R}) : bounded_fun f. Proof. @@ -632,7 +632,10 @@ Variable f : {nnsfun T >-> R}. Lemma nnsfun_cover : \big[setU/set0]_(i \in range f) (f @^-1` [set i]) = setT. -Proof. by rewrite fsbig_setU//= -subTset => x _; exists (f x). Qed. +Proof. +rewrite fsbig_setU//=; last exact: fimfunP. +by rewrite -subTset => x _; exists (f x). +Qed. Lemma nnsfun_coverT : \big[setU/set0]_(i \in [set: R]) (f @^-1` [set i]) = setT. @@ -648,7 +651,7 @@ End nnsfun_cover. Lemma measurable_sfun_inP {d} {aT : measurableType d} {rT : realType} (f : {mfun aT >-> rT}) D (y : rT) : measurable D -> measurable (D `&` f @^-1` [set y]). -Proof. by move=> Dm; apply: measurableI. Qed. +Proof. by move=> Dm; exact: measurableI. Qed. #[global] Hint Extern 0 (measurable (_ `&` _ @^-1` [set _])) => solve [apply: measurable_sfun_inP; assumption] : core. @@ -696,7 +699,7 @@ move=> A0 xA /=; have [x0|x0] := ltP x 0%R; first by rewrite (xA x0) mule0. by rewrite mule_ge0. Qed. -Lemma nnfun_muleindic_ge0 d (T : measurableType d) (R : realDomainType) +Lemma nnfun_muleindic_ge0 d (T : sigmaRingType d) (R : realDomainType) (f : {nnfun T >-> R}) r z : 0 <= r%:E * (\1_(f @^-1` [set r]) z)%:E. Proof. apply: (@mulef_ge0 _ _ (fun r => (\1_(f @^-1` [set r]) z)%:E)). @@ -704,7 +707,7 @@ apply: (@mulef_ge0 _ _ (fun r => (\1_(f @^-1` [set r]) z)%:E)). by move=> r0; rewrite preimage_nnfun0// indic0. Qed. -Lemma mulemu_ge0 d (T : measurableType d) (R : realType) +Lemma mulemu_ge0 d (T : sigmaRingType d) (R : realType) (mu : {measure set T -> \bar R}) x (A : R -> set T) : ((x < 0)%R -> A x = set0) -> 0 <= x%:E * mu (A x). Proof. @@ -712,12 +715,13 @@ by move=> xA; rewrite (@mulef_ge0 _ _ (mu \o _))//= => /xA ->; rewrite measure0. Qed. Global Arguments mulemu_ge0 {d T R mu x} A. -Lemma nnsfun_mulemu_ge0 d (T : measurableType d) (R : realType) +Lemma nnsfun_mulemu_ge0 d (T : sigmaRingType d) (R : realType) (mu : {measure set T -> \bar R}) (f : {nnsfun T >-> R}) x : 0 <= x%:E * mu (f @^-1` [set x]). Proof. by apply: (mulemu_ge0 (fun x => f @^-1` [set x])); exact: preimage_nnfun0. Qed. + End mulem_ge0. (** Definition of Simple Integrals *) @@ -738,7 +742,7 @@ End simple_fun_raw_integral. solve [apply: measure_ge0] : core. Section sintegral_lemmas. -Context d (T : measurableType d) (R : realType). +Context d (T : sigmaRingType d) (R : realType). Variable mu : {measure set T -> \bar R}. Local Open Scope ereal_scope. @@ -781,15 +785,15 @@ Qed. End sintegral_lemmas. -Lemma eq_sintegral d (T : measurableType d) (R : numDomainType) - (mu : set T -> \bar R) g f : - f =1 g -> sintegral mu f = sintegral mu g. +Lemma eq_sintegral d (T : sigmaRingType d) (R : numDomainType) + (mu : set T -> \bar R) g f : + f =1 g -> sintegral mu f = sintegral mu g. Proof. by move=> /funext->. Qed. Arguments eq_sintegral {d T R mu} g. Section sintegralrM. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). +Context d (T : sigmaRingType d) (R : realType). Variables (m : {measure set T -> \bar R}) (r : R) (f : {nnsfun T >-> R}). Lemma sintegralrM : sintegral m (cst r \* f)%R = r%:E * sintegral m f. @@ -1850,7 +1854,7 @@ pose K := \bigcap_i gK i; have mgK n : measurable (gK n). have mK : measurable K by exact: bigcap_measurable. have Kab : K `<=` A by move=> z /(_ O I); have [_ + _ _] := gKP O; apply. have []// := @pointwise_almost_uniform _ rT R mu g_ f K (eps%:num / 2). -- by move=> n; exact: measurable_funTS. +- by move=> n; apply: measurable_funTS. - exact: (measurable_funS _ Kab). - by rewrite (@le_lt_trans _ _ (mu A))// le_measure// ?inE. - by move=> z Kz; have /fine_fcvg := gf' z (Kab _ Kz); rewrite -fmap_comp compA. @@ -1973,7 +1977,6 @@ Lemma ge0_emeasurable_fun_sum D (h : nat -> (T -> \bar R)) (P : pred nat) : (forall k x, D x -> P k -> 0 <= h k x) -> (forall k, P k -> measurable_fun D (h k)) -> measurable_fun D (fun x => \sum_(i h0 mh. move=> mD; move: (mD). apply/(@measurable_restrict _ _ _ _ _ setT) => //. @@ -2031,7 +2034,7 @@ wlog fg : D mD mf mg mfg / forall x, D x -> f x *? g x => [hwlogM|]; last first. move=> A mA; wlog NA0: A mD mf mg mA / ~ (A 0) => [hwlogA|]. have [] := pselect (A 0); last exact: hwlogA. move=> /(@setD1K _ 0)<-; rewrite preimage_setU setIUr. - apply: measurableU; last by apply: hwlogA=> //; [exact: measurableD|case => /=]. + apply: measurableU; last by apply: hwlogA=> //; [exact: measurableD|case=>/=]. have -> : (fun x => f x * g x) @^-1` [set 0] = f @^-1` [set 0] `|` g @^-1` [set 0]. apply/seteqP; split=> x /= => [/eqP|[]]; rewrite /preimage/=. @@ -2457,7 +2460,7 @@ rewrite [LHS]ge0_integral_fsum//; last 2 first. - by move=> r; exact/EFin_measurable_fun/measurableT_comp. - by move=> n x _; rewrite EFinM nnfun_muleindic_ge0. rewrite -[RHS]ge0_integralZl//; last 2 first. - - exact/EFin_measurable_fun/measurable_funTS. + - by apply: measurableT_comp => //; exact: measurable_funTS. - by move=> x _; rewrite lee_fin. under [RHS]eq_integral. move=> x xD; rewrite fimfunE -fsumEFin// ge0_mule_fsumr; last first. @@ -2480,7 +2483,7 @@ move=> f0; have [f_ [ndf_ f_f]] := approximation mD mf f0. transitivity (limn (fun n => \int[mscale k m]_(x in D) (f_ n x)%:E)). rewrite -monotone_convergence//=. - by apply: eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //=; exact: f_f. - - by move=> n; exact/EFin_measurable_fun/measurable_funTS. + - by move=> n; apply: measurableT_comp => //; exact: measurable_funTS. - by move=> n x _; rewrite lee_fin. - by move=> x _ a b /ndf_ /lefP; rewrite lee_fin. rewrite (_ : \int[m]_(x in D) _ = @@ -4650,7 +4653,7 @@ have CB : C `<=` B. have [xX1|xX1] := boolP (x \in X1); first by rewrite mule1 in_xsectionM. by rewrite mule0 notin_xsectionM// set0I measure0. exact/measurable_funeM/EFin_measurable_fun. -suff monoB : monotone_class setT B by exact: monotone_class_subset. +suff lsystemB : lambda_system setT B by exact: lambda_system_subset. split => //; [exact: CB| |exact: xsection_ndseq_closed]. move=> X Y XY [mX mphiX] [mY mphiY]; split; first exact: measurableD. have -> : phi (X `\` Y) = (fun x => phi X x - phi Y x)%E. @@ -4691,7 +4694,7 @@ have CB : C `<=` B. have [yX2|yX2] := boolP (y \in X2); first by rewrite mule1 in_ysectionM. by rewrite mule0 notin_ysectionM// set0I measure0. exact/measurable_funeM/EFin_measurable_fun. -suff monoB : monotone_class setT B by exact: monotone_class_subset. +suff lsystemB : lambda_system setT B by exact: lambda_system_subset. split => //; [exact: CB| |exact: ysection_ndseq_closed]. move=> X Y XY [mX mphiX] [mY mphiY]; split; first exact: measurableD. rewrite (_ : psi _ = (psi X \- psi Y)%E); first exact: emeasurable_funB. @@ -5122,8 +5125,7 @@ have [g [gfe2 ig]] : exists g : {sfun R >-> rT}, split; last exact: intG. have /= := Nb _ (leqnn n); rewrite /ball/= sub0r normrN -fine_abse// -lte_fin. by rewrite fineK ?abse_fin_num// => /le_lt_trans; apply; exact: lee_abs. -have mg : measurable_fun E g. - by apply: (measurable_funS measurableT) => //; exact: measurable_funP. +have mg : measurable_fun E g by exact: measurable_funTS. have [M Mpos Mbd] : (exists2 M, 0 < M & forall x, `|g x| <= M)%R. have [M [_ /= bdM]] := simple_bounded g. exists (`|M| + 1)%R; first exact: ltr_pwDr. @@ -6861,13 +6863,13 @@ rewrite muleA lee_pmul//. by rewrite lebesgue_measure_ball// ltry andbT lte_fin mulrn_wgt0. rewrite fineK; last by rewrite ge0_fin_numE// (nicely_shrinking_lty (hE x)). exact: muEr_. -+ apply: le_trans. - * apply: le_abse_integral => //; first exact: (hE x).1. +- apply: le_trans. + + apply: le_abse_integral => //; first exact: (hE x).1. apply/EFin_measurable_fun; apply/measurable_funB => //. by case: locf => + _ _; exact: measurable_funS. - * apply: ge0_subset_integral => //; first exact: (hE x).1. + + apply: ge0_subset_integral => //; first exact: (hE x).1. exact: measurable_ball. - * apply/EFin_measurable_fun; apply: measurableT_comp => //. + + apply/EFin_measurable_fun; apply: measurableT_comp => //. apply/measurable_funB => //. by case: locf => + _ _; exact: measurable_funS. Unshelve. all: by end_near. Qed. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index f8e1c5b86..8f8c3d2d2 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -349,7 +349,7 @@ End LebesgueMeasure. Definition lebesgue_measure {R : realType} : set [the measurableType _.-sigma of - salgebraType R.-ocitv.-measurable] -> \bar R := + g_sigma_algebraType R.-ocitv.-measurable] -> \bar R := [the measure _ _ of lebesgue_stieltjes_measure [the cumulative _ of idfun]]. HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R). HB.instance Definition _ (R : realType) := @@ -482,7 +482,7 @@ End puncture_ereal_itv. Section salgebra_R_ssets. Variable R : realType. -Definition measurableTypeR := salgebraType (R.-ocitv.-measurable). +Definition measurableTypeR := g_sigma_algebraType (R.-ocitv.-measurable). Definition measurableR : set (set R) := (R.-ocitv.-measurable).-sigma.-measurable. @@ -495,7 +495,7 @@ HB.instance Definition R_isMeasurable : Lemma measurable_set1 (r : R) : measurable [set r]. Proof. -rewrite set1_bigcap_oc; apply: bigcap_measurable => k // _. +rewrite set1_bigcap_oc; apply: bigcap_measurable => // k _. by apply: sub_sigma_algebra; exact/is_ocitv. Qed. #[local] Hint Resolve measurable_set1 : core. @@ -938,7 +938,7 @@ Qed. Section measurable_fun_measurable. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). +Context d (T : sigmaRingType 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. @@ -1242,9 +1242,9 @@ Definition G := [set A : set \bar R | exists r, A = `]r%:E, +oo[%classic]. Lemma measurable_set1Ny : G.-sigma.-measurable [set -oo]. Proof. -rewrite eset1Ny; apply: bigcap_measurable => i _. +rewrite eset1Ny; apply: bigcap_measurable => // i _. rewrite -setCitvr; apply: measurableC; rewrite (eitv_bnd_infty false). -apply: bigcap_measurable => j _; apply: sub_sigma_algebra. +apply: bigcap_measurable => // j _; apply: sub_sigma_algebra. by exists (- (i%:R + j.+1%:R^-1))%R; rewrite opprD. Qed. @@ -1301,9 +1301,9 @@ Qed. Lemma measurable_set1y : G.-sigma.-measurable [set +oo]. Proof. -rewrite eset1y; apply: bigcap_measurable => i _. +rewrite eset1y; apply: bigcap_measurable => // i _. rewrite -setCitvl; apply: measurableC; rewrite (eitv_infty_bnd true). -apply: bigcap_measurable => j _; rewrite -setCitvr; apply: measurableC. +apply: bigcap_measurable => // j _; rewrite -setCitvr; apply: measurableC. by apply: sub_sigma_algebra; exists (i%:R + j.+1%:R^-1)%R. Qed. @@ -1357,38 +1357,6 @@ Qed. End erealgeninftyo. End ErealGenInftyO. -Section trace. -Variable (T : Type). -Implicit Types (G : set (set T)) (A D : set T). - -(* intended as a trace sigma-algebra *) -Definition strace G D := [set x `&` D | x in G]. - -Lemma stracexx G D : G D -> strace G D D. -Proof. by rewrite /strace /=; exists D => //; rewrite setIid. Qed. - -Lemma sigma_algebra_strace G D : - sigma_algebra setT G -> sigma_algebra D (strace G D). -Proof. -move=> [G0 GC GU]; split; first by exists set0 => //; rewrite set0I. -- move=> S [A mA ADS]; have mCA := GC _ mA. - have : strace G D (D `&` ~` A). - by rewrite setIC; exists (setT `\` A) => //; rewrite setTD. - rewrite -setDE => trDA. - have DADS : D `\` A = D `\` S by rewrite -ADS !setDE setCI setIUr setICr setU0. - by rewrite DADS in trDA. -- move=> S mS; have /choice[M GM] : forall n, exists A, G A /\ S n = A `&` D. - by move=> n; have [A mA ADSn] := mS n; exists A. - exists (\bigcup_i (M i)); first by apply GU => i; exact: (GM i).1. - by rewrite setI_bigcupl; apply eq_bigcupr => i _; rewrite (GM i).2. -Qed. - -End trace. - -Lemma strace_measurable d (T : measurableType d) (A : set T) : measurable A -> - strace measurable A `<=` measurable. -Proof. by move=> mA=> _ [C mC <-]; apply: measurableI. Qed. - (* more properties of measurable functions *) Lemma is_interval_measurable (R : realType) (I : set R) : @@ -1795,7 +1763,7 @@ Proof. move=> mf n mD. apply: (measurability (ErealGenCInfty.measurableE R)) => //. move=> _ [_ [x ->] <-]; rewrite einfs_preimage -bigcapIr; last by exists n =>/=. -by apply: bigcap_measurable => ? ?; exact/mf/emeasurable_itv. +by apply: bigcap_measurableType => ? ?; exact/mf/emeasurable_itv. Qed. Lemma measurable_fun_esups D (f : (T -> \bar R)^nat) : diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index e5978362a..4a29cb657 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -510,7 +510,7 @@ Notation wlength_sigma_sub_additive := wlength_sigma_subadditive (only parsing). Section lebesgue_stieltjes_measure. Variable R : realType. -Let gitvs := [the measurableType _ of salgebraType (@ocitv R)]. +Let gitvs := [the measurableType _ of g_sigma_algebraType (@ocitv R)]. Lemma lebesgue_stieltjes_measure_unique (f : cumulative R) (mu : {measure set gitvs -> \bar R}) : diff --git a/theories/measure.v b/theories/measure.v index 3865b1354..25ff40621 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -35,6 +35,8 @@ From HB Require Import structures. (* The HB class is SemiRingOfSets. *) (* ringOfSetsType d == the type of rings of sets *) (* The HB class is RingOfSets. *) +(* sigmaRingType d == the type of sigma-rings (of sets) *) +(* The HB class is SigmaRing. *) (* algebraOfSetsType d == the type of algebras of sets *) (* The HB class is AlgebraOfsets. *) (* measurableType == the type of sigma-algebras *) @@ -50,19 +52,23 @@ From HB Require Import structures. (* discrete_measurable_nat == the measurableType corresponding to *) (* [set: set nat] *) (* setring G == the set of sets G contains the empty set, is *) -(* closed by union, and difference *) +(* closed by union, and difference (it is a ring *) +(* of sets in the sense of ringOfSetsType) *) (* <> := smallest setring G *) (* <> is equipped with a structure of ring *) (* of sets. *) (* G.-ring.-measurable A == A belongs to the ring of sets <> *) -(* sigma_algebra D G == the set of sets G forms a sigma algebra on D *) +(* sigma_ring G == the set of sets G forms a sigma-ring *) +(* <> == sigma-ring generated by G *) +(* := smallest sigma_ring G *) +(* sigma_algebra D G == the set of sets G forms a sigma-algebra on D *) (* <> == sigma-algebra generated by G on D *) (* := smallest (sigma_algebra D) G *) (* <> := <> *) (* <> is equipped with a structure of *) (* sigma-algebra *) (* G.-sigma.-measurable A == A is measurable for the sigma-algebra <> *) -(* salgebraType G == the measurableType corresponding to <> *) +(* g_sigma_algebraType G == the measurableType corresponding to <> *) (* This is an HB alias. *) (* mu .-cara.-measurable == sigma-algebra of Caratheodory measurable sets *) (* ``` *) @@ -183,15 +189,21 @@ From HB Require Import structures. (* setD_closed G == the set of sets G is closed under difference *) (* ndseq_closed G == the set of sets G is closed under non-decreasing *) (* countable union *) +(* niseq_closed G == the set of sets G is closed under non-increasing *) +(* countable intersection *) (* trivIset_closed G == the set of sets G is closed under pairwise-disjoint *) (* countable union *) -(* monotone_class D G == G is a monotone class of subsets of D *) -(* <> == monotone class generated by G on D *) -(* <> := <> *) +(* lambda_system D G == G is a lambda_system of subsets of D *) +(* <> == lambda-system generated by G on D *) +(* <> := <> *) +(* monotone G == G is a monotone class *) +(* <> == monotone class generated by G *) +(* := smallest monotone G *) (* dynkin G == G is a set of sets that form a Dynkin *) -(* (or a lambda) system *) +(* system (or a d-system) *) (* <> == Dynkin system generated by G, i.e., *) (* smallest dynkin G *) +(* strace G D := [set x `&` D | x in G] *) (* ``` *) (* ## Other measure-theoretic definitions *) (* *) @@ -284,10 +296,10 @@ Reserved Notation "mu .-cara.-measurable" (at level 2, format "mu .-cara.-measurable"). Reserved Notation "mu .-caratheodory" (at level 2, format "mu .-caratheodory"). -Reserved Notation "'<>'" - (at level 2, format "'<>'"). -Reserved Notation "'<>'" - (at level 2, format "'<>'"). +Reserved Notation "'<>'" + (at level 2, format "'<>'"). +Reserved Notation "'<>'" + (at level 2, format "'<>'"). Reserved Notation "'<>'" (at level 2, format "'<>'"). Reserved Notation "'<>'" @@ -296,6 +308,10 @@ Reserved Notation "'<>'" (at level 2, format "'<>'"). Reserved Notation "'<>'" (at level 2, format "'<>'"). +Reserved Notation "'<>'" + (at level 2, format "'<>'"). +Reserved Notation "'<>'" + (at level 2, format "'<>'"). Reserved Notation "{ 'content' fUV }" (at level 0, format "{ 'content' fUV }"). Reserved Notation "[ 'content' 'of' f 'as' g ]" (at level 0, format "[ 'content' 'of' f 'as' g ]"). @@ -351,8 +367,18 @@ Definition fin_bigcup_closed := Definition semi_setD_closed := forall A B, G A -> G B -> exists D, [/\ finite_set D, D `<=` G, A `\` B = \bigcup_(X in D) X & trivIset D id]. +Lemma setDI_semi_setD_closed : setDI_closed -> semi_setD_closed. +Proof. +move=> mD A B Am Bm; exists [set A `\` B]; split; rewrite ?bigcup_set1//. + by move=> X ->; apply: mD. +by move=> X Y -> ->. +Qed. + Definition ndseq_closed := - forall F, nondecreasing_seq F -> (forall i, G (F i)) -> G (\bigcup_i (F i)). + forall F, nondecreasing_seq F -> (forall i, G (F i)) -> G (\bigcup_i (F i)). + +Definition niseq_closed := + forall F, nonincreasing_seq F -> (forall i, G (F i)) -> G (\bigcap_i (F i)). Definition trivIset_closed := forall F : (set T)^nat, trivIset setT F -> (forall n, G (F n)) -> @@ -364,25 +390,69 @@ Definition fin_trivIset_closed := Definition setring := [/\ G set0, setU_closed & setDI_closed]. +Definition sigma_ring := [/\ G set0, setDI_closed & + (forall A : (set T)^nat, (forall n, G (A n)) -> G (\bigcup_k A k))]. + Definition sigma_algebra := [/\ G set0, (forall A, G A -> G (D `\` A)) & (forall A : (set T)^nat, (forall n, G (A n)) -> G (\bigcup_k A k))]. Definition dynkin := [/\ G setT, setC_closed & trivIset_closed]. -Definition monotone_class := +(**md Until MathComp-Analysis 1.1.0, the identifier was `monotone_class` +because this definition corresponds to "classe monotone" in several +French references, e.g., the definition of "classe monotone" on the French wikipedia. *) +Definition lambda_system := [/\ forall A, G A -> A `<=` D, G D, setD_closed & ndseq_closed]. +Definition monotone := ndseq_closed /\ niseq_closed. + End classes. +#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `lambda_system`")] +Notation monotone_class := lambda_system (only parsing). -Notation "'<>'" := (smallest (monotone_class D) G) : +Lemma powerset_sigma_ring (T : Type) (D : set T) : + sigma_ring [set X | X `<=` D]. +Proof. +split => //; last first. + by move=> F FA/=; apply: bigcup_sub => i _; exact: FA. +by move=> U V + VA; apply: subset_trans; exact: subDsetl. +Qed. + +Lemma powerset_lambda_system (T : Type) (D : set T) : + lambda_system D [set X | X `<=` D]. +Proof. +split => //. +- by move=> A B BA + BD; apply: subset_trans; exact: subDsetl. +- by move=> /= F _ FD; exact: bigcup_sub. +Qed. + +Notation "'<>'" := (smallest (lambda_system D) G) : classical_set_scope. -Notation "'<>'" := (<>) : classical_set_scope. +Notation "'<>'" := (<>) : classical_set_scope. Notation "'<>'" := (smallest dynkin G) : classical_set_scope. Notation "'<>'" := (smallest (sigma_algebra D) G) : classical_set_scope. Notation "'<>'" := (<>) : classical_set_scope. Notation "'<>'" := (smallest setring G) : classical_set_scope. +Notation "'<>'" := (smallest sigma_ring G) : classical_set_scope. +Notation "'<>'" := (smallest monotone G) : classical_set_scope. + +Section lambda_system_smallest. +Variables (T : Type) (D : set T) (G : set (set T)). +Hypothesis GD : forall A, G A -> A `<=` D. + +Lemma lambda_system_smallest : lambda_system D <>. +Proof. +split => [A MA | E [monoE] | A B BA MA MB E [[EsubD ED setDE ndE] GE] |]. +- have monoH := powerset_lambda_system D. + by case: (monoH) => + _ _ _; apply; exact: MA. +- by case: monoE. +- by apply setDE => //; [exact: MA|exact: MB]. +- by move=> F ndF MF E [[EsubD ED setDE ndE] CE]; apply ndE=> // n; exact: MF. +Qed. + +End lambda_system_smallest. Lemma fin_bigcup_closedP T (G : set (set T)) : (G set0 /\ setU_closed G) <-> fin_bigcup_closed G. @@ -530,32 +600,143 @@ Qed. End generated_setring. #[global] Hint Resolve smallest_setring setring0 : core. -Lemma monotone_class_g_salgebra T (G : set (set T)) (D : set T) : - (forall X, <> X -> X `<=` D) -> G D -> - monotone_class D (<>). +Lemma g_sigma_algebra_lambda_system T (G : set (set T)) (D : set T) : + (forall X, <> X -> X `<=` D) -> + lambda_system D <>. Proof. -move=> sDGD GD; have := smallest_sigma_algebra D G. +move=> sDGD; have := smallest_sigma_algebra D G. by move=> /(sigma_algebraP sDGD) [sT sD snd sI]; split. Qed. +#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `g_sigma_algebra_lambda_system`")] +Notation monotone_class_g_salgebra := g_sigma_algebra_lambda_system (only parsing). + +Lemma smallest_sigma_ring T (G : set (set T)) : sigma_ring <>. +Proof. +split=> [B [[]]//|A B GA GB C [[? CDI ?]] GC|A GA C [[? ? CU]] GC] /=. +- by apply: (CDI); [exact: GA|exact: GB]. +- by apply: (CU) => n; exact: GA. +Qed. + +(**md see Paul Halmos' Measure Theory, Ch.1, sec.6, thm.A(1), p.27 *) +Lemma sigma_ring_monotone T (G : set (set T)) : sigma_ring G -> monotone G. +Proof. +move=> [G0 GDI GU]; split => [F ndF GF|F icF GF]; first exact: GU. +rewrite -(@setD_bigcup _ _ F _ O)//; apply: (GDI); first exact: GF. +by rewrite bigcup_mkcond; apply: GU => n; case: ifPn => // _; exact: GDI. +Qed. + +Lemma g_sigma_ring_monotone T (G : set (set T)) : monotone <>. +Proof. by apply: sigma_ring_monotone => //; exact: smallest_sigma_ring. Qed. + +Lemma sub_g_sigma_ring T (G : set (set T)) : G `<=` <>. +Proof. exact: sub_smallest. Qed. + +(**md see Paul Halmos' Measure Theory, Ch.1, sec.6, thm.A(2), p.27 *) +Lemma setring_monotone_sigma_ring T (G : set (set T)) : + setring G -> monotone G -> sigma_ring G. +Proof. +move=> [G0 GU GD] [ndG niG]; split => // F GF. +rewrite -bigcup_bigsetU_bigcup; apply: ndG. + by move=> *; exact/subsetPset/subset_bigsetU. +by elim=> [|n ih]; rewrite big_ord_recr/= ?big_ord0 ?set0U//; exact: GU. +Qed. + +Lemma g_monotone_monotone T (G : set (set T)) : monotone <>. +Proof. +split=> /= F ndF GF C [[ndC niC] GC]; + have {}GC : <> `<=` C by exact: smallest_sub. +- by apply: (ndC) => // i; apply: (GC); exact: GF. +- by apply: (niC) => // i; apply: (GC); exact: GF. +Qed. + +Section g_monotone_g_sigma_ring. +Variables (T : Type) (G : set (set T)). +Hypothesis ringG : setring G. + +(**md see Paul Halmos' Measure Theory, Ch.1, sec.6, thm.B, p.27 *) +Lemma g_monotone_setring : setring <>. +Proof. +pose M := <>. +pose K F := [set E | [/\ M (E `\` F), M (F `\` E) & M (E `|` F)] ]. +have KP E F : K(F) E -> K(E) F by move=> [] *; split; rewrite 1?setUC. +have K_monotone F : monotone (K(F)). + split. + move=> /= H ndH KFH; split. + - rewrite setD_bigcupl; apply: (g_monotone_monotone G).1. + by move=> m n mn; apply/subsetPset; apply: setSD; exact/subsetPset/ndH. + by move=> i; have [] := KFH i. + - rewrite setDE setC_bigcup -bigcapIr//; apply: (g_monotone_monotone G).2. + move=> m n mn; apply/subsetPset. + by apply: setDS; exact/subsetPset/ndH. + by move=> i; have [] := KFH i. + - rewrite -bigcupUl//; apply: (g_monotone_monotone G).1. + move=> m n mn; apply/subsetPset. + by apply: setSU; exact/subsetPset/ndH. + by move=> i; have [] := KFH i. + move=> /= H niH KFH; split. + - rewrite setDE -bigcapIl//; apply: (g_monotone_monotone G).2. + move=> m n mn; apply/subsetPset; apply: setSI; exact/subsetPset/niH. + by move=> i; have [] := KFH i. + - rewrite setDE setC_bigcap setI_bigcupr; apply: (g_monotone_monotone G).1. + move=> m n mn; apply/subsetPset. + by apply: setIS; apply: subsetC; exact/subsetPset/niH. + by move=> i; have [] := KFH i. + - rewrite setU_bigcapl//; apply: (g_monotone_monotone G).2. + move=> m n mn; apply/subsetPset. + by apply: setSU; exact/subsetPset/niH. + by move=> i; have [] := KFH i. +have G_KF F : G F -> G `<=` K(F). + case: ringG => _ GU GDI GF A GA; split. + - by apply: sub_gen_smallest; exact: GDI. + - by apply: sub_gen_smallest; exact: GDI. + - by apply: sub_gen_smallest; exact: GU. +have GM_KF F : G F -> M `<=` K(F). + by move=> GF; apply: smallest_sub => //; exact: G_KF. +have MG_KF F : M F -> G `<=` K(F). + by move=> MF A GA; rewrite /K/=; split; have /KP[] := GM_KF _ GA _ MF. +have MM_KF F : M F -> M `<=` K(F). + by move=> MF; apply: smallest_sub => //; exact: MG_KF. +split. +- by apply: sub_gen_smallest; case: ringG. +- by move=> A B GA GB; have [] := MM_KF _ GB _ GA. +- by move=> A B GA GB; have [] := MM_KF _ GB _ GA. +Qed. + +Lemma g_monotone_g_sigma_ring : <> = <>. +Proof. +rewrite eqEsubset; split. + by apply: smallest_sub; [exact: g_sigma_ring_monotone| + exact: sub_g_sigma_ring]. +apply: smallest_sub; last exact: sub_smallest. +apply: setring_monotone_sigma_ring; last exact: g_monotone_monotone. +exact: g_monotone_setring. +Qed. + +End g_monotone_g_sigma_ring. + +Corollary monotone_setring_sub_g_sigma_ring T (G R : set (set T)) : monotone G -> + setring R -> R `<=` G -> <> `<=` G. +Proof. +by move=> mG rR RG; rewrite -g_monotone_g_sigma_ring//; exact: smallest_sub. +Qed. -Section smallest_monotone_classE. -Variables (T : Type) (G : set (set T)) (setIG : setI_closed G). -Variables (D : set T) (GD : G D). -Variables (H : set (set T)) (monoH : monotone_class D H) (GH : G `<=` H). +Section smallest_lambda_system. +Variables (T : Type) (G : set (set T)) (setIG : setI_closed G) (D : set T). +Hypothesis lambdaDG : lambda_system D <>. -Lemma smallest_monotone_classE : (forall X, <> X -> X `<=` D) -> - (forall E, monotone_class D E -> G `<=` E -> H `<=` E) -> - H = <>. +Lemma smallest_lambda_system : (forall X, <> X -> X `<=` D) -> + <> = <>. Proof. -move=> sDGD smallestH; rewrite eqEsubset; split. - apply: (smallestH _ _ (@sub_sigma_algebra _ D G)). - exact: monotone_class_g_salgebra. -suff: setI_closed H. +move=> sDGD; rewrite eqEsubset; split. + apply: smallest_sub; first exact: g_sigma_algebra_lambda_system. + exact: sub_sigma_algebra. +suff: setI_closed <>. move=> IH; apply: smallest_sub => //. - by apply/sigma_algebraP; by case: monoH. + by apply/sigma_algebraP; case: lambdaDG. +pose H := <>. pose H_ A := [set X | H X /\ H (X `&` A)]. have setDH_ A : setD_closed (H_ A). - move=> X Y XY [HX HXA] [HY HYA]; case: monoH => h _ setDH _; split. + move=> X Y XY [HX HXA] [HY HYA]; case: lambdaDG => h _ setDH _; split. exact: setDH. rewrite (_ : _ `&` _ = (X `&` A) `\` (Y `&` A)); last first. rewrite predeqE => x; split=> [[[? ?] ?]|]; first by split => // -[]. @@ -563,47 +744,54 @@ have setDH_ A : setD_closed (H_ A). by apply: setDH => //; exact: setSI. have ndH_ A : ndseq_closed (H_ A). move=> F ndF H_AF; split. - by case: monoH => h _ _; apply => // => n; have [] := H_AF n. - rewrite setI_bigcupl; case: monoH => h _ _; apply => //. + by case: lambdaDG => h _ _; apply => // => n; have [] := H_AF n. + rewrite setI_bigcupl; case: lambdaDG => h _ _; apply => //. by move=> m n mn; apply/subsetPset; apply: setSI; apply/subsetPset/ndF. by move=> n; have [] := H_AF n. have GGH_ X : G X -> G `<=` H_ X. - by move=> *; split; [exact: GH | apply: GH; exact: setIG]. + move=> GX; rewrite /H_ => A GA; split; first exact: sub_smallest GA. + by apply: (@sub_smallest _ _ _ G) => //; exact: setIG. +have HD X : H X -> X `<=` D by move=> ?; case: lambdaDG => + _ _ _; apply. have GHH_ X : G X -> H `<=` H_ X. - move=> CX; apply: smallestH; [split => //; last exact: GGH_|exact: GGH_]. - by move=> ? [? ?]; case: monoH => + _ _ _; exact. + move=> GX; apply: smallest_sub; last exact: GGH_. + split => //; first by move=> A [HA _]; case: lambdaDG => + _ _ _; exact. + have XD : X `<=` D by apply: HD; exact: (@sub_smallest _ _ _ G). + rewrite /H_ /= setIidr//; split; [by case: lambdaDG|]. + exact: (@sub_smallest _ _ _ G). have HGH_ X : H X -> G `<=` H_ X. - by move=> *; split; [exact: GH|rewrite setIC; apply GHH_]. + move=> *; split; [|by rewrite setIC; apply GHH_]. + exact: (@sub_smallest _ _ _ G). have HHH_ X : H X -> H `<=` H_ X. - move=> HX; apply: (smallestH _ _ (HGH_ _ HX)); split=> //. - - by move=> ? [? ?]; case: monoH => + _ _ _; exact. - - exact: HGH_. + move=> HX; apply: smallest_sub; last exact: HGH_. + split=> //. + - by move=> ? [? ?]; case: lambdaDG => + _ _ _; exact. + - have XD : X `<=` D := HD _ HX. + by rewrite /H_/= setIidr//; split => //; case: lambdaDG. by move=> *; apply HHH_. Qed. -End smallest_monotone_classE. +End smallest_lambda_system. +#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `smallest_lambda_system`")] +Notation smallest_monotone_classE := smallest_lambda_system (only parsing). -Section monotone_class_subset. -Variables (T : Type) (G : set (set T)) (setIG : setI_closed G). -Variables (D : set T) (GD : G D). -Variables (H : set (set T)) (monoH : monotone_class D H) (GH : G `<=` H). +Section lambda_system_subset. +Variables (T : Type) (G : set (set T)) (setIG : setI_closed G) (D : set T). +Variables (H : set (set T)) (DH : lambda_system D H) (GH : G `<=` H). -Lemma monotone_class_subset : (forall X, (<>) X -> X `<=` D) -> +(**md a.k.a. Sierpiński–Dynkin's pi-lambda theorem *) +Lemma lambda_system_subset : (forall X, (<>) X -> X `<=` D) -> <> `<=` H. Proof. -move=> sDGD; set M := <>. -rewrite -(@smallest_monotone_classE _ _ setIG _ _ M) //. +move=> sDGD; set M := <>. +rewrite -(@smallest_lambda_system _ _ setIG D) //. - exact: smallest_sub. -- split => [A MA | E [monoE] | A B BA MA MB E [[EsubD ED setDE ndE] GE] |]. - + by case: monoH => + _ _ _; apply; exact: MA. - + exact. - + by apply setDE => //; [exact: MA|exact: MB]. - + by move=> F ndF MF E [[EsubD ED setDE ndE] CE]; apply ndE=> // n; exact: MF. -- exact: sub_smallest. -- by move=> ? ? ?; exact: smallest_sub. +- apply: lambda_system_smallest => A GA. + by apply: sDGD; exact: sub_sigma_algebra. Qed. -End monotone_class_subset. +End lambda_system_subset. +#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `lambda_system_subset`")] +Notation monotone_class_subset := lambda_system_subset (only parsing). Section dynkin. Variable T : Type. @@ -622,14 +810,14 @@ Section dynkin_lemmas. Variable T : Type. Implicit Types D G : set (set T). -Lemma dynkin_monotone G : dynkin G <-> monotone_class setT G. +Lemma dynkin_lambda_system G : dynkin G <-> lambda_system setT G. Proof. split => [[GT setCG trG]|[_ GT setDG ndG]]; split => //. - move=> A B BA GA GB; rewrite setDE -(setCK (_ `&` _)) setCI; apply: (setCG). rewrite setCK -bigcup2E; apply trG. + by rewrite -trivIset_bigcup2 setIC; apply subsets_disjoint. + by move=> [|[//|n]]; [exact: setCG|rewrite /bigcup2 -setCT; apply: setCG]. -- move=> F ndF GF; rewrite eq_bigcup_seqD; apply: (trG). +- move=> F ndF GF; rewrite -eq_bigcup_seqD; apply: (trG). exact: trivIset_seqD. move=> [/=|n]; first exact: GF. rewrite /seqD setDE -(setCK (_ `&` _)) setCI; apply: (setCG). @@ -640,10 +828,7 @@ split => [[GT setCG trG]|[_ GT setDG ndG]]; split => //. by move=> _; rewrite -setCT; apply: setCG. - by move=> A B; rewrite -setTD; apply: setDG. - move=> F tF GF; pose A i := \big[setU/set0]_(k < i.+1) F k. - rewrite (_ : bigcup _ _ = \bigcup_i A i); last first. - rewrite predeqE => t; split => [[n _ Fn]|[n _]]. - by exists n => //; rewrite /A -bigcup_mkord; exists n=> //=; rewrite ltnS. - by rewrite /A -bigcup_mkord => -[m /=]; rewrite ltnS => mn Fmt; exists m. + rewrite -bigcup_bigsetU_bigcup. apply: ndG; first by move=> a b ab; exact/subsetPset/subset_bigsetU. elim=> /= => [|n ih]. by rewrite /A big_ord_recr /= big_ord0 set0U; exact: GF. @@ -656,7 +841,7 @@ split => [[GT setCG trG]|[_ GT setDG ndG]]; split => //. by apply: (@trivIset_bigsetUI _ predT) => //; rewrite /predT /= trueE. Qed. -Lemma dynkin_g_dynkin G : dynkin (<>). +Lemma g_dynkin_dynkin G : dynkin <>. Proof. split=> [D /= [] []//| | ]. - by move=> Y sGY D /= [dD GD]; exact/(dynkinC dD)/(sGY D). @@ -689,10 +874,11 @@ move=> dG GI; split => [|//|F DF]. by apply: (@dynkin_setI_bigsetI _ (fun x => ~` F x)) => // ?; exact/(dynkinC dG). Qed. -Lemma setI_closed_gdynkin_salgebra G : setI_closed G -> <> = <>. +Lemma setI_closed_g_dynkin_g_sigma_algebra G : + setI_closed G -> <> = <>. Proof. move=> GI; rewrite eqEsubset; split. - by apply: sub_smallest2l; apply: sigma_algebra_dynkin. + by apply: sub_smallest2l; exact: sigma_algebra_dynkin. pose delta (D : set T) := [set E | <> (E `&` D)]. have ddelta (D : set T) : <> D -> dynkin (delta D). move=> dGD; split; first by rewrite /delta /= setTI. @@ -733,10 +919,134 @@ have dGdGdelta A : <> A -> <> `<=` delta A. have dGdGdG A B : <> A -> <> B -> <> (A `&` B). by move=> ? ?; exact: dGdGdelta. apply: smallest_sub => //; apply: dynkin_setI_sigma_algebra => //. -exact: dynkin_g_dynkin. +exact: g_dynkin_dynkin. Qed. End dynkin_lemmas. +#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed into `setI_closed_g_dynkin_g_sigma_algebra`")] +Notation setI_closed_gdynkin_salgebra := setI_closed_g_dynkin_g_sigma_algebra (only parsing). +#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed into `g_dynkin_dynkin`")] +Notation dynkin_g_dynkin := g_dynkin_dynkin (only parsing). +#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed into `dynkin_lambda_system`")] +Notation dynkin_monotone := dynkin_lambda_system (only parsing). + +Section trace. +Variable (T : Type). +Implicit Types (G : set (set T)) (A D : set T). + +Definition strace G D := [set x `&` D | x in G]. + +Lemma subset_strace G C : G `<=` C -> forall D, strace G D `<=` strace C D. +Proof. by move=> GC D _ [A GA <-]; exists A => //; exact: GC. Qed. + +Lemma g_sigma_ring_strace G A B : <> B -> B `<=` A. +Proof. +move=> H; apply H => /=; split; first exact: powerset_sigma_ring. +by move=> X [A0 GA0 <-]; exact: subIsetr. +Qed. + +Lemma strace_sigma_ring G A : sigma_ring (strace <> A). +Proof. +split. +- by exists set0; rewrite ?set0I//; have [] := smallest_sigma_ring G. +- move=> _ _ [A0 GA0] <- [A1 GA1] <-. + exists (A0 `\` A1); first by have [_ + _] := smallest_sigma_ring G; exact. + by rewrite -setIDA setDIr setDv setU0 setIDAC setIDA. +- move=> F GAF. + pose f n := sval (cid2 (GAF n)). + pose Hf n := (svalP (cid2 (GAF n))).1. + pose H n := (svalP (cid2 (GAF n))).2. + exists (\bigcup_k f k). + by have [_ _] := smallest_sigma_ring G; apply => n; exact: Hf. + by rewrite setI_bigcupl; apply: eq_bigcupr => i _; exact: H. +Qed. + +(**md see Paul Halmos' Measure Theory, Ch.1, sec.5, thm.E, p.25 *) +Lemma setI_g_sigma_ring G A : strace <> A = <>. +Proof. +pose D := [set B `|` (C `\` A) | B in <> & C in <>]. +have D_sigma_ring : sigma_ring D. + split. + - exists set0; first by have [] := smallest_sigma_ring (strace G A). + exists set0; first by have [] := smallest_sigma_ring G. + by rewrite set0D setU0. + - move=> _ _ [B0 GAB0] [C0 GC0] <- [B1 GAB1] [C1 GC1] <-. + exists (B0 `\` B1). + by have [_ + _] := smallest_sigma_ring (strace G A); exact. + exists (C0 `\` C1); first by have [_ + _] := smallest_sigma_ring G; exact. + apply/esym; rewrite setDUD. + transitivity (((B0 `\` B1) `&` (B0 `\` (C1 `\` A))) `|` + ((C0 `\` (A `|` B1)) `&` (C0 `\` C1))). + congr setU; first by rewrite setDUr. + apply/seteqP; split => [x [[C0x Ax]]|x]. + move=> /not_orP[B1x /not_andP[C1x|//]]. + by split=> //; split => // -[]. + move=> [[C0x /not_orP[Ax B1x] [_ C1x]]]. + by split=> // -[//|[]]. + transitivity (((B0 `\` B1) `&` B0) `|` + ((C0 `\` A ) `&` (C0 `\` C1))). + apply/seteqP; split => [x [[[B0x B1x] [_ /not_andP[C1x|]]]| + [[C0x /not_orP[Ax B1x]] [_ C1x]]]| + x [[[B0x B1x] _]|[[C0x Ax] [_ C1x]]]]. + + by left; split. + + by move=> /contrapT Ax; left. + + by right; split. + + left; split => //; split => // -[] _; apply. + exact: (g_sigma_ring_strace GAB0). + + right; split => //; split => // -[//|B1x]; apply: Ax. + exact: (g_sigma_ring_strace GAB1). + + congr setU; first by rewrite setDE setIAC setIid. + by rewrite setDDl setDUr setIC. + - move=> F DF. + pose f n := sval (cid2 (DF n)). + pose Hf n := (svalP (cid2 (DF n))).1. + pose g n := sval (cid2 (svalP (cid2 (DF n))).2). + pose Hg n := (svalP (cid2 (svalP (cid2 (DF n))).2)).1. + exists (\bigcup_n f n). + have [_ _] := smallest_sigma_ring (strace G A). + by apply => n; exact: Hf. + exists (\bigcup_n g n). + have [_ _] := smallest_sigma_ring G. + by apply => n; exact: Hg. + pose H n := (svalP (cid2 (svalP (cid2 (DF n))).2)).2. + by rewrite setD_bigcupl -bigcupU; apply: eq_bigcupr => k _; exact: H. +apply/seteqP; split => [|]. + have GD : G `<=` D. + move=> E GE; exists (E `&` A). + by apply: sub_g_sigma_ring; exists E. + by exists E; [exact: sub_g_sigma_ring|exact: setUIDK]. + have {}GD : <> `<=` D by exact: smallest_sub GD. + have GDA : strace <> A `<=` strace D A by exact: subset_strace. + suff: strace D A = <> by move=> <-. + apply/seteqP; split. + move=> _ [_ [gA HgA [g Hg] <-] <-]. + by rewrite setIUl setDKI setU0 setIidl//; exact: (g_sigma_ring_strace HgA). + move=> X HX; exists X. + exists X => //; exists set0; rewrite ?set0D ?setU0//. + by have [] := smallest_sigma_ring G. + by rewrite setIidl//; exact: (g_sigma_ring_strace HX). +have : strace G A `<=` strace <> A. + by move=> X [Y GY <-]; exists Y => //; exact: sub_smallest GY. +by apply: smallest_sub; exact: strace_sigma_ring. +Qed. + +Lemma sigma_algebra_strace G D : + sigma_algebra setT G -> sigma_algebra D (strace G D). +Proof. +move=> [G0 GC GU]; split; first by exists set0 => //; rewrite set0I. +- move=> S [A mA ADS]; have mCA := GC _ mA. + have : strace G D (D `&` ~` A). + by rewrite setIC; exists (setT `\` A) => //; rewrite setTD. + rewrite -setDE => trDA. + have DADS : D `\` A = D `\` S by rewrite -ADS !setDE setCI setIUr setICr setU0. + by rewrite DADS in trDA. +- move=> S mS; have /choice[M GM] : forall n, exists A, G A /\ S n = A `&` D. + by move=> n; have [A mA ADSn] := mS n; exists A. + exists (\bigcup_i (M i)); first by apply GU => i; exact: (GM i).1. + by rewrite setI_bigcupl; apply eq_bigcupr => i _; rewrite (GM i).2. +Qed. + +End trace. HB.mixin Record isSemiRingOfSets (d : measure_display) T := { measurable : set (set T) ; @@ -776,14 +1086,54 @@ HB.mixin Record RingOfSets_isAlgebraOfSets d T of RingOfSets d T := { HB.structure Definition AlgebraOfSets d := {T of RingOfSets d T & RingOfSets_isAlgebraOfSets d T }. -HB.mixin Record AlgebraOfSets_isMeasurable d T of AlgebraOfSets d T := { +HB.mixin Record hasMeasurableCountableUnion d T of SemiRingOfSets d T := { + bigcupT_measurable : forall F : (set T)^nat, (forall i, measurable (F i)) -> + measurable (\bigcup_i (F i)) +}. + +HB.builders Context d T of hasMeasurableCountableUnion d T. + +Let mU : @setU_closed T measurable. +Proof. +move=> A B mA mB; rewrite -bigcup2E. +by apply: bigcupT_measurable => -[//|[//|/= _]]; exact: measurable0. +Qed. + +HB.instance Definition _ := SemiRingOfSets_isRingOfSets.Build d T mU. + +HB.end. + +#[short(type="sigmaRingType")] +HB.structure Definition SigmaRing d := + {T of SemiRingOfSets d T & hasMeasurableCountableUnion d T}. + +HB.factory Record isSigmaRing (d : measure_display) T of Pointed T := { + measurable : set (set T) ; + measurable0 : measurable set0 ; + measurableD : setDI_closed measurable ; bigcupT_measurable : forall F : (set T)^nat, (forall i, measurable (F i)) -> measurable (\bigcup_i (F i)) }. +HB.builders Context d T of isSigmaRing d T. + +Let m0 : measurable set0. Proof. exact: measurable0. Qed. + +Let mI : setI_closed measurable. +Proof. by have [] := (sedDI_closedP measurable).1 measurableD. Qed. + +Let mD : semi_setD_closed measurable. +Proof. by apply: setDI_semi_setD_closed; exact: measurableD. Qed. + +HB.instance Definition _ := isSemiRingOfSets.Build d T m0 mI mD. + +HB.instance Definition _ := hasMeasurableCountableUnion.Build d T bigcupT_measurable. + +HB.end. + #[short(type="measurableType")] HB.structure Definition Measurable d := - {T of AlgebraOfSets d T & AlgebraOfSets_isMeasurable d T }. + {T of AlgebraOfSets d T & hasMeasurableCountableUnion d T }. HB.factory Record isRingOfSets (d : measure_display) T of Pointed T := { measurable : set (set T) ; @@ -796,14 +1146,10 @@ HB.builders Context d T of isRingOfSets d T. Implicit Types (A B C D : set T). Lemma mI : setI_closed measurable. -Proof. by move=> A B mA mB; rewrite -setDD; do ?apply: measurableD. Qed. +Proof. by have [] := (sedDI_closedP measurable).1 measurableD. Qed. Lemma mD : semi_setD_closed measurable. -Proof. -move=> A B Am Bm; exists [set A `\` B]; split; rewrite ?bigcup_set1//. - by move=> C ->; apply: measurableD. -by move=> X Y -> ->. -Qed. +Proof. by apply: setDI_semi_setD_closed; exact: measurableD. Qed. HB.instance Definition _ := @isSemiRingOfSets.Build d T measurable measurable0 mI mD. @@ -861,7 +1207,7 @@ HB.instance Definition _ := @isAlgebraOfSets.Build d T measurable measurable0 mU mC. HB.instance Definition _ := - @AlgebraOfSets_isMeasurable.Build d T measurable_bigcup. + @hasMeasurableCountableUnion.Build d T measurable_bigcup. HB.end. @@ -929,13 +1275,10 @@ Qed. End algebraofsets_lemmas. -Section measurable_lemmas. -Context d (T : measurableType d). +Section sigmaring_lemmas. +Context d (T : sigmaRingType d). Implicit Types (A B : set T) (F : (set T)^nat) (P : set nat). -Lemma sigma_algebra_measurable : sigma_algebra setT (@measurable d T). -Proof. by split=> // [A|]; [exact: measurableD|exact: bigcupT_measurable]. Qed. - Lemma bigcup_measurable F P : (forall k, P k -> measurable (F k)) -> measurable (\bigcup_(i in P) F i). Proof. @@ -943,26 +1286,61 @@ move=> PF; rewrite bigcup_mkcond; apply: bigcupT_measurable => k. by case: ifP => //; rewrite inE; exact: PF. Qed. -Lemma bigcap_measurable F P : +Lemma bigcap_measurable F P : P !=set0 -> (forall k, P k -> measurable (F k)) -> measurable (\bigcap_(i in P) F i). Proof. -move=> PF; rewrite -[X in measurable X]setCK setC_bigcap; apply: measurableC. -by apply: bigcup_measurable => k Pk; exact/measurableC/PF. +move=> [j Pj] PF; rewrite -(setD_bigcup F Pj). +apply: measurableD; first exact: PF. +by apply: bigcup_measurable => k/= [Pk kj]; apply: measurableD; exact: PF. Qed. -Lemma bigcapT_measurable F : (forall i, measurable (F i)) -> - measurable (\bigcap_i (F i)). -Proof. by move=> ?; exact: bigcap_measurable. Qed. +Lemma bigcapT_measurable F : + (forall k, measurable (F k)) -> measurable (\bigcap_i F i). +Proof. by move=> PF; apply: bigcap_measurable => //; exists 1. Qed. -End measurable_lemmas. +End sigmaring_lemmas. + +Section sigma_ring_lambda_system. +Context d (T : sigmaRingType d). + +Lemma sigmaRingType_lambda_system (D : set T) : measurable D -> + lambda_system D [set X | measurable X /\ X `<=` D]. +Proof. +move=> mD; split. +- by move=> A /=[]. +- by split. +- move=> B A AB/= [mB BD] [mA AD]; split; first exact: measurableD. + by apply: subset_trans BD; exact: subDsetl. +- move=> /= F _ mFD; split. + by apply: bigcup_measurable => i _; exact: (mFD _).1. + by apply: bigcup_sub => i _; exact: (mFD _).2. +Qed. -Lemma bigcupT_measurable_rat d (T : measurableType d) (F : rat -> set T) : +End sigma_ring_lambda_system. + +Lemma bigcupT_measurable_rat d (T : sigmaRingType d) (F : rat -> set T) : (forall i, measurable (F i)) -> measurable (\bigcup_i F i). Proof. move=> Fm; have /ppcard_eqP[f] := card_rat. by rewrite (reindex_bigcup f^-1%FUN setT)//=; exact: bigcupT_measurable. Qed. +Section measurable_lemmas. +Context d (T : measurableType d). +Implicit Types (A B : set T) (F : (set T)^nat) (P : set nat). + +Lemma sigma_algebra_measurable : sigma_algebra setT (@measurable d T). +Proof. by split=> // [A|]; [exact: measurableD|exact: bigcupT_measurable]. Qed. + +Lemma bigcap_measurableType F P : + (forall k, P k -> measurable (F k)) -> measurable (\bigcap_(i in P) F i). +Proof. +move=> PF; rewrite -[X in measurable X]setCK setC_bigcap; apply: measurableC. +by apply: bigcup_measurable => k Pk; exact/measurableC/PF. +Qed. + +End measurable_lemmas. + Section discrete_measurable_unit. Definition discrete_measurable_unit : set (set unit) := [set: set unit]. @@ -1028,7 +1406,9 @@ End discrete_measurable_nat. Definition sigma_display {T} : set (set T) -> measure_display. Proof. exact. Qed. -Definition salgebraType {T} (G : set (set T)) := T. +Definition g_sigma_algebraType {T} (G : set (set T)) := T. +#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed into `g_sigma_algebraType`")] +Notation salgebraType := g_sigma_algebraType (only parsing). Section g_salgebra_instance. Variables (T : pointedType) (G : set (set T)). @@ -1036,9 +1416,9 @@ Variables (T : pointedType) (G : set (set T)). Lemma sigma_algebraC (A : set T) : <> A -> <> (~` A). Proof. by move=> sGA; rewrite -setTD; exact: sigma_algebraCD. Qed. -HB.instance Definition _ := Pointed.on (salgebraType G). +HB.instance Definition _ := Pointed.on (g_sigma_algebraType G). HB.instance Definition _ := @isMeasurable.Build (sigma_display G) - (salgebraType G) + (g_sigma_algebraType G) <> (@sigma_algebra0 _ setT G) (@sigma_algebraC) (@sigma_algebra_bigcup _ setT G). @@ -1046,19 +1426,19 @@ End g_salgebra_instance. Notation "G .-sigma" := (sigma_display G) : measure_display_scope. Notation "G .-sigma.-measurable" := - (measurable : set (set (salgebraType G))) : classical_set_scope. + (measurable : set (set (g_sigma_algebraType G))) : classical_set_scope. Lemma measurable_g_measurableTypeE (T : pointedType) (G : set (set T)) : sigma_algebra setT G -> G.-sigma.-measurable = G. Proof. exact: sigma_algebra_id. Qed. -Definition measurable_fun d d' (T : measurableType d) (U : measurableType d') +Definition measurable_fun d d' (T : sigmaRingType d) (U : sigmaRingType d') (D : set T) (f : T -> U) := measurable D -> forall Y, measurable Y -> measurable (D `&` f @^-1` Y). Section measurable_fun. -Context d1 d2 d3 (T1 : measurableType d1) (T2 : measurableType d2) - (T3 : measurableType d3). +Context d1 d2 d3 (T1 : sigmaRingType d1) (T2 : sigmaRingType d2) + (T3 : sigmaRingType d3). Implicit Type D E : set T1. Lemma measurable_id D : measurable_fun D id. @@ -1076,10 +1456,6 @@ rewrite (_ : _ `&` _ = E `&` g @^-1` (F `&` f @^-1` A)); last first. by apply/mg => //; exact: mf. Qed. -Lemma measurableT_comp (f : T2 -> T3) E (g : T1 -> T2) : - measurable_fun setT f -> measurable_fun E g -> measurable_fun E (f \o g). -Proof. exact: measurable_comp. Qed. - Lemma eq_measurable_fun D (f g : T1 -> T2) : {in D, f =1 g} -> measurable_fun D f -> measurable_fun D g. Proof. @@ -1123,12 +1499,54 @@ suff -> : D `|` (E `\` D) = E by move=> [[]] //. by rewrite setDUK. Qed. +Lemma measurable_fun_if (g h : T1 -> T2) D (mD : measurable D) + (f : T1 -> bool) (mf : measurable_fun D f) : + measurable_fun (D `&` (f @^-1` [set true])) g -> + measurable_fun (D `&` (f @^-1` [set false])) h -> + measurable_fun D (fun t => if f t then g t else h t). +Proof. +move=> mx my /= _ B mB; rewrite (_ : _ @^-1` B = + ((f @^-1` [set true]) `&` (g @^-1` B)) `|` + ((f @^-1` [set false]) `&` (h @^-1` B))). + rewrite setIUr; apply: measurableU. + - by rewrite setIA; apply: mx => //; exact: mf. + - by rewrite setIA; apply: my => //; exact: mf. +apply/seteqP; split=> [t /=| t /= [] [] ->//]. +by case: ifPn => ft; [left|right]. +Qed. + +End measurable_fun. +#[global] Hint Extern 0 (measurable_fun _ (fun=> _)) => + solve [apply: measurable_cst] : core. +#[global] Hint Extern 0 (measurable_fun _ (cst _)) => + solve [apply: measurable_cst] : core. +#[global] Hint Extern 0 (measurable_fun _ id) => + solve [apply: measurable_id] : core. +Arguments eq_measurable_fun {d1 d2 T1 T2 D} f {g}. +#[deprecated(since="mathcomp-analysis 0.6.2", note="renamed `eq_measurable_fun`")] +Notation measurable_fun_ext := eq_measurable_fun (only parsing). +#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_id`")] +Notation measurable_fun_id := measurable_id (only parsing). +#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_cst`")] +Notation measurable_fun_cst := measurable_cst (only parsing). +#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_comp`")] +Notation measurable_fun_comp := measurable_comp (only parsing). + +Section measurable_fun_measurableType. +Context d1 d2 d3 (T1 : measurableType d1) (T2 : measurableType d2) + (T3 : measurableType d3). +Implicit Type D E : set T1. + +Lemma measurableT_comp (f : T2 -> T3) E (g : T1 -> T2) : + measurable_fun [set: T2] f -> measurable_fun E g -> measurable_fun E (f \o g). +Proof. exact: measurable_comp. Qed. + Lemma measurable_funTS D (f : T1 -> T2) : - measurable_fun setT f -> measurable_fun D f. + measurable_fun [set: T1] f -> measurable_fun D f. Proof. exact: measurable_funS. Qed. Lemma measurable_restrict D E (f : T1 -> T2) : - measurable D -> measurable E -> D `<=` E -> + measurable D -> measurable E -> D `<=` E -> measurable_fun D f <-> measurable_fun E (f \_ D). Proof. move=> mD mE DE; split => mf _ /= X mX. @@ -1142,26 +1560,10 @@ move=> mD mE DE; split => mf _ /= X mX. by rewrite setIA (setIidl DE) setIUr setICr set0U. Qed. -Lemma measurable_fun_if (g h : T1 -> T2) D (mD : measurable D) - (f : T1 -> bool) (mf : measurable_fun D f) : - measurable_fun (D `&` (f @^-1` [set true])) g -> - measurable_fun (D `&` (f @^-1` [set false])) h -> - measurable_fun D (fun t => if f t then g t else h t). -Proof. -move=> mx my /= _ B mB; rewrite (_ : _ @^-1` B = - ((f @^-1` [set true]) `&` (g @^-1` B)) `|` - ((f @^-1` [set false]) `&` (h @^-1` B))). - rewrite setIUr; apply: measurableU. - - by rewrite setIA; apply: mx => //; exact: mf. - - by rewrite setIA; apply: my => //; exact: mf. -apply/seteqP; split=> [t /=| t /= [] [] ->//]. -by case: ifPn => ft; [left|right]. -Qed. - Lemma measurable_fun_ifT (g h : T1 -> T2) (f : T1 -> bool) - (mf : measurable_fun setT f) : - measurable_fun setT g -> measurable_fun setT h -> - measurable_fun setT (fun t => if f t then g t else h t). + (mf : measurable_fun [set: T1] f) : + measurable_fun [set: T1] g -> measurable_fun [set: T1] h -> + measurable_fun [set: T1] (fun t => if f t then g t else h t). Proof. by move=> mx my; apply: measurable_fun_if => //; [exact: measurable_funS mx|exact: measurable_funS my]. @@ -1201,13 +1603,13 @@ Lemma measurable_and D (f : T1 -> bool) (g : T1 -> bool) : measurable_fun D (fun x => f x && g x). Proof. move=> mf mg mD; apply: (measurable_fun_bool true) => //. -- rewrite [X in measurable X](_ : _ = D `&` f @^-1` [set true] `&` - (D `&` g @^-1` [set true])); last first. - by rewrite setIACA setIid; congr (_ `&` _); apply/seteqP; split => x /andP. - by apply: measurableI; [exact: mf|exact: mg]. +rewrite [X in measurable X](_ : _ = D `&` f @^-1` [set true] `&` + (D `&` g @^-1` [set true])); last first. + by rewrite setIACA setIid; congr (_ `&` _); apply/seteqP; split => x /andP. +by apply: measurableI; [exact: mf|exact: mg]. Qed. -End measurable_fun. +End measurable_fun_measurableType. #[global] Hint Extern 0 (measurable_fun _ (fun=> _)) => solve [apply: measurable_cst] : core. #[global] Hint Extern 0 (measurable_fun _ (cst _)) => @@ -1216,14 +1618,6 @@ End measurable_fun. solve [apply: measurable_id] : core. Arguments eq_measurable_fun {d1 d2 T1 T2 D} f {g}. Arguments measurable_fun_bool {d1 T1 D f} b. -#[deprecated(since="mathcomp-analysis 0.6.2", note="renamed `eq_measurable_fun`")] -Notation measurable_fun_ext := eq_measurable_fun (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_id`")] -Notation measurable_fun_id := measurable_id (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_cst`")] -Notation measurable_fun_cst := measurable_cst (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_comp`")] -Notation measurable_fun_comp := measurable_comp (only parsing). #[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurableT_comp`")] Notation measurable_funT_comp := measurableT_comp (only parsing). @@ -1236,7 +1630,7 @@ Definition preimage_class (aT rT : Type) (D : set aT) (f : aT -> rT) (* f is measurable on the sigma-algebra generated by itself *) Lemma preimage_class_measurable_fun d (aT : pointedType) (rT : measurableType d) (D : set aT) (f : aT -> rT) : - measurable_fun (D : set (salgebraType (preimage_class D f measurable))) f. + measurable_fun (D : set (g_sigma_algebraType (preimage_class D f measurable))) f. Proof. by move=> mD A mA; apply: sub_sigma_algebra; exists A. Qed. Lemma sigma_algebra_preimage_class (aT rT : Type) (G : set (set rT)) @@ -1300,16 +1694,15 @@ by move=> _ [B mB <-]; exact: sG'sfun. Qed. Lemma measurability d d' (aT : measurableType d) (rT : measurableType d') - (D : set aT) (f : aT -> rT) - (G' : set (set rT)) : - @measurable _ rT = <> -> preimage_class D f G' `<=` @measurable _ aT -> + (D : set aT) (f : aT -> rT) (G : set (set rT)) : + @measurable _ rT = <> -> preimage_class D f G `<=` @measurable _ aT -> measurable_fun D f. Proof. move=> sG_rT fG_aT mD. suff h : preimage_class D f (@measurable _ rT) `<=` @measurable _ aT. by move=> A mA; apply: h; exists A. have -> : preimage_class D f (@measurable _ rT) = - <>. + <>. by rewrite [in LHS]sG_rT [in RHS]sigma_algebra_preimage_classE. apply: smallest_sub => //; split => //. - by move=> A mA; exact: measurableD. @@ -1430,7 +1823,7 @@ by rewrite [X in _ + X]big1 ?adde0// => ?; rewrite -ltn_subRL subnn. Unshelve. all: by end_near. Qed. Lemma semi_sigma_additiveE - (R : numFieldType) d (T : measurableType d) (mu : set T -> \bar R) : + (R : numFieldType) d (T : sigmaRingType d) (mu : set T -> \bar R) : semi_sigma_additive mu = sigma_additive mu. Proof. rewrite propeqE; split=> [amu A mA tA|amu A mA tA mbigcupA]; last exact: amu. @@ -1438,7 +1831,7 @@ by apply: amu => //; exact: bigcupT_measurable. Qed. Lemma sigma_additive_is_additive - (R : realFieldType) d (T : measurableType d) (mu : set T -> \bar R) : + (R : realFieldType) d (T : sigmaRingType d) (mu : set T -> \bar R) : mu set0 = 0 -> sigma_additive mu -> additive mu. Proof. move=> mu0; rewrite -semi_sigma_additiveE -semi_additiveE. @@ -1674,7 +2067,7 @@ End measure_lemmas. #[global] Hint Extern 0 (is_true (0%:E <= _)) => solve [apply: measure_ge0] : core. Section measure_lemmas. -Context d (R : realFieldType) (T : measurableType d). +Context d (R : realFieldType) (T : sigmaRingType d). Variable mu : {measure set T -> \bar R}. Lemma measure_sigma_additive : sigma_additive mu. @@ -1689,7 +2082,7 @@ move=> mF tF; rewrite bigcup_mkcond measure_semi_bigcup. - by rewrite [in RHS]eseries_mkcond; apply: eq_eseriesr => n _; case: ifPn. - by move=> i; case: ifPn => // /set_mem; exact: mF. - by move/trivIset_mkcond : tF. -- by rewrite -bigcup_mkcond; apply: bigcup_measurable. +- by rewrite -bigcup_mkcond; exact: bigcup_measurable. Qed. End measure_lemmas. @@ -1698,9 +2091,9 @@ Arguments measure_bigcup {d R T} _ _. #[global] Hint Extern 0 (sigma_additive _) => solve [apply: measure_sigma_additive] : core. -Definition pushforward d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) +Definition pushforward d1 d2 (T1 : sigmaRingType d1) (T2 : sigmaRingType d2) (R : realFieldType) (m : set T1 -> \bar R) (f : T1 -> T2) - of measurable_fun setT f := fun A => m (f @^-1` A). + of measurable_fun [set: T1] f := fun A => m (f @^-1` A). Arguments pushforward {d1 d2 T1 T2 R} m {f}. Section pushforward_measure. @@ -1708,7 +2101,7 @@ Local Open Scope ereal_scope. Context d d' (T1 : measurableType d) (T2 : measurableType d') (R : realFieldType). Variables (m : {measure set T1 -> \bar R}) (f : T1 -> T2). -Hypothesis mf : measurable_fun setT f. +Hypothesis mf : measurable_fun [set: T1] f. Let pushforward0 : pushforward m mf set0 = 0. Proof. by rewrite /pushforward preimage_set0 measure0. Qed. @@ -1733,7 +2126,7 @@ End pushforward_measure. Section dirac_measure. Local Open Scope ereal_scope. -Context d (T : measurableType d) (a : T) (R : realFieldType). +Context d (T : sigmaRingType d) (a : T) (R : realFieldType). Definition dirac (A : set T) : \bar R := (\1_A a)%:E. @@ -1769,7 +2162,7 @@ Notation "\d_ a" := (dirac a) : ring_scope. Section dirac_lemmas_realFieldType. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realFieldType). +Context d (T : sigmaRingType d) (R : realFieldType). Lemma diracE a (A : set T) : \d_a A = (a \in A)%:R%:E :> \bar R. Proof. by rewrite /dirac indicE. Qed. @@ -1784,7 +2177,7 @@ End dirac_lemmas_realFieldType. Section dirac_lemmas. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). +Context d (T : sigmaRingType d) (R : realType). Lemma finite_card_sum (A : set T) : finite_set A -> \esum_(i in A) 1 = (#|` fset_set A|%:R)%:E :> \bar R. @@ -1818,7 +2211,7 @@ End dirac_lemmas. Section measure_sum. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). +Context d (T : sigmaRingType d) (R : realType). Variables (m : {measure set T -> \bar R}^nat) (n : nat). Definition msum (A : set T) : \bar R := \sum_(k < n) m k A. @@ -1844,7 +2237,7 @@ Arguments msum {d T R}. Section measure_zero. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). +Context d (T : sigmaRingType d) (R : realFieldType). Definition mzero (A : set T) : \bar R := 0. @@ -1864,14 +2257,14 @@ HB.instance Definition _ := isMeasure.Build _ _ _ mzero End measure_zero. Arguments mzero {d T R}. -Lemma msum_mzero d (T : measurableType d) (R : realType) +Lemma msum_mzero d (T : sigmaRingType d) (R : realType) (m_ : {measure set T -> \bar R}^nat) : msum m_ 0 = mzero. Proof. by apply/funext => A/=; rewrite /msum big_ord0. Qed. Section measure_add. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). +Context d (T : sigmaRingType d) (R : realType). Variables (m1 m2 : {measure set T -> \bar R}). Definition measure_add := msum (fun n => if n is 0%N then m1 else m2) 2. @@ -1883,7 +2276,7 @@ End measure_add. Section measure_scale. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realFieldType). +Context d (T : sigmaRingType d) (R : realFieldType). Variables (r : {nonneg R}) (m : {measure set T -> \bar R}). Definition mscale (A : set T) : \bar R := r%:num%:E * m A. @@ -1912,7 +2305,7 @@ Arguments mscale {d T R}. Section measure_series. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). +Context d (T : sigmaRingType d) (R : realType). Variables (m : {measure set T -> \bar R}^nat) (n : nat). Definition mseries (A : set T) : \bar R := \sum_(n <= k \bar R) (mD : measurable D) := fun X => f (X `&` D). Section measure_restr. -Context d (T : measurableType d) (R : realFieldType). +Context d (T : sigmaRingType d) (R : realFieldType). Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D). Local Notation restr := (mrestr mu mD). @@ -1983,7 +2376,7 @@ Definition counting (T : choiceType) (R : realType) (X : set T) : \bar R := Arguments counting {T R}. Section measure_count. -Context d (T : measurableType d) (R : realType). +Context d (T : sigmaRingType d) (R : realType). Variables (D : set T) (mD : measurable D). Local Notation counting := (@counting T R). @@ -2733,7 +3126,7 @@ move=> h U mU; rewrite fin_real// (lt_le_trans _ (measure_ge0 mu U))//=. by rewrite (le_lt_trans _ h)//= le_measure// inE. Qed. -Definition sfinite_measure d (T : measurableType d) (R : realType) +Definition sfinite_measure d (T : sigmaRingType d) (R : realType) (mu : set T -> \bar R) := exists2 s : {measure set T -> \bar R}^nat, forall n, fin_num_fun (s n) & @@ -2776,12 +3169,11 @@ apply: (@measure_sigma_additive _ _ _ mu (fun k => U `&` seqDU F k)). exact/trivIset_setIl/trivIset_seqDU. Qed. -HB.mixin Record isSFinite d (T : measurableType d) (R : realType) +HB.mixin Record isSFinite d (T : sigmaRingType d) (R : realType) (mu : set T -> \bar R) := { s_finite : sfinite_measure mu }. -HB.structure Definition SFiniteMeasure - d (T : measurableType d) (R : realType) := +HB.structure Definition SFiniteMeasure d (T : sigmaRingType d) (R : realType) := {mu of @Measure _ T R mu & isSFinite _ T R mu }. Arguments s_finite {d T R} _. @@ -2818,8 +3210,8 @@ Notation "{ 'sigma_finite_measure' 'set' T '->' '\bar' R }" := format "{ 'sigma_finite_measure' 'set' T '->' '\bar' R }") : ring_scope. -HB.factory Record Measure_isSigmaFinite d (T : measurableType d) (R : realType) - (mu : set T -> \bar R) of isMeasure _ _ _ mu := +HB.factory Record Measure_isSigmaFinite d (T : measurableType d) + (R : realType) (mu : set T -> \bar R) of isMeasure _ _ _ mu := { sigma_finiteT : sigma_finite setT mu }. HB.builders Context d (T : measurableType d) (R : realType) @@ -2834,11 +3226,11 @@ HB.instance Definition _ := @isSigmaFinite.Build _ _ _ mu sigma_finiteT. HB.end. -Lemma sigma_finite_mzero d (T : measurableType d) (R : realType) : +Lemma sigma_finite_mzero d (T : measurableType d) (R : realFieldType) : sigma_finite setT (@mzero d T R). Proof. by apply: fin_num_fun_sigma_finite => //; rewrite measure0. Qed. -HB.instance Definition _ d (T : measurableType d) (R : realType) := +HB.instance Definition _ d (T : measurableType d) (R : realFieldType) := @isSigmaFinite.Build d T R mzero (@sigma_finite_mzero d T R). Lemma sfinite_mzero d (T : measurableType d) (R : realType) : @@ -2858,7 +3250,7 @@ HB.structure Definition FinNumFun d (T : semiRingOfSetsType d) Notation "'@SigmaFinite_isFinite.Build' d T R k" := (@isFinite.Build d T R k) (at level 2, d, T, R, k at next level, only parsing). -HB.structure Definition FiniteMeasure d (T : measurableType d) (R : realType) := +HB.structure Definition FiniteMeasure d (T : sigmaRingType d) (R : realType) := { k of @SigmaFiniteMeasure _ _ _ k & isFinite _ T R k }. Arguments fin_num_measure {d T R} _. @@ -2894,12 +3286,12 @@ HB.instance Definition _ := @isFinite.Build d T R k finite. HB.end. -HB.factory Record Measure_isSFinite d (T : measurableType d) +HB.factory Record Measure_isSFinite d (T : sigmaRingType d) (R : realType) (k : set T -> \bar R) of isMeasure _ _ _ k := { s_finite : exists s : {finite_measure set T -> \bar R}^nat, forall U, measurable U -> k U = mseries s 0 U }. -HB.builders Context d (T : measurableType d) (R : realType) +HB.builders Context d (T : sigmaRingType d) (R : realType) k of Measure_isSFinite d T R k. Let sfinite : sfinite_measure k. @@ -2971,7 +3363,7 @@ HB.instance Definition _ := Measure_isFinite.Build _ _ _ restr restr_fin. End measure_frestr. -HB.mixin Record isSubProbability d (T : measurableType d) (R : realType) +HB.mixin Record isSubProbability d (T : sigmaRingType d) (R : realType) (P : set T -> \bar R) := { sprobability_setT : P setT <= 1%E }. #[short(type=subprobability)] @@ -3102,7 +3494,7 @@ End pdirac. HB.instance Definition _ d (T : measurableType d) (R : realType) := isPointed.Build (probability T R) [the probability _ _ of dirac point]. -Section dist_salgebra_instance. +Section dist_sigma_algebra_instance. Context d (T : measurableType d) (R : realType). Definition mset (U : set T) (r : R) := [set mu : probability T R | mu U < r%:E]. @@ -3124,9 +3516,9 @@ Definition pset : set (set (probability T R)) := [set mset U r | r in `[0%R,1%R] & U in measurable]. Definition pprobability : measurableType pset.-sigma := - [the measurableType _ of salgebraType pset]. + [the measurableType _ of g_sigma_algebraType pset]. -End dist_salgebra_instance. +End dist_sigma_algebra_instance. Lemma sigma_finite_counting (R : realType) : sigma_finite [set: nat] (@counting _ R). @@ -3250,14 +3642,15 @@ Proof. move=> mF mbigcupF ndF. have Binter : trivIset setT (seqD F) := trivIset_seqD ndF. have FBE : forall n, F n.+1 = F n `|` seqD F n.+1 := setU_seqD ndF. -have FE n : F n = \big[setU/set0]_(i < n.+1) (seqD F) i := eq_bigsetU_seqD n ndF. -rewrite eq_bigcup_seqD. -have mB i : measurable (seqD F i) by elim: i => * //=; apply: measurableD. +have FE n : \big[setU/set0]_(i < n.+1) (seqD F) i = F n := + nondecreasing_bigsetU_seqD n ndF. +rewrite -eq_bigcup_seqD. +have mB i : measurable (seqD F i) by elim: i => * //=; exact: measurableD. apply: cvg_trans (measure_semi_sigma_additive _ mB Binter _); last first. - by rewrite -eq_bigcup_seqD. -apply: (@cvg_trans _ ((fun n => \sum_(i < n.+1) mu (seqD F i)) @ \oo)). + by rewrite eq_bigcup_seqD. +apply: (@cvg_trans _ (\sum_(i < n.+1) mu (seqD F i) @[n --> \oo])). rewrite [X in _ --> X @ \oo](_ : _ = mu \o F) // funeqE => n. - by rewrite -measure_semi_additive // -?FE// => -[|k]. + by rewrite -measure_semi_additive ?FE// => -[|]. move=> S [n _] nS; exists n => // m nm. under eq_fun do rewrite -(big_mkord predT (mu \o seqD F)). exact/(nS m.+1)/(leq_trans nm). @@ -3275,7 +3668,7 @@ have F0E r : mu (F 0%N) - (mu (F 0%N) - r) = r. by rewrite oppeB ?addeA ?subee ?add0e// fin_num_adde_defr. rewrite -[x in _ --> x] F0E. have -> : mu \o F = fun n => mu (F 0%N) - (mu (F 0%N) - mu (F n)). - by apply:funext => n; rewrite F0E. + by apply: funext => n; rewrite F0E. apply: cvgeB; rewrite ?fin_num_adde_defr//; first exact: cvg_cst. have -> : \bigcap_n F n = F 0%N `&` \bigcap_n F n. by rewrite setIidr//; exact: bigcap_inf. @@ -3291,6 +3684,50 @@ Qed. End measure_continuity. +Section g_sigma_algebra_measure_unique_trace. +Context d (R : realType) (T : measurableType d). +Variables (G : set (set T)) (D : set T) (mD : measurable D). +Let H := [set X | G X /\ X `<=` D] (* "trace" of G wrt D *). +Hypotheses (Hm : H `<=` measurable) (setIH : setI_closed H). +Variables m1 m2 : {measure set T -> \bar R}. +Hypothesis m1m2D : m1 D = m2 D. +Hypotheses (m1m2 : forall A, H A -> m1 A = m2 A) (m1oo : (m1 D < +oo)%E). + +Lemma g_sigma_algebra_measure_unique_trace : + (forall X, (<>) X -> X `<=` D) -> forall X, <> X -> + m1 X = m2 X. +Proof. +move=> sDHD; set E := [set A | [/\ measurable A, m1 A = m2 A & A `<=` D] ]. +have HE : H `<=` E. + by move=> X HX; rewrite /E /=; split; [exact: Hm|exact: m1m2|case: HX]. +have setDE : setD_closed E. + move=> A B BA [mA m1m2A AD] [mB m1m2B BD]; split; first exact: measurableD. + - rewrite measureD//; last first. + by rewrite (le_lt_trans _ m1oo)//; apply: le_measure => // /[!inE]. + rewrite setIidr//= m1m2A m1m2B measureD// ?setIidr//. + by rewrite (le_lt_trans _ m1oo)//= -m1m2A; apply: le_measure => // /[!inE]. + - by rewrite setDE; apply: subIset; left. +have ndE : ndseq_closed E. + move=> A ndA EA; split; have mA n : measurable (A n) by have [] := EA n. + - exact: bigcupT_measurable. + - transitivity (limn (m1 \o A)). + apply/esym/cvg_lim=>//. + exact/(nondecreasing_cvg_mu mA _ ndA)/bigcupT_measurable. + transitivity (limn (m2 \o A)). + by apply/congr_lim/funext => n; have [] := EA n. + apply/cvg_lim => //. + exact/(nondecreasing_cvg_mu mA _ ndA)/bigcupT_measurable. + - by apply: bigcup_sub => n; have [] := EA n. +have sDHE : <> `<=` E. + by apply: lambda_system_subset => //; split => //; [move=> ? []|split]. +by move=> X /sDHE[]. +Qed. + +End g_sigma_algebra_measure_unique_trace. +Arguments g_sigma_algebra_measure_unique_trace {d R T} G D. +#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `g_sigma_algebra_measure_unique_trace`")] +Notation g_salgebra_measure_unique_trace := g_sigma_algebra_measure_unique_trace (only parsing). + Section boole_inequality. Context d (R : realFieldType) (T : ringOfSetsType d). Variable mu : {content set T -> \bar R}. @@ -3413,7 +3850,7 @@ Qed. End negligible_ringOfSetsType. -Lemma negligible_bigcup d (T : measurableType d) (R : realFieldType) +Lemma negligible_bigcup d (T : sigmaRingType d) (R : realFieldType) (mu : {measure set T -> \bar R}) (F : (set T)^nat) : (forall k, mu.-negligible (F k)) -> mu.-negligible (\bigcup_k F k). Proof. @@ -3497,7 +3934,7 @@ Qed. Section ae_eq. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). +Context d (T : sigmaRingType d) (R : realType). Variables (mu : {measure set T -> \bar R}) (D : set T). Implicit Types f g h i : T -> \bar R. @@ -3544,7 +3981,7 @@ Proof. by apply: filterS => x /[apply] /= ->. Qed. End ae_eq. Section ae_eq_lemmas. -Context d (T : measurableType d) (R : realType). +Context d (T : sigmaRingType d) (R : realType). Implicit Types mu : {measure set T -> \bar R}. Lemma ae_eq_subset mu A B f g : B `<=` A -> ae_eq mu A f g -> ae_eq mu B f g. @@ -4101,47 +4538,7 @@ HB.instance Definition _ := isOuterMeasure.Build End outer_measure_of_content. -Section g_salgebra_measure_unique_trace. -Context d (R : realType) (T : measurableType d). -Variables (G : set (set T)) (D : set T) (mD : measurable D). -Let H := [set X | G X /\ X `<=` D] (* "trace" of G wrt D *). -Hypotheses (Hm : H `<=` measurable) (setIH : setI_closed H) (HD : H D). -Variables m1 m2 : {measure set T -> \bar R}. -Hypotheses (m1m2 : forall A, H A -> m1 A = m2 A) (m1oo : (m1 D < +oo)%E). - -Lemma g_salgebra_measure_unique_trace : - (forall X, (<>) X -> X `<=` D) -> forall X, <> X -> - m1 X = m2 X. -Proof. -move=> sDHD; set E := [set A | [/\ measurable A, m1 A = m2 A & A `<=` D] ]. -have HE : H `<=` E. - by move=> X HX; rewrite /E /=; split; [exact: Hm|exact: m1m2|case: HX]. -have setDE : setD_closed E. - move=> A B BA [mA m1m2A AD] [mB m1m2B BD]; split; first exact: measurableD. - - rewrite measureD//; last first. - by rewrite (le_lt_trans _ m1oo)//; apply: le_measure => // /[!inE]. - rewrite setIidr//= m1m2A m1m2B measureD// ?setIidr//. - by rewrite (le_lt_trans _ m1oo)//= -m1m2A; apply: le_measure => // /[!inE]. - - by rewrite setDE; apply: subIset; left. -have ndE : ndseq_closed E. - move=> A ndA EA; split; have mA n : measurable (A n) by have [] := EA n. - - exact: bigcupT_measurable. - - transitivity (limn (m1 \o A)). - apply/esym/cvg_lim=>//. - exact/(nondecreasing_cvg_mu mA _ ndA)/bigcupT_measurable. - transitivity (limn (m2 \o A)). - by apply/congr_lim/funext => n; have [] := EA n. - apply/cvg_lim => //. - exact/(nondecreasing_cvg_mu mA _ ndA)/bigcupT_measurable. - - by apply: bigcup_sub => n; have [] := EA n. -have sDHE : <> `<=` E. - by apply: monotone_class_subset => //; split => //; [move=> A []|exact/HE]. -by move=> X /sDHE[]. -Qed. - -End g_salgebra_measure_unique_trace. - -Section g_salgebra_measure_unique. +Section g_sigma_algebra_measure_unique. Context d (R : realType) (T : measurableType d). Variable G : set (set T). Hypothesis Gm : G `<=` measurable. @@ -4150,11 +4547,11 @@ Hypotheses Gg : forall i, G (g i). Hypothesis g_cover : \bigcup_k (g k) = setT. Variables m1 m2 : {measure set T -> \bar R}. -Lemma g_salgebra_measure_unique_cover : +Lemma g_sigma_algebra_measure_unique_cover : (forall n A, <> A -> m1 (g n `&` A) = m2 (g n `&` A)) -> forall A, <> A -> m1 A = m2 A. Proof. -pose GT := [the ringOfSetsType _ of salgebraType G]. +pose GT : ringOfSetsType G.-sigma:= g_sigma_algebraType G. move=> sGm1m2; pose g' k := \bigcup_(i < k) g i. have sGm := smallest_sub (@sigma_algebra_measurable _ T) Gm. have Gg' i : <> (g' i). @@ -4193,7 +4590,7 @@ Hypothesis setIG : setI_closed G. Hypothesis m1m2 : forall A, G A -> m1 A = m2 A. Hypothesis m1goo : forall k, (m1 (g k) < +oo)%E. -Lemma g_salgebra_measure_unique : forall E, <> E -> m1 E = m2 E. +Lemma g_sigma_algebra_measure_unique : forall E, <> E -> m1 E = m2 E. Proof. pose G_ n := [set X | G X /\ X `<=` g n]. (* "trace" *) have G_E n : G_ n = [set g n `&` C | C in G]. @@ -4209,19 +4606,24 @@ have preimg_gGE n : preimage_class (g n) id G = G_ n. rewrite eqEsubset; split => [_ [Y GY <-]|]. by rewrite preimage_id G_E /=; exists Y => //; rewrite setIC. by move=> X [GX Xgn]; exists X => //; rewrite preimage_id setIidr. -apply: g_salgebra_measure_unique_cover => //. -move=> n A sGA; apply: (@g_salgebra_measure_unique_trace _ _ _ G (g n)) => //. +apply: g_sigma_algebra_measure_unique_cover => //. +move=> n A sGA; apply: (g_sigma_algebra_measure_unique_trace G (g n)) => //. - exact: Gm. - by move=> ? [? _]; exact/Gm. - by move=> ? ? [? ?] [? ?]; split; [exact: setIG|apply: subIset; tauto]. -- by split. +- exact: m1m2. - by move=> ? [? ?]; exact: m1m2. - move=> X; rewrite -/(G_ n) -preimg_gGE -gIsGE. by case=> B sGB <-{X}; apply: subIset; left. - by rewrite -/(G_ n) -preimg_gGE -gIsGE; exists A. Qed. -End g_salgebra_measure_unique. +End g_sigma_algebra_measure_unique. +Arguments g_sigma_algebra_measure_unique {d R T} G. +#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `g_sigma_algebra_measure_unique_cover`")] +Notation g_salgebra_measure_unique_cover := g_sigma_algebra_measure_unique_cover (only parsing). +#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `g_sigma_algebra_measure_unique`")] +Notation g_salgebra_measure_unique := g_sigma_algebra_measure_unique (only parsing). Section measure_unique. Context d (R : realType) (T : measurableType d). @@ -4235,7 +4637,7 @@ Hypothesis m1goo : forall k, (m1 (g k) < +oo)%E. Lemma measure_unique A : measurable A -> m1 A = m2 A. Proof. -move=> mA; apply: (@g_salgebra_measure_unique _ _ _ G); rewrite -?mG//. +move=> mA; apply: (g_sigma_algebra_measure_unique G); rewrite -?mG//. by rewrite mG; exact: sub_sigma_algebra. Qed. @@ -4358,7 +4760,7 @@ near=> n; apply: lee_sum => i _; rewrite -measure_semi_additive2. - by rewrite setIACA setICr setI0. Unshelve. all: by end_near. Qed. -Let I := [the measurableType _ of salgebraType (@measurable _ T)]. +Let I := [the measurableType _ of g_sigma_algebraType (@measurable _ T)]. Definition measure_extension : set I -> \bar R := mu^*. @@ -4481,7 +4883,7 @@ rewrite setMT setTM; apply: measurableI. - by apply: sub_sigma_algebra; right; exists B => //; rewrite setTI. Qed. -Section product_salgebra_measurableType. +Section product_salgebra_algebraOfSetsType. Context d1 d2 (T1 : algebraOfSetsType d1) (T2 : algebraOfSetsType d2). Let M1 := @measurable _ T1. Let M2 := @measurable _ T2. @@ -4503,7 +4905,7 @@ apply: smallest_sub; first exact: smallest_sigma_algebra. by move=> _ [A MA] [B MB] <-; apply: measurableM => //; exact: sub_sigma_algebra. Qed. -End product_salgebra_measurableType. +End product_salgebra_algebraOfSetsType. Section product_salgebra_g_measurableTypeR. Context d1 (T1 : algebraOfSetsType d1) (T2 : pointedType) (C2 : set (set T2)). @@ -4511,7 +4913,7 @@ Hypothesis setTC2 : setT `<=` C2. (* NB: useful? *) Lemma measurable_prod_g_measurableTypeR : - @measurable _ [the measurableType _ of T1 * salgebraType C2 : Type] + @measurable _ [the measurableType _ of T1 * g_sigma_algebraType C2 : Type] = <>. Proof. rewrite measurable_prod_measurableType //; congr (<>). @@ -4527,8 +4929,8 @@ Variables (T1 T2 : pointedType) (C1 : set (set T1)) (C2 : set (set T2)). Hypotheses (setTC1 : setT `<=` C1) (setTC2 : setT `<=` C2). Lemma measurable_prod_g_measurableType : - @measurable _ [the measurableType _ of salgebraType C1 * salgebraType C2 : Type] - = <>. + @measurable _ (g_sigma_algebraType C1 * g_sigma_algebraType C2)%type = + <>. Proof. rewrite measurable_prod_measurableType //; congr (<>). rewrite predeqE => X; split=> [[A mA] [B mB] <-{X}|[A C1A] [B C2B] <-{X}]. diff --git a/theories/probability.v b/theories/probability.v index 85727757f..576b95ccb 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -655,8 +655,7 @@ have le (u : R) : (0 <= u)%R -> - rewrite -[[set _ | _]]setTI inE; apply: emeasurable_fun_c_infty => [//|]. rewrite EFin_measurable_fun [X in measurable_fun _ X](_ : _ = (fun x => x ^+ 2) \o (fun x => Y x + u))%R//. - apply/measurableT_comp => //; apply/measurable_funD => //. - by rewrite -EFin_measurable_fun; apply: measurable_int Y1. + by apply/measurableT_comp => //; apply/measurable_funD. set eps := ((lambda + u) ^ 2)%R. have peps : (0 < eps)%R by rewrite exprz_gt0 ?ltr_wpDr. rewrite (lee_pdivl_mulr _ _ peps) muleC. diff --git a/theories/sequences.v b/theories/sequences.v index b77a383a3..cdd82622d 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -301,37 +301,47 @@ by move=> ?; have [?|?] := pselect (F n x); [left | right]. by move=> -[|[]//]; move: x; exact/subsetPset/ndF. Qed. -Lemma eq_bigsetU_seqD F n : nondecreasing_seq F -> - F n = \big[setU/set0]_(i < n.+1) seqD F i. +Lemma nondecreasing_bigsetU_seqD F n : nondecreasing_seq F -> + \big[setU/set0]_(i < n.+1) seqD F i = F n. Proof. move=> ndF; elim: n => [|n ih]; rewrite funeqE => x; rewrite propeqE; split. -- by move=> ?; rewrite big_ord_recl big_ord0; left. - by rewrite big_ord_recl big_ord0 setU0. -- rewrite (setU_seqD ndF) => -[|/=]. - by rewrite big_ord_recr /= -ih => Fnx; left. - by move=> -[Fn1x Fnx]; rewrite big_ord_recr /=; right. -- by rewrite big_ord_recr /= -ih => -[|[]//]; move: x; exact/subsetPset/ndF. +- by move=> ?; rewrite big_ord_recl big_ord0; left. +- by rewrite big_ord_recr /= ih => -[|[]//]; move: x; exact/subsetPset/ndF. +- rewrite (setU_seqD ndF) => -[|/= [Fn1x Fnx]]. + by rewrite big_ord_recr /= -ih => Fnx; left. + by rewrite big_ord_recr /=; right. Qed. -Lemma eq_bigcup_seqD F : \bigcup_n F n = \bigcup_n seqD F n. +Lemma eq_bigcup_seqD F : \bigcup_n seqD F n = \bigcup_n F n. Proof. -rewrite funeqE => x; rewrite propeqE; split. - case; elim=> [_ F0x|n ih _ Fn1x]; first by exists O. - have [|Fnx] := pselect (F n x); last by exists n.+1. - by move=> /(ih I)[m _ Fmx]; exists m. -case; elim=> [_ /= F0x|n ih _ /= [Fn1x Fnx]]; by [exists O | exists n.+1]. +apply/seteqP; split => [x []|x []]. + by elim=> [_ /= F0x|n ih _ /= [Fn1x Fnx]]; [exists O | exists n.+1]. +elim=> [_ F0x|n ih _ Fn1x]; first by exists O. +have [|Fnx] := pselect (F n x); last by exists n.+1. +by move=> /(ih I)[m _ Fmx]; exists m. Qed. Lemma eq_bigcup_seqD_bigsetU F : \bigcup_n (seqD (fun n => \big[setU/set0]_(i < n.+1) F i) n) = \bigcup_n F n. Proof. -rewrite -(@eq_bigcup_seqD (fun n => \big[setU/set0]_(i < n.+1) F i)). +rewrite (eq_bigcup_seqD (fun n => \big[setU/set0]_(i < n.+1) F i)). rewrite eqEsubset; split => [t [i _]|t [i _ Fit]]. by rewrite -bigcup_seq_cond => -[/= j _ Fjt]; exists j. by exists i => //; rewrite big_ord_recr /=; right. Qed. +Lemma bigcup_bigsetU_bigcup F : + \bigcup_k \big[setU/set0]_(i < k.+1) F i = \bigcup_k F k. +Proof. +apply/seteqP; split=> [x [i _]|x [i _ Fix]]. + by rewrite -bigcup_mkord => -[j _ Fjx]; exists j. +by exists i => //; rewrite big_ord_recr/=; right. +Qed. + End seqD. +#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed to `nondecreasing_bigsetU_seqD`")] +Notation eq_bigsetU_seqD := nondecreasing_bigsetU_seqD (only parsing). (** Convergence of patched sequences *)