From 251817b88461ad97655c7ccfc08bf4aaf71b98cd Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 25 Feb 2023 19:38:58 +0900 Subject: [PATCH] generalize emeasurable_itv_* lemmas - a few pinfty/ninfty -> y/Ny renamings --- CHANGELOG_UNRELEASED.md | 16 ++++++ theories/lebesgue_integral.v | 2 +- theories/lebesgue_measure.v | 99 +++++++++++++++++------------------- 3 files changed, 65 insertions(+), 52 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 83b78d3ca..5c7f246c1 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -7,15 +7,31 @@ - in `contructive_ereal.v`: + lemmas `ereal_blatticeMixin`, `ereal_tblatticeMixin` + canonicals `ereal_blatticeType`, `ereal_tblatticeType` +- in `lebesgue_measure.v`: + + lemma `emeasurable_itv` ### Changed ### Renamed +- in `lebesgue_measure.v`: + + `punct_eitv_bnd_pinfty` -> `punct_eitv_bndy` + + `punct_eitv_ninfty_bnd` -> `punct_eitv_Nybnd` + + `eset1_pinfty` -> `eset1y` + + `eset1_ninfty` -> `eset1Ny` + + `ErealGenOInfty.measurable_set1_ninfty` -> `ErealGenOInfty.measurable_set1Ny` + + `ErealGenOInfty.measurable_set1_pinfty` -> `ErealGenOInfty.measurable_set1y` + + `ErealGenCInfty.measurable_set1_ninfty` -> `ErealGenCInfty.measurable_set1Ny` + + `ErealGenCInfty.measurable_set1_pinfty` -> `ErealGenCInfty.measurable_set1y` + ### Generalized ### Deprecated +- in `lebesgue_measure.v`: + + lemmas `emeasurable_itv_bnd_pinfty`, `emeasurable_itv_ninfty_bnd` + (use `emeasurable_itv` instead) + ### Removed ### Infrastructure diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 96bb978d3..0456e22cf 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -3607,7 +3607,7 @@ rewrite [X in measurable X](_ : _ = D `&` ~` N `&` (f @^-1` `]x%:E, +oo[) - by move=> [[]]. apply: measurableU. - rewrite setIAC; apply: measurableI; last exact/measurableC. - exact/mf/emeasurable_itv_bnd_pinfty. + exact/mf/emeasurable_itv. - by apply: cmu; exists N; split => //; rewrite setIAC; apply: subIset; right. Qed. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 64e5d5d34..94a5f5e7d 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -514,7 +514,7 @@ Variable R : realDomainType. Implicit Types (y : R) (b : bool). Local Open Scope ereal_scope. -Lemma punct_eitv_bnd_pinfty b y : [set` Interval (BSide b y%:E) +oo%O] = +Lemma punct_eitv_bndy b y : [set` Interval (BSide b y%:E) +oo%O] = EFin @` [set` Interval (BSide b y) +oo%O] `|` [set +oo]. Proof. rewrite predeqE => x; split; rewrite /= in_itv andbT. @@ -525,7 +525,7 @@ rewrite predeqE => x; split; rewrite /= in_itv andbT. + by case: b => /=; rewrite ?(ltry, leey). Qed. -Lemma punct_eitv_ninfty_bnd b y : [set` Interval -oo%O (BSide b y%:E)] = +Lemma punct_eitv_Nybnd b y : [set` Interval -oo%O (BSide b y%:E)] = [set -oo%E] `|` EFin @` [set x | x \in Interval -oo%O (BSide b y)]. Proof. rewrite predeqE => x; split; rewrite /= in_itv. @@ -711,21 +711,28 @@ Proof. by rewrite itv_oNyy. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_oNyy`")] Notation itv_oninfty_pinfty := __deprecated__itv_oninfty_pinfty. -Lemma emeasurable_itv_bnd_pinfty b (y : \bar R) : +Let emeasurable_itv_bndy b (y : \bar R) : measurable [set` Interval (BSide b y) +oo%O]. Proof. move: y => [y| |]. - exists [set` Interval (BSide b y) +oo%O]; first exact: measurable_itv. - by exists [set +oo%E]; [constructor|rewrite -punct_eitv_bnd_pinfty]. + by exists [set +oo%E]; [constructor|rewrite -punct_eitv_bndy]. - by case: b; rewrite ?itv_oyy ?itv_cyy. - case: b; first by rewrite itv_cNyy. by rewrite itv_oNyy; exact/measurableC. Qed. -Lemma emeasurable_itv_ninfty_bnd b (y : \bar R) : +Let emeasurable_itv_Nybnd b (y : \bar R) : measurable [set` Interval -oo%O (BSide b y)]. +Proof. by rewrite -setCitvr; exact/measurableC/emeasurable_itv_bndy. Qed. + +Lemma emeasurable_itv (i : interval (\bar R)) : + measurable ([set` i]%classic : set \bar R). Proof. -by rewrite -setCitvr; exact/measurableC/emeasurable_itv_bnd_pinfty. +rewrite -[X in measurable X]setCK; apply: measurableC. +rewrite set_interval.setCitv /=; apply: measurableU => [|]. +- by move: i => [[b1 i1|[|]] i2] /=; rewrite ?set_interval.set_itvE. +- by move: i => [i1 [b2 i2|[|]]] /=; rewrite ?set_interval.set_itvE. Qed. Definition elebesgue_measure : set \bar R -> \bar R := @@ -830,6 +837,12 @@ End salgebra_R_ssets. #[global] Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1| apply: emeasurable_set1] : core. +#[deprecated(since="mathcomp-analysis 0.6.2", + note="use `emeasurable_itv` instead")] +Notation emeasurable_itv_bnd_pinfty := emeasurable_itv. +#[deprecated(since="mathcomp-analysis 0.6.2", + note="use `emeasurable_itv` instead")] +Notation emeasurable_itv_ninfty_bnd := emeasurable_itv. Lemma measurable_fun_fine (R : realType) (D : set (\bar R)) : measurable D -> measurable_fun D fine. @@ -1020,24 +1033,16 @@ Hypotheses (mD : measurable D) (mf : measurable_fun D f). Implicit Types y : \bar R. Lemma emeasurable_fun_c_infty y : measurable (D `&` [set x | y <= f x]). -Proof. -by rewrite -preimage_itv_c_infty; exact/mf/emeasurable_itv_bnd_pinfty. -Qed. +Proof. by rewrite -preimage_itv_c_infty; exact/mf/emeasurable_itv. Qed. Lemma emeasurable_fun_o_infty y : measurable (D `&` [set x | y < f x]). -Proof. -by rewrite -preimage_itv_o_infty; exact/mf/emeasurable_itv_bnd_pinfty. -Qed. +Proof. by rewrite -preimage_itv_o_infty; exact/mf/emeasurable_itv. Qed. Lemma emeasurable_fun_infty_o y : measurable (D `&` [set x | f x < y]). -Proof. -by rewrite -preimage_itv_infty_o; exact/mf/emeasurable_itv_ninfty_bnd. -Qed. +Proof. by rewrite -preimage_itv_infty_o; exact/mf/emeasurable_itv. Qed. Lemma emeasurable_fun_infty_c y : measurable (D `&` [set x | f x <= y]). -Proof. -by rewrite -preimage_itv_infty_c; exact/mf/emeasurable_itv_ninfty_bnd. -Qed. +Proof. by rewrite -preimage_itv_infty_c; exact/mf/emeasurable_itv. Qed. Lemma emeasurable_fin_num : measurable (D `&` [set x | f x \is a fin_num]). Proof. @@ -1295,7 +1300,7 @@ rewrite predeqE => x; split=> [|]. + by rewrite lee_fin leNgt rks. Qed. -Lemma eset1_ninfty : +Lemma eset1Ny : [set -oo] = \bigcap_k `]-oo, (-k%:R%:E)[%classic :> set (\bar R). Proof. rewrite eqEsubset; split=> [_ -> i _ |]; first by rewrite /= in_itv /= ltNyr. @@ -1308,8 +1313,7 @@ rewrite ler_oppl -abszN natr_absz gtr0_norm; last first. by rewrite mulrNz ler_oppl opprK floor_le. Qed. -Lemma eset1_pinfty : - [set +oo] = \bigcap_k `]k%:R%:E, +oo[%classic :> set (\bar R). +Lemma eset1y : [set +oo] = \bigcap_k `]k%:R%:E, +oo[%classic :> set (\bar R). Proof. rewrite eqEsubset; split=> [_ -> i _/=|]; first by rewrite in_itv /= ltry. move=> [r| |/(_ O Logic.I)] // /(_ `|ceil r|%N Logic.I); rewrite /= in_itv /=. @@ -1329,17 +1333,17 @@ Local Open Scope ereal_scope. Definition G := [set A : set \bar R | exists r, A = `]r%:E, +oo[%classic]. -Lemma measurable_set1_ninfty : G.-sigma.-measurable [set -oo]. +Lemma measurable_set1Ny : G.-sigma.-measurable [set -oo]. Proof. -rewrite eset1_ninfty; 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. by exists (- (i%:R + j.+1%:R^-1))%R; rewrite opprD. Qed. -Lemma measurable_set1_pinfty : G.-sigma.-measurable [set +oo]. +Lemma measurable_set1y : G.-sigma.-measurable [set +oo]. Proof. -rewrite eset1_pinfty; apply: bigcapT_measurable => i. +rewrite eset1y; apply: bigcapT_measurable => i. by apply: sub_sigma_algebra; exists i%:R. Qed. @@ -1354,23 +1358,20 @@ apply/seteqP; split; last first. exists `]r, +oo[%classic. rewrite RGenOInfty.measurableE. exact: RGenOInfty.measurable_itv_bnd_infty. - by exists [set +oo]; [constructor|rewrite -punct_eitv_bnd_pinfty]. + by exists [set +oo]; [constructor|rewrite -punct_eitv_bndy]. move=> A [B mB [C mC]] <-; apply: measurableU; last first. - case: mC; [by []|exact: measurable_set1_ninfty - |exact: measurable_set1_pinfty|]. - - by apply: measurableU; [exact: measurable_set1_ninfty| - exact: measurable_set1_pinfty]. + case: mC; [by []|exact: measurable_set1Ny|exact: measurable_set1y|]. + - by apply: measurableU; [exact: measurable_set1Ny|exact: measurable_set1y]. rewrite RGenOInfty.measurableE in mB. have smB := smallest_sub _ _ mB. (* BUG: elim/smB : _. fails !! *) apply: (smB (G.-sigma.-measurable \o (image^~ EFin))); last first. move=> _ [r ->]/=; rewrite EFin_itv_bnd_infty; apply: measurableD. by apply: sub_sigma_algebra => /=; exists r. - exact: measurable_set1_pinfty. + exact: measurable_set1y. split=> /= [|D mD|F mF]; first by rewrite image_set0. - rewrite setTD EFin_setC; apply: measurableD; first exact: measurableC. - by apply: measurableU; [exact: measurable_set1_ninfty| - exact: measurable_set1_pinfty]. + by apply: measurableU; [exact: measurable_set1Ny| exact: measurable_set1y]. - by rewrite EFin_bigcup; apply: bigcup_measurable => i _ ; exact: mF. Qed. @@ -1385,15 +1386,15 @@ Local Open Scope ereal_scope. Definition G := [set A : set \bar R | exists r, A = `[r%:E, +oo[%classic]. -Lemma measurable_set1_ninfty : G.-sigma.-measurable [set -oo]. +Lemma measurable_set1Ny : G.-sigma.-measurable [set -oo]. Proof. -rewrite eset1_ninfty; apply: bigcapT_measurable=> i; rewrite -setCitvr. +rewrite eset1Ny; apply: bigcapT_measurable=> i; rewrite -setCitvr. by apply: measurableC; apply: sub_sigma_algebra; exists (- i%:R)%R. Qed. -Lemma measurable_set1_pinfty : G.-sigma.-measurable [set +oo]. +Lemma measurable_set1y : G.-sigma.-measurable [set +oo]. Proof. -rewrite eset1_pinfty; 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. by apply: sub_sigma_algebra; exists (i%:R + j.+1%:R^-1)%R. @@ -1409,23 +1410,20 @@ apply/seteqP; split; last first. move=> _ [r ->]/=; exists `[r, +oo[%classic. rewrite RGenOInfty.measurableE. exact: RGenOInfty.measurable_itv_bnd_infty. - by exists [set +oo]; [constructor | rewrite -punct_eitv_bnd_pinfty]. + by exists [set +oo]; [constructor|rewrite -punct_eitv_bndy]. move=> _ [A' mA' [C mC]] <-; apply: measurableU; last first. - case: mC; [by []|exact: measurable_set1_ninfty| - exact: measurable_set1_pinfty|]. - by apply: measurableU; [exact: measurable_set1_ninfty| - exact: measurable_set1_pinfty]. + case: mC; [by []|exact: measurable_set1Ny| exact: measurable_set1y|]. + by apply: measurableU; [exact: measurable_set1Ny|exact: measurable_set1y]. rewrite RGenCInfty.measurableE in mA'. have smA' := smallest_sub _ _ mA'. (* BUG: elim/smA' : _. fails !! *) apply: (smA' (G.-sigma.-measurable \o (image^~ EFin))); last first. move=> _ [r ->]/=; rewrite EFin_itv_bnd_infty; apply: measurableD. by apply: sub_sigma_algebra => /=; exists r. - exact: measurable_set1_pinfty. + exact: measurable_set1y. split=> /= [|D mD|F mF]; first by rewrite image_set0. - rewrite setTD EFin_setC; apply: measurableD; first exact: measurableC. - by apply: measurableU; [exact: measurable_set1_ninfty| - exact: measurable_set1_pinfty]. + by apply: measurableU; [exact: measurable_set1Ny|exact: measurable_set1y]. - by rewrite EFin_bigcup; apply: bigcup_measurable => i _; exact: mF. Qed. @@ -1716,7 +1714,7 @@ Lemma measurable_fun_abse (D : set (\bar R)) : measurable_fun D abse. Proof. move=> mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //. move=> /= _ [_ [x ->] <-]. -rewrite [X in _ @^-1` X](punct_eitv_bnd_pinfty _ x) preimage_setU setIUr. +rewrite [X in _ @^-1` X](punct_eitv_bndy _ x) preimage_setU setIUr. apply: measurableU; last first. by rewrite preimage_abse_pinfty; apply: measurableI => //; exact: measurableU. apply: measurableI => //; exists (normr @^-1` `]x, +oo[%classic). @@ -1734,7 +1732,7 @@ Lemma emeasurable_fun_minus (D : set (\bar R)) : Proof. move=> mD; apply: (measurability (ErealGenCInfty.measurableE R)) => //. move=> _ [_ [x ->] <-]; rewrite (_ : _ @^-1` _ = `]-oo, (- x)%:E]%classic). - by apply: measurableI => //; exact: emeasurable_itv_ninfty_bnd. + by apply: measurableI => //; exact: emeasurable_itv. by rewrite predeqE => y; rewrite preimage_itv !in_itv/= andbT in_itv lee_oppr. Qed. @@ -1786,7 +1784,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_bnd_pinfty. +by apply: bigcap_measurable => ? ?; exact/mf/emeasurable_itv. Qed. Lemma measurable_fun_esups D (f : (T -> \bar R)^nat) : @@ -1795,7 +1793,7 @@ Lemma measurable_fun_esups D (f : (T -> \bar R)^nat) : Proof. move=> mf n mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //. move=> _ [_ [x ->] <-];rewrite esups_preimage setI_bigcupr. -by apply: bigcup_measurable => ? ?; exact/mf/emeasurable_itv_bnd_pinfty. +by apply: bigcup_measurable => ? ?; exact/mf/emeasurable_itv. Qed. Lemma emeasurable_fun_max D (f g : T -> \bar R) : @@ -1810,8 +1808,7 @@ move=> _ [_ [x ->] <-]; rewrite [X in measurable X](_ : _ = tauto. by move=> [|]; rewrite !/= /= !in_itv/= !andbT le_maxr; move=> [Dx ->]//; rewrite orbT. -by apply: measurableU; [exact/mf/emeasurable_itv_bnd_pinfty| - exact/mg/emeasurable_itv_bnd_pinfty]. +by apply: measurableU; [exact/mf/emeasurable_itv| exact/mg/emeasurable_itv]. Qed. Lemma emeasurable_funN D (f : T -> \bar R) :