From a93338c2ec163d8439cec8762847f5485eb5c958 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 26 Dec 2024 22:49:36 +0900 Subject: [PATCH] renaming --- CHANGELOG_UNRELEASED.md | 107 +++++++--------------------------------- theories/independence.v | 101 ++++++++++++++++++------------------- theories/kernel.v | 51 +++++++++++++++++-- theories/measure.v | 56 ++++++++++----------- theories/probability.v | 28 +++++------ 5 files changed, 158 insertions(+), 185 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d14913fda..3b548d496 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -14,10 +14,21 @@ + lemmas `horner0_ext`, `hornerD_ext`, `horner_scale_ext`, `hornerC_ext`, `derivable_horner`, `derivE`, `continuous_horner` + instance `is_derive_poly` -- in `mathcomp_extra.v`: - + lemma `partition_disjoint_bigfcup` -- in `lebesgue_measure.v`: - + lemma `measurable_indicP` + +- in `lebesgue_integral.v`: + + lemmas `integral_fin_num_abs`, `Rintegral_cst`, `le_Rintegral` + +- new file `pi_irrational.v`: + + lemmas `measurable_poly` + + definition `rational` + + module `pi_irrational` + + lemma `pi_irrationnal` + +- in `numfun.v` + + lemmas `funeposE`, `funenegE`, `funepos_comp`, `funeneg_comp` + +- in `classical_sets.v`: + + lemmas `xsectionE`, `ysectionE` - in `numfun.v`: + defintions `funrpos`, `funrneg` with notations `^\+` and `^\-` @@ -29,47 +40,26 @@ - in `measure.v`: + lemma `preimage_class_comp` - + defintions `mapping_display`, `g_sigma_algebra_mappingType`, `g_sigma_algebra_mapping`, - notations `.-mapping`, `.-mapping.-measurable` + + defintions `preimage_display`, `g_sigma_algebra_preimageType`, `g_sigma_algebra_preimage`, + notations `.-preimage`, `.-preimage.-measurable` - in `lebesgue_measure.v`: + lemmas `measurable_funrpos`, `measurable_funrneg` -- in `lebesgue_integral.v`: - + lemmas `integral_fin_num_abs`, `Rintegral_cst`, `le_Rintegral` - -- new file `pi_irrational.v`: - + lemmas `measurable_poly` - + definition `rational` - + module `pi_irrational` - + lemma `pi_irrationnal` -- in `constructive_ereal.v`: - + notations `\prod` in scope ereal_scope - + lemmas `prode_ge0`, `prode_fin_num` -- in `probability.v`: - + lemma `expectation_def` - + notation `'M_` - - new file `independence.v`: + lemma `expectationM_ge0` + definition `independent_events` + definition `mutual_independence` + definition `independent_RVs` + definition `independent_RVs2` - + lemmas `g_sigma_algebra_mapping_comp`, `g_sigma_algebra_mapping_funrpos`, - `g_sigma_algebra_mapping_funrneg` + + lemmas `g_sigma_algebra_preimage_comp`, `g_sigma_algebra_preimage_funrpos`, + `g_sigma_algebra_preimage_funrneg` + lemmas `independent_RVs2_comp`, `independent_RVs2_funrposneg`, `independent_RVs2_funrnegpos`, `independent_RVs2_funrnegneg`, `independent_RVs2_funrpospos` + lemma `expectationM_ge0`, `integrable_expectationM`, `independent_integrableM`, ` expectation_prod` -- in `numfun.v` - + lemmas `funeposE`, `funenegE`, `funepos_comp`, `funeneg_comp` - -- in `classical_sets.v`: - + lemmas `xsectionE`, `ysectionE` - ### Changed - in `lebesgue_integrale.v` @@ -95,33 +85,6 @@ + `sigma_algebra_image_class` -> `sigma_algebra_image` + `sigma_algebra_preimage_classE` -> `g_sigma_preimageE` + `preimage_classes_comp` -> `g_sigma_preimageU_comp` - -### Renamed - -- in `lebesgue_measure.v`: - + `measurable_fun_indic` -> `measurable_indic` - + `emeasurable_fun_sum` -> `emeasurable_sum` - + `emeasurable_fun_fsum` -> `emeasurable_fsum` - + `ge0_emeasurable_fun_sum` -> `ge0_emeasurable_sum` -- in `probability.v`: - + `expectationM` -> `expectationZl` - -- in `classical_sets.v`: - + `preimage_itv_o_infty` -> `preimage_itvoy` - + `preimage_itv_c_infty` -> `preimage_itvcy` - + `preimage_itv_infty_o` -> `preimage_itvNyo` - + `preimage_itv_infty_c` -> `preimage_itvNyc` - -- in `constructive_ereal.v`: - + `maxeMr` -> `maxe_pMr` - + `maxeMl` -> `maxe_pMl` - + `mineMr` -> `mine_pMr` - + `mineMl` -> `mine_pMl` - -- in `probability.v`: - + `integral_distribution` -> `ge0_integral_distribution` - -- file `homotopy_theory/path.v` -> `homotopy_theory/continuous_path.v` ### Generalized @@ -143,38 +106,6 @@ - in `sequences.v`: + notations `nneseries_pred0`, `eq_nneseries`, `nneseries0`, `ereal_cvgPpinfty`, `ereal_cvgPninfty` (were deprecated since 0.6.0) -- in `topology_structure.v`: - + lemma `closureC` - -- in file `lebesgue_integral.v`: - + lemma `approximation` - -### Removed - -- in `lebesgue_integral.v`: - + definition `cst_mfun` - + lemma `mfun_cst` - -- in `cardinality.v`: - + lemma `cst_fimfun_subproof` - -- in `lebesgue_integral.v`: - + lemma `cst_mfun_subproof` (use lemma `measurable_cst` instead) - + lemma `cst_nnfun_subproof` (turned into a `Let`) - + lemma `indic_mfun_subproof` (use lemma `measurable_fun_indic` instead) - -- in `lebesgue_integral.v`: - + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`) - + notation `measurable_fun_indic` (deprecation since 0.6.3) -- in `constructive_ereal.v` - + notation `lee_opp` (deprecated since 0.6.5) - + notation `lte_opp` (deprecated since 0.6.5) -- in `measure.v`: - + `dynkin_setI_bigsetI` (use `big_ind` instead) - -- in `lebesgue_measurable.v`: - + notation `measurable_fun_power_pos` (deprecated since 0.6.3) - + notation `measurable_power_pos` (deprecated since 0.6.4) ### Infrastructure diff --git a/theories/independence.v b/theories/independence.v index ce54443b3..80c4d15ff 100644 --- a/theories/independence.v +++ b/theories/independence.v @@ -213,7 +213,7 @@ Section mutual_independence_properties. Context {R : realType} d {T : measurableType d} (P : probability T R). Local Open Scope ereal_scope. -(**md see Achim Klenke's Probability Thery, Ch.2, sec.2.1, thm.2.13(i) *) +(**md see Achim Klenke's Probability Theory, Ch.2, sec.2.1, thm.2.13(i) *) Lemma mutual_independence_fset {I0 : choiceType} (I : {fset I0}) (F : I0 -> set_system T) : (forall i, i \in I -> F i `<=` measurable /\ (F i) [set: T]) -> @@ -237,7 +237,7 @@ rewrite -big_seq => ->. by rewrite !big_seq; apply: eq_bigr => i iJ; rewrite /E' iJ. Qed. -(**md see Achim Klenke's Probability Thery, Ch.2, sec.2.1, thm.2.13(ii) *) +(**md see Achim Klenke's Probability Theory, Ch.2, sec.2.1, thm.2.13(ii) *) Lemma mutual_independence_finiteS {I0 : choiceType} (I : set I0) (F : I0 -> set_system T) : mutual_independence P I F <-> @@ -255,7 +255,7 @@ split=> [i Ii|J JI E EF]. by have [_] := indeF _ JI; exact. Qed. -(**md see Achim Klenke's Probability Thery, Ch.2, sec.2.1, thm.2.13(iii) *) +(**md see Achim Klenke's Probability Theory, Ch.2, sec.2.1, thm.2.13(iii) *) Theorem mutual_independence_finite_g_sigma {I0 : choiceType} (I : set I0) (F : I0 -> set_system T) : (forall i, i \in I -> setI_closed (F i `|` [set set0])) -> @@ -437,7 +437,7 @@ apply/negP/set0P; exists j; split => //. exact/set_mem. Qed. -(**md see Achim Klenke's Probability Thery, Ch.2, sec.2.1, thm.2.13(iv) *) +(**md see Achim Klenke's Probability Theory, Ch.2, sec.2.1, thm.2.13(iv) *) Lemma mutual_independence_bigcup (K0 I0 : pointedType) (K : {fset K0}) (I_ : K0 -> set I0) (I : set I0) (F : I0 -> set_system T) : trivIset [set` K] (fun i => I_ i) -> @@ -482,28 +482,28 @@ Qed. End mutual_independence_properties. -Section g_sigma_algebra_mapping_lemmas. +Section g_sigma_algebra_preimage_lemmas. Context d {T : measurableType d} {R : realType}. -Lemma g_sigma_algebra_mapping_comp (X : {mfun T >-> R}) (f : R -> R) : +Lemma g_sigma_algebra_preimage_comp (X : {mfun T >-> R}) (f : R -> R) : measurable_fun setT f -> - g_sigma_algebra_mapping (f \o X)%R `<=` g_sigma_algebra_mapping X. + g_sigma_algebra_preimage (f \o X)%R `<=` g_sigma_algebra_preimage X. Proof. exact: preimage_set_system_comp. Qed. -Lemma g_sigma_algebra_mapping_funrpos (X : {mfun T >-> R}) : - g_sigma_algebra_mapping X^\+%R `<=` d.-measurable. +Lemma g_sigma_algebra_preimage_funrpos (X : {mfun T >-> R}) : + g_sigma_algebra_preimage X^\+%R `<=` d.-measurable. Proof. by move=> A/= -[B mB] <-; have := measurable_funrpos (measurable_funP X); exact. Qed. -Lemma g_sigma_algebra_mapping_funrneg (X : {mfun T >-> R}) : - g_sigma_algebra_mapping X^\-%R `<=` d.-measurable. +Lemma g_sigma_algebra_preimage_funrneg (X : {mfun T >-> R}) : + g_sigma_algebra_preimage X^\-%R `<=` d.-measurable. Proof. by move=> A/= -[B mB] <-; have := measurable_funrneg (measurable_funP X); exact. Qed. -End g_sigma_algebra_mapping_lemmas. -Arguments g_sigma_algebra_mapping_comp {d T R X} f. +End g_sigma_algebra_preimage_lemmas. +Arguments g_sigma_algebra_preimage_comp {d T R X} f. Section independent_RVs. Context {R : realType} d (T : measurableType d). @@ -513,7 +513,7 @@ Variable P : probability T R. Definition independent_RVs (I : set I0) (X : forall i : I0, {mfun T >-> T' i}) : Prop := - mutual_independence P I (fun i => g_sigma_algebra_mapping (X i)). + mutual_independence P I (fun i => g_sigma_algebra_preimage (X i)). End independent_RVs. @@ -532,7 +532,7 @@ Context {I0 : choiceType}. Context {d' : I0 -> _} (T' : forall i : I0, measurableType (d' i)). Variable P : probability T R. -(**md see Achim Klenke's Probability Thery, Ch.2, sec.2.1, thm.2.16 *) +(**md see Achim Klenke's Probability Theory, Ch.2, sec.2.1, thm.2.16 *) Theorem independent_generators (I : set I0) (F : forall i : I0, set_system (T' i)) (X : forall i, {RV P >-> T' i}) : (forall i, i \in I -> setI_closed (F i)) -> @@ -550,9 +550,9 @@ have closed_preimage i : I i -> setI_closed (preimage_set_system setT (X i) (F i - exact/mem_set. - by rewrite setTI. have gen_preimage i : I i -> - <> = g_sigma_algebra_mapping (X i). + <> = g_sigma_algebra_preimage (X i). move=> Ii. - rewrite /g_sigma_algebra_mapping AsF; last exact/mem_set. + rewrite /g_sigma_algebra_preimage AsF; last exact/mem_set. by rewrite -g_sigma_preimageE. rewrite /independent_RVs. suff: mutual_independence P I (fun i => <>). @@ -576,27 +576,27 @@ Lemma independent_RVs2_comp (X Y : {RV P >-> R}) (f g : {mfun R >-> R}) : Proof. move=> indeXY; split => /=. - move=> [] _ /= A. - + by rewrite /g_sigma_algebra_mapping/= /preimage_set_system/= => -[B mB <-]; + + by rewrite /g_sigma_algebra_preimage/= /preimage_set_system/= => -[B mB <-]; exact/measurableT_comp. - + by rewrite /g_sigma_algebra_mapping/= /preimage_set_system/= => -[B mB <-]; + + by rewrite /g_sigma_algebra_preimage/= /preimage_set_system/= => -[B mB <-]; exact/measurableT_comp. - move=> J _ E JE. apply indeXY => //= i iJ; have := JE _ iJ. by move: i {iJ} =>[|]//=; rewrite !inE => Eg; - exact: g_sigma_algebra_mapping_comp Eg. + exact: g_sigma_algebra_preimage_comp Eg. Qed. Lemma independent_RVs2_funrposneg (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\-. Proof. move=> indeXY; split=> [[|]/= _|J J2 E JE]. -- exact: g_sigma_algebra_mapping_funrneg. -- exact: g_sigma_algebra_mapping_funrpos. +- exact: g_sigma_algebra_preimage_funrneg. +- exact: g_sigma_algebra_preimage_funrpos. - apply indeXY => //= i iJ; have := JE _ iJ. move/J2 : iJ; move: i => [|]// _; rewrite !inE. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + + apply: (g_sigma_algebra_preimage_comp (fun x => maxr (- x) 0)%R). exact: measurable_funrneg. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R) => //. + + apply: (g_sigma_algebra_preimage_comp (fun x => maxr x 0)%R) => //. exact: measurable_funrpos. Qed. @@ -604,13 +604,13 @@ Lemma independent_RVs2_funrnegpos (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\+. Proof. move=> indeXY; split=> [/= [|]// _ |J J2 E JE]. -- exact: g_sigma_algebra_mapping_funrpos. -- exact: g_sigma_algebra_mapping_funrneg. +- exact: g_sigma_algebra_preimage_funrpos. +- exact: g_sigma_algebra_preimage_funrneg. - apply indeXY => //= i iJ; have := JE _ iJ. move/J2 : iJ; move: i => [|]// _; rewrite !inE. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + + apply: (g_sigma_algebra_preimage_comp (fun x => maxr x 0)%R). exact: measurable_funrpos. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + + apply: (g_sigma_algebra_preimage_comp (fun x => maxr (- x) 0)%R). exact: measurable_funrneg. Qed. @@ -618,13 +618,13 @@ Lemma independent_RVs2_funrnegneg (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\-. Proof. move=> indeXY; split=> [/= [|]// _ |J J2 E JE]. -- exact: g_sigma_algebra_mapping_funrneg. -- exact: g_sigma_algebra_mapping_funrneg. +- exact: g_sigma_algebra_preimage_funrneg. +- exact: g_sigma_algebra_preimage_funrneg. - apply indeXY => //= i iJ; have := JE _ iJ. move/J2 : iJ; move: i => [|]// _; rewrite !inE. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + + apply: (g_sigma_algebra_preimage_comp (fun x => maxr (- x) 0)%R). exact: measurable_funrneg. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + + apply: (g_sigma_algebra_preimage_comp (fun x => maxr (- x) 0)%R). exact: measurable_funrneg. Qed. @@ -632,22 +632,23 @@ Lemma independent_RVs2_funrpospos (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\+. Proof. move=> indeXY; split=> [/= [|]//= _ |J J2 E JE]. -- exact: g_sigma_algebra_mapping_funrpos. -- exact: g_sigma_algebra_mapping_funrpos. +- exact: g_sigma_algebra_preimage_funrpos. +- exact: g_sigma_algebra_preimage_funrpos. - apply indeXY => //= i iJ; have := JE _ iJ. move/J2 : iJ; move: i => [|]// _; rewrite !inE. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + + apply: (g_sigma_algebra_preimage_comp (fun x => maxr x 0)%R). exact: measurable_funrpos. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + + apply: (g_sigma_algebra_preimage_comp (fun x => maxr x 0)%R). exact: measurable_funrpos. Qed. End independent_RVs_lemmas. -Definition preimage_classes I (d : I -> measure_display) - (Tn : forall k, semiRingOfSetsType (d k)) (T : Type) (fn : forall k, T -> Tn k) := - <>. -Arguments preimage_classes {I} d Tn {T} fn. +Definition preimage_classes I0 (I : set I0) (d_ : forall i : I, measure_display) + (T_ : forall k : I, semiRingOfSetsType (d_ k)) (T : Type) + (f_ : forall k : I, T -> T_ k) := + <>. +Arguments preimage_classes {I0} I d_ T_ {T} f_. Lemma measurable_prod d [T : measurableType d] [R : realType] [D : set T] [I : eqType] (s : seq I) [h : I -> T -> R] : @@ -717,7 +718,7 @@ rewrite /independent_RVs2 /independent_RVs /mutual_independence /= => -[_]. move/(_ [fset false; true]%fset (@subsetT _ _) (fun b => if b then Y @^-1` B2 else X @^-1` B1)). rewrite !big_fsetU1 ?inE//= !big_seq_fset1/=. -apply => -[|] /= _; rewrite !inE; rewrite /g_sigma_algebra_mapping. +apply => -[|] /= _; rewrite !inE; rewrite /g_sigma_algebra_preimage. by exists B2 => //; rewrite setTI. by exists B1 => //; rewrite setTI. Qed. @@ -958,23 +959,23 @@ pose AY := dyadic_approx setT (EFin \o Y). pose BX := integer_approx setT (EFin \o X). pose BY := integer_approx setT (EFin \o Y). have mA (Z : {RV P >-> R}) m k : (k < m * 2 ^ m)%N -> - g_sigma_algebra_mapping Z (dyadic_approx setT (EFin \o Z) m k). - move=> mk; rewrite /g_sigma_algebra_mapping /dyadic_approx mk setTI. + g_sigma_algebra_preimage Z (dyadic_approx setT (EFin \o Z) m k). + move=> mk; rewrite /g_sigma_algebra_preimage /dyadic_approx mk setTI. rewrite /preimage_set_system/=; exists [set` dyadic_itv R m k] => //. rewrite setTI/=; apply/seteqP; split => z/=. by rewrite inE/= => Zz; exists (Z z). by rewrite inE/= => -[r rmk] [<-]. have mB (Z : {RV P >-> R}) k : - g_sigma_algebra_mapping Z (integer_approx setT (EFin \o Z) k). - rewrite /g_sigma_algebra_mapping /integer_approx setTI /preimage_set_system/=. + g_sigma_algebra_preimage Z (integer_approx setT (EFin \o Z) k). + rewrite /g_sigma_algebra_preimage /integer_approx setTI /preimage_set_system/=. by exists `[k%:R, +oo[%classic => //; rewrite setTI preimage_itvcy. have m1A (Z : {RV P >-> R}) : forall k, (k < n * 2 ^ n)%N -> measurable_fun setT - (\1_(dyadic_approx setT (EFin \o Z) n k) : g_sigma_algebra_mappingType Z -> R). + (\1_(dyadic_approx setT (EFin \o Z) n k) : g_sigma_algebra_preimageType Z -> R). move=> k kn. - exact/(@measurable_indicP _ (g_sigma_algebra_mappingType Z))/mA. + exact/(@measurable_indicP _ (g_sigma_algebra_preimageType Z))/mA. rewrite !inE => /orP[|]/eqP->{i} //=. - have : @measurable_fun _ _ (g_sigma_algebra_mappingType X) _ setT (X_ n). + have : @measurable_fun _ _ (g_sigma_algebra_preimageType X) _ setT (X_ n). rewrite nnsfun_approxE//. apply: measurable_funD => //=. apply: measurable_sum => //= k'; apply: measurable_funM => //. @@ -983,7 +984,7 @@ rewrite !inE => /orP[|]/eqP->{i} //=. by apply: measurable_indic; exact: mB. rewrite /measurable_fun => /(_ measurableT _ (measurable_set1 x)). by rewrite setTI. -have : @measurable_fun _ _ (g_sigma_algebra_mappingType Y) _ setT (Y_ n). +have : @measurable_fun _ _ (g_sigma_algebra_preimageType Y) _ setT (Y_ n). rewrite nnsfun_approxE//. apply: measurable_funD => //=. apply: measurable_sum => //= k'; apply: measurable_funM => //. @@ -1036,7 +1037,7 @@ exact/measurable_EFinP/measurable_funM. Qed. (* TODO: rename to expectationM when deprecation is removed *) -Lemma expectation_prod (X Y : {RV P >-> R}) : +Lemma expectation_mul (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> 'E_P [X * Y] = 'E_P [X] * 'E_P [Y]. diff --git a/theories/kernel.v b/theories/kernel.v index 872dab165..393c39ccf 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -187,7 +187,23 @@ have ? : m1 = m2. by subst m1; f_equal; f_equal; f_equal; apply/Prop_irrelevance. Qed. -HB.mixin Record SFiniteKernel_isFinite d d' +(* klenke def 8.25 *) +HB.mixin Record SFiniteKernel_isFiniteTransitionKernel + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) := { + finite_finite_transition_kernel : forall x, fin_num_fun (k x) }. + +#[short(type=finite_transition_kernel)] +HB.structure Definition FiniteTransitionKernel + d d' (X : measurableType d) (Y : measurableType d') (R : realType) := + { k of @SFiniteKernel _ _ _ _ _ k & + SFiniteKernel_isFiniteTransitionKernel _ _ X Y R k }. + +Reserved Notation "R .-ftker X ~> Y" + (at level 42, format "R .-ftker X ~> Y"). +Notation "R .-ftker X ~> Y" := (finite_transition_kernel X%type Y R). + +HB.mixin Record FiniteTransitionKernel_isFinite d d' (X : measurableType d) (Y : measurableType d') (R : realType) (k : X -> {measure set Y -> \bar R}) := { measure_uub : measure_fam_uub k }. @@ -195,8 +211,8 @@ HB.mixin Record SFiniteKernel_isFinite d d' #[short(type=finite_kernel)] HB.structure Definition FiniteKernel d d' (X : measurableType d) (Y : measurableType d') (R : realType) := - { k of @SFiniteKernel _ _ _ _ _ k & - SFiniteKernel_isFinite _ _ X Y R k }. + { k of @FiniteTransitionKernel _ _ _ _ _ k & + FiniteTransitionKernel_isFinite _ _ X Y R k }. Notation "R .-fker X ~> Y" := (finite_kernel X%type Y R). Arguments measure_uub {_ _ _ _ _} _. @@ -240,8 +256,20 @@ Qed. HB.instance Definition _ := @Kernel_isSFinite_subdef.Build d d' X Y R k sfinite_finite. +Let finite_transition_finite : forall x, fin_num_fun (k x). +Proof. +move=> x U mU. +have [r kr] := measure_uub. +rewrite ge0_fin_numE//. +rewrite (@le_lt_trans _ _ (k x setT)) ?le_measure ?inE//. +by rewrite (lt_trans (kr x)) ?ltry. +Qed. + +HB.instance Definition _ := + @SFiniteKernel_isFiniteTransitionKernel.Build d d' X Y R k finite_transition_finite. + HB.instance Definition _ := - @SFiniteKernel_isFinite.Build d d' X Y R k measure_uub. + @FiniteTransitionKernel_isFinite.Build d d' X Y R k measure_uub. HB.end. @@ -355,6 +383,20 @@ HB.factory Record Kernel_isSubProbability d d' (k : X -> {measure set Y -> \bar R}) of isKernel _ _ X Y R k := { sprob_kernel : ereal_sup [set k x [set: Y] | x in [set: X]] <= 1 }. +Lemma sprob_kernelP d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> set Y -> \bar R) : + (ereal_sup [set k x [set: _] | x in [set: _]] <= 1)%E <-> + forall x, (k x setT <= 1)%E. +Proof. +split => [H x|]. + apply: le_trans H. + apply: ereal_sup_ubound => /=. + by exists x. +move=> H. +apply: ub_ereal_sup => _ /= [z _ <-]. +exact: H. +Qed. + HB.builders Context d d' (X : measurableType d) (Y : measurableType d') (R : realType) k of Kernel_isSubProbability d d' X Y R k. @@ -764,7 +806,6 @@ HB.instance Definition _ (P : probability Y R):= End knormalize. -(* TODO: useful? *) Lemma measurable_fun_mnormalize d d' (X : measurableType d) (Y : measurableType d') (R : realType) (k : R.-ker X ~> Y) : measurable_fun [set: X] (fun x => mnormalize (k x) point : pprobability Y R). diff --git a/theories/measure.v b/theories/measure.v index 2c1a76146..754b63ea1 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -65,11 +65,11 @@ From HB Require Import structures. (* G.-sigma.-measurable A == A is measurable for the sigma-algebra <> *) (* g_sigma_algebraType G == the measurableType corresponding to <> *) (* This is an HB alias. *) -(* g_sigma_algebra_mapping f == sigma-algebra generated by the mapping f *) -(* g_sigma_algebra_mappingType f == the measurableType corresponding to *) -(* g_sigma_algebra_mapping f *) +(* g_sigma_algebra_preimage f == sigma-algebra generated by the function f *) +(* g_sigma_algebra_preimageType f == the measurableType corresponding to *) +(* g_sigma_algebra_preimage f *) (* This is an HB alias. *) -(* f.-mapping.-measurable A == A is measurable for g_sigma_algebra_mapping f *) +(* f.-preimage.-measurable A == A measurable for g_sigma_algebra_preimage f *) (* mu .-cara.-measurable == sigma-algebra of Caratheodory measurable sets *) (* ``` *) (* *) @@ -298,9 +298,9 @@ Reserved Notation "'\d_' a" (at level 8, a at level 2, format "'\d_' a"). Reserved Notation "G .-sigma" (at level 1, format "G .-sigma"). Reserved Notation "G .-sigma.-measurable" (at level 2, format "G .-sigma.-measurable"). -Reserved Notation "f .-mapping" (at level 1, format "f .-mapping"). -Reserved Notation "f .-mapping.-measurable" - (at level 2, format "f .-mapping.-measurable"). +Reserved Notation "f .-preimage" (at level 1, format "f .-preimage"). +Reserved Notation "f .-preimage.-measurable" + (at level 2, format "f .-preimage.-measurable"). Reserved Notation "d .-ring" (at level 1, format "d .-ring"). Reserved Notation "d .-ring.-measurable" (at level 2, format "d .-ring.-measurable"). @@ -1818,38 +1818,38 @@ Notation sigma_algebra_image_class := sigma_algebra_image (only parsing). #[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `g_sigma_preimageE`")] Notation sigma_algebra_preimage_classE := g_sigma_preimageE (only parsing). -Definition mapping_display {T T'} : (T -> T') -> measure_display. +Definition preimage_display {T T'} : (T -> T') -> measure_display. Proof. exact. Qed. -Definition g_sigma_algebra_mappingType d' (T : pointedType) +Definition g_sigma_algebra_preimageType d' (T : pointedType) (T' : measurableType d') (f : T -> T') : Type := T. -Definition g_sigma_algebra_mapping d' (T : pointedType) +Definition g_sigma_algebra_preimage d' (T : pointedType) (T' : measurableType d') (f : T -> T') := preimage_set_system setT f (@measurable _ T'). -Section mapping_generated_sigma_algebra. +Section preimage_generated_sigma_algebra. Context {d'} (T : pointedType) (T' : measurableType d'). Variable f : T -> T'. -Let mapping_set0 : g_sigma_algebra_mapping f set0. +Let preimage_set0 : g_sigma_algebra_preimage f set0. Proof. -rewrite /g_sigma_algebra_mapping /preimage_set_system/=. +rewrite /g_sigma_algebra_preimage /preimage_class/=. by exists set0 => //; rewrite preimage_set0 setI0. Qed. -Let mapping_setC A : - g_sigma_algebra_mapping f A -> g_sigma_algebra_mapping f (~` A). +Let preimage_setC A : + g_sigma_algebra_preimage f A -> g_sigma_algebra_preimage f (~` A). Proof. -rewrite /g_sigma_algebra_mapping /preimage_set_system/= => -[B mB] <-{A}. +rewrite /g_sigma_algebra_preimage /preimage_class/= => -[B mB] <-{A}. by exists (~` B); [exact: measurableC|rewrite !setTI preimage_setC]. Qed. -Let mapping_bigcup (F : (set T)^nat) : - (forall i, g_sigma_algebra_mapping f (F i)) -> - g_sigma_algebra_mapping f (\bigcup_i (F i)). +Let preimage_bigcup (F : (set T)^nat) : + (forall i, g_sigma_algebra_preimage f (F i)) -> + g_sigma_algebra_preimage f (\bigcup_i (F i)). Proof. -move=> mF; rewrite /g_sigma_algebra_mapping /preimage_set_system/=. +move=> mF; rewrite /g_sigma_algebra_preimage /preimage_class/=. pose g := fun i => sval (cid2 (mF i)). pose mg := fun i => svalP (cid2 (mF i)). exists (\bigcup_i g i). @@ -1858,17 +1858,17 @@ rewrite setTI /g preimage_bigcup; apply: eq_bigcupr => k _. by case: (mg k) => _; rewrite setTI. Qed. -HB.instance Definition _ := Pointed.on (g_sigma_algebra_mappingType f). +HB.instance Definition _ := Pointed.on (g_sigma_algebra_preimageType f). -HB.instance Definition _ := @isMeasurable.Build (mapping_display f) - (g_sigma_algebra_mappingType f) (g_sigma_algebra_mapping f) - mapping_set0 mapping_setC mapping_bigcup. +HB.instance Definition _ := @isMeasurable.Build (preimage_display f) + (g_sigma_algebra_preimageType f) (g_sigma_algebra_preimage f) + preimage_set0 preimage_setC preimage_bigcup. -End mapping_generated_sigma_algebra. +End preimage_generated_sigma_algebra. -Notation "f .-mapping" := (mapping_display f) : measure_display_scope. -Notation "f .-mapping.-measurable" := - (measurable : set (set (g_sigma_algebra_mappingType f))) : classical_set_scope. +Notation "f .-preimage" := (preimage_display f) : measure_display_scope. +Notation "f .-preimage.-measurable" := + (measurable : set (set (g_sigma_algebra_preimageType f))) : classical_set_scope. Local Open Scope ereal_scope. diff --git a/theories/probability.v b/theories/probability.v index 75b16a10c..5da093c03 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -912,7 +912,7 @@ Variable P : probability T R. Definition independent_RVs (I0 : choiceType) (I : set I0) (X : I0 -> {mfun T >-> T'}) : Prop := - mutual_independence P I (fun i => g_sigma_algebra_mapping (X i)). + mutual_independence P I (fun i => g_sigma_algebra_preimage (X i)). Definition independent_RVs2 (X Y : {mfun T >-> T'}) := independent_RVs [set: bool] [eta (fun=> cst point) with false |-> X, true |-> Y]. @@ -924,17 +924,17 @@ Context d {T : measurableType d} {R : realType}. Lemma g_sigma_algebra_mapping_comp (X : {mfun T >-> R}) (f : R -> R) : measurable_fun setT f -> - g_sigma_algebra_mapping (f \o X)%R `<=` g_sigma_algebra_mapping X. + g_sigma_algebra_preimage (f \o X)%R `<=` g_sigma_algebra_preimage X. Proof. exact: preimage_set_system_comp. Qed. Lemma g_sigma_algebra_mapping_funrpos (X : {mfun T >-> R}) : - g_sigma_algebra_mapping X^\+%R `<=` d.-measurable. + g_sigma_algebra_preimage X^\+%R `<=` d.-measurable. Proof. by move=> A/= -[B mB] <-; have := measurable_funrpos (measurable_funP X); exact. Qed. Lemma g_sigma_algebra_mapping_funrneg (X : {mfun T >-> R}) : - g_sigma_algebra_mapping X^\-%R `<=` d.-measurable. + g_sigma_algebra_preimage X^\-%R `<=` d.-measurable. Proof. by move=> A/= -[B mB] <-; have := measurable_funrneg (measurable_funP X); exact. Qed. @@ -952,9 +952,9 @@ Lemma independent_RVs2_comp (X Y : {RV P >-> R}) (f g : {mfun R >-> R}) : Proof. move=> indeXY; split => /=. - move=> [] _ /= A. - + by rewrite /g_sigma_algebra_mapping/= /preimage_set_system/= => -[B mB <-]; + + by rewrite /g_sigma_algebra_preimage/= /preimage_set_system/= => -[B mB <-]; exact/measurableT_comp. - + by rewrite /g_sigma_algebra_mapping/= /preimage_set_system/= => -[B mB <-]; + + by rewrite /g_sigma_algebra_preimage/= /preimage_set_system/= => -[B mB <-]; exact/measurableT_comp. - move=> J _ E JE. apply indeXY => //= i iJ; have := JE _ iJ. @@ -1163,23 +1163,23 @@ pose AY := dyadic_approx setT (EFin \o Y). pose BX := integer_approx setT (EFin \o X). pose BY := integer_approx setT (EFin \o Y). have mA (Z : {RV P >-> R}) m k : (k < m * 2 ^ m)%N -> - g_sigma_algebra_mapping Z (dyadic_approx setT (EFin \o Z) m k). - move=> mk; rewrite /g_sigma_algebra_mapping /dyadic_approx mk setTI. + g_sigma_algebra_preimage Z (dyadic_approx setT (EFin \o Z) m k). + move=> mk; rewrite /g_sigma_algebra_preimage /dyadic_approx mk setTI. rewrite /preimage_set_system/=; exists [set` dyadic_itv R m k] => //. rewrite setTI/=; apply/seteqP; split => z/=. by rewrite inE/= => Zz; exists (Z z). by rewrite inE/= => -[r rmk] [<-]. have mB (Z : {RV P >-> R}) k : - g_sigma_algebra_mapping Z (integer_approx setT (EFin \o Z) k). - rewrite /g_sigma_algebra_mapping /integer_approx setTI /preimage_set_system/=. + g_sigma_algebra_preimage Z (integer_approx setT (EFin \o Z) k). + rewrite /g_sigma_algebra_preimage /integer_approx setTI /preimage_set_system/=. by exists `[k%:R, +oo[%classic => //; rewrite setTI preimage_itvcy. have m1A (Z : {RV P >-> R}) : forall k, (k < n * 2 ^ n)%N -> measurable_fun setT - (\1_(dyadic_approx setT (EFin \o Z) n k) : g_sigma_algebra_mappingType Z -> R). + (\1_(dyadic_approx setT (EFin \o Z) n k) : g_sigma_algebra_preimageType Z -> R). move=> k kn. - exact/(@measurable_indicP _ (g_sigma_algebra_mappingType Z))/mA. + exact/(@measurable_indicP _ (g_sigma_algebra_preimageType Z))/mA. rewrite !inE => /orP[|]/eqP->{i} //=. - have : @measurable_fun _ _ (g_sigma_algebra_mappingType X) _ setT (X_ n). + have : @measurable_fun _ _ (g_sigma_algebra_preimageType X) _ setT (X_ n). rewrite nnsfun_approxE//. apply: measurable_funD => //=. apply: measurable_sum => //= k'; apply: measurable_funM => //. @@ -1188,7 +1188,7 @@ rewrite !inE => /orP[|]/eqP->{i} //=. by apply: measurable_indic; exact: mB. rewrite /measurable_fun => /(_ measurableT _ (measurable_set1 x)). by rewrite setTI. -have : @measurable_fun _ _ (g_sigma_algebra_mappingType Y) _ setT (Y_ n). +have : @measurable_fun _ _ (g_sigma_algebra_preimageType Y) _ setT (Y_ n). rewrite nnsfun_approxE//. apply: measurable_funD => //=. apply: measurable_sum => //= k'; apply: measurable_funM => //.