From b2149ba512bc7e03ecc3f3ba7cc1f609d5e9966c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 29 Aug 2024 09:33:55 +0900 Subject: [PATCH 1/3] lemmas about measurable from PR prob_lang Co-authored-by: @AyumuSaito --- CHANGELOG_UNRELEASED.md | 12 ++ theories/lebesgue_measure.v | 212 ++++++++++++++++++++++++++++++++++++ theories/measure.v | 34 ++++-- 3 files changed, 250 insertions(+), 8 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f27496e85..d50eb0350 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -52,6 +52,18 @@ - in `topology.v`: + Structures `PointedFiltered`, `PointedNbhs`, `PointedUniform`, `PseudoPointedMetric` +- in `measure.v`: + + lemma `measurable_neg`, `measurable_or` + +- in `lebesgue_measure.v`: + + lemmas `measurable_fun_eqr`, `measurable_fun_dirac`, `measurable_fun_addn`, + `measurable_fun_maxn`, `measurable_fun_subn`, `measurable_fun_ltn`, + `measurable_fun_leq`, `measurable_fun_eqn` + + module `NGenCInfty` + * definition `G` + * lemmas `measurable_itv_bounded`, `measurableE` + +### Changed ### Changed - in `topology.v`: diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index eafcde9f9..adde7caf0 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -987,6 +987,15 @@ under eq_fun do rewrite -subr_ge0. by rewrite preimage_true -preimage_itv_c_infty; exact: measurable_funB. Qed. +Lemma measurable_fun_eqr D f g : measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x == g x). +Proof. +move=> mf mg. +rewrite (_ : (fun x => f x == g x) = (fun x => (f x <= g x) && (g x <= f x))). + by apply: measurable_and; exact: measurable_fun_ler. +by under eq_fun do rewrite eq_le. +Qed. + Lemma measurable_maxr D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \max g). Proof. @@ -1054,6 +1063,27 @@ apply: (@measurable_fun_limn_sup _ h) => // t Dt. - by apply/bounded_fun_has_lbound/cvg_seq_bounded/cvg_ex; eexists; exact: f_f. Qed. +Lemma measurable_fun_dirac (U : set R) : measurable U -> + measurable_fun [set: _] (fun x : R => \d_x U : \bar R). +Proof. +move=> mU _ /= Y mY; rewrite setTI; + have [Y0|Y0] := pselect (Y 0%E); have [Y1|Y1] := pselect (Y 1%E). +- rewrite [X in measurable X](_ : _ = setT)//. + apply/seteqP; split => //= r _ /=. + by rewrite diracE; case: (_ \in _). +- rewrite [X in measurable X](_ : _ = ~` U)//; first exact: measurableC. + apply/seteqP; split => [//= r /= + Ur|r Ur]; rewrite /= diracE. + by rewrite mem_set. + by rewrite memNset. +- rewrite [X in measurable X](_ : _ = U)//. + apply/seteqP; split => [//= r /=|r Ur]; rewrite /= diracE. + by have [//|Ur] := pselect (U r); rewrite memNset. + by rewrite mem_set. +- rewrite [X in measurable X](_ : _ = set0)//. + apply/seteqP; split => //= r /=. + by rewrite diracE; case: (_ \in _). +Qed. + End measurable_fun_realType. #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed `measurable_fun_limn_sup`")] Notation measurable_fun_lim_sup := measurable_fun_limn_sup (only parsing). @@ -1118,6 +1148,188 @@ Notation measurable_fun_max := measurable_maxr (only parsing). #[deprecated(since="mathcomp-analysis 1.4.0", note="use `measurable_funX` instead")] Notation measurable_fun_pow := measurable_funX (only parsing). +Module NGenCInfty. +Section ngencinfty. +Implicit Types x y z : nat. + +Definition G : set (set nat) := [set A | exists x, A = `[x, +oo[%classic]. + +Lemma measurable_itv_bnd_infty b x : + G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. +Proof. +case: b; first by apply: sub_sigma_algebra; exists x; rewrite set_itv_c_infty. +rewrite [X in measurable X](_ : _ = + \bigcup_(k in [set k | k >= x]%N) `[k.+1, +oo[%classic); last first. + apply/seteqP; split => [z /=|/= z [t/= xt]]. + rewrite in_itv/= andbT => xz; exists z.-1 => /=. + by rewrite -ltnS//=; case: z xz. + by case: z xz => //= z xz; rewrite in_itv/= lexx andbT. + by rewrite !in_itv/= !andbT; apply: lt_le_trans; rewrite ltEnat/= ltnS. +rewrite bigcup_mkcond; apply: bigcupT_measurable => k. +by case: ifPn => //= _; apply: sub_sigma_algebra; eexists; reflexivity. +Qed. + +Lemma measurable_itv_bounded a b y : a != +oo%O -> + G.-sigma.-measurable [set` Interval a (BSide b y)]. +Proof. +case: a => [a r _|[_|//]]. + by rewrite set_itv_splitD; apply: measurableD; apply: measurable_itv_bnd_infty. +by rewrite -setCitvr; apply: measurableC; apply: measurable_itv_bnd_infty. +Qed. + +Lemma measurableE : @measurable _ nat = G.-sigma.-measurable. +Proof. +rewrite eqEsubset; split => [A mA|A]; last exact: smallest_sub. +rewrite (_ : A = \bigcup_(i in A) `[i, i.+1[%classic). + by apply: bigcup_measurable => k Ak; exact: measurable_itv_bounded. +apply/seteqP; split => [x Ax|x [k Ak]]. + by exists x => //=; rewrite in_itv/= lexx/= ltEnat /= ltnS. +by rewrite /= in_itv/= leEnat ltEnat /= ltnS -eqn_leq => /eqP <-. +Qed. + +End ngencinfty. +End NGenCInfty. + +Section measurable_fun_nat. +Context d (T : measurableType d). +Implicit Types (D : set T) (f g : T -> nat). + +Lemma measurable_fun_addn D f g : measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x + g x)%N. +Proof. +move=> mf mg mD; apply: (measurability NGenCInfty.measurableE) => //. +move=> /= _ [_ [a ->] <-]; rewrite preimage_itv_c_infty. +rewrite [X in measurable X](_ : _ = \bigcup_q + ((D `&` [set x | q <= f x]%O) `&` (D `&` [set x | (a - q)%N <= g x]%O))). + apply: bigcupT_measurable => q; apply: measurableI. + - by rewrite -preimage_itv_c_infty; exact: mf. + - by rewrite -preimage_itv_c_infty; exact: mg. +rewrite predeqE => x; split => [|[r ?] []/= [Dx rfx]] /= => [[Dx]|[?]]. +- move=> afxgx; exists (a - g x)%N => //=; split; split => //. + by rewrite leEnat leq_subLR// addnC -leEnat. + have [gxa|gxa] := leqP (g x) a; first by rewrite subKn. + by move/ltnW : (gxa); rewrite -subn_eq0 => /eqP ->; rewrite subn0 ltW. +- rewrite leEnat leq_subLR => arg; split => //. + by rewrite (leq_trans arg)// leq_add2r. +Qed. + +Lemma measurable_fun_maxn D f g : measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => maxn (f x) (g x)). +Proof. +move=> mf mg mD; apply: (measurability NGenCInfty.measurableE) => //. +move=> /= _ [_ [a ->] <-]; rewrite [X in measurable X](_ : _ = + ((D `&` [set x | a <= f x]%O) `|` (D `&` [set x | a <= g x]%O))). + apply: measurableU. + - by rewrite -preimage_itv_c_infty; exact: mf. + - by rewrite -preimage_itv_c_infty; exact: mg. +rewrite predeqE => x; split => [[Dx /=]|]. +- by rewrite in_itv/= andbT; have [fg agx|gf afx] := leqP (f x) (g x); tauto. +- move=> [[Dx /= afx]|[Dx /= agx]]. + + rewrite in_itv/= andbT; split => //. + by rewrite (le_trans afx)// leEnat leq_maxl. + + rewrite in_itv/= andbT; split => //. + by rewrite (le_trans agx)// leEnat leq_maxr. +Qed. + +Let measurable_fun_subn' D f g : (forall t, g t <= f t)%N -> + measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x - g x)%N. +Proof. +move=> gf mf mg mD; apply: (measurability NGenCInfty.measurableE) => //. +move=> /= _ [_ [a ->] <-]; rewrite preimage_itv_c_infty. +rewrite [X in measurable X](_ : _ = \bigcup_q + ((D `&` [set x | maxn a q <= f x]%O) `&` + (D `&` [set x | g x <= (q - a)%N]%O))). + apply: bigcupT_measurable => q; apply: measurableI. + - by rewrite -preimage_itv_c_infty; exact: mf. + - by rewrite -preimage_itv_infty_c; exact: mg. +rewrite predeqE => x; split => [|[r ?] []/= [Dx rfx]] /= => [[Dx]|[_]]. +- move=> afxgx; exists (g x + a)%N => //; split; split => //=. + rewrite leEnat; have /maxn_idPr -> := leq_addl (g x) a. + by rewrite -leq_subRL. + by rewrite leEnat addnK. +- rewrite leEnat => gxra; split => //; rewrite -(leq_add2r (g x)) subnK//. + have [afx|afx] := leqP a (f x). + rewrite -(@leq_sub2rE a)// addnC addnK (leq_trans gxra)// leq_sub2r//. + by rewrite (leq_trans _ rfx)//; exact: leq_maxr. + move: gxra; rewrite -(leq_add2l a) subnKC//; last first. + by have := leq_ltn_trans rfx afx; rewrite ltnNge leq_maxl. + by move=> /leq_trans; apply; rewrite (leq_trans _ rfx)//; exact: leq_maxr. +Qed. + +Lemma measurable_fun_subn D f g : measurable_fun D f -> + measurable_fun D g -> measurable_fun D (fun x => f x - g x)%N. +Proof. +move=> mf mg. +rewrite [X in measurable_fun _ X](_ : _ = fun x => (maxn (f x) (g x) - g x)%N). + apply: measurable_fun_subn' => //; last exact: measurable_fun_maxn. + by move=> t; rewrite leq_maxr. +apply/funext => x; have [//|gf] := leqP (g x) (f x). +by apply/eqP; rewrite subnn subn_eq0// ltnW. +Qed. + +Lemma measurable_fun_ltn D f g : measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x < g x)%N. +Proof. +move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->. +- have -> : (fun x => f x < g x)%O = (fun x => 0%N < (g x - f x)%N)%O. + apply/funext => n; apply/idP/idP. + by rewrite !ltEnat /ltn/= => fg; rewrite subn_gt0. + by rewrite !ltEnat /ltn/= => fg; rewrite -subn_gt0. + by rewrite preimage_true -preimage_itv_o_infty; exact: measurable_fun_subn. +- under eq_fun do rewrite ltnNge. + rewrite preimage_false set_predC setCK. + rewrite [X in _ `&` X](_ : _ = \bigcup_(i in range f) + ([set y | g y <= i]%O `&` [set t | i <= f t]%O)). + rewrite setI_bigcupr; apply: bigcup_measurable => k fk. + rewrite setIIr; apply: measurableI => //. + + by rewrite -preimage_itv_infty_c; exact: mg. + + by rewrite -preimage_itv_c_infty; exact: mf. + apply/funext => n/=. + suff : (g n <= f n)%N <-> + (\bigcup_(i in range f) ([set y | g y <= i]%O `&` [set t | i <= f t]%O)) n. + by move/propext. + split=> [gfn|[k [t _ <- []]] /=]. + by exists (f n) => //; split => /=. + by move=> /leq_trans; apply. +- by rewrite preimage_set0 setI0. +- by rewrite preimage_setT setIT. +Qed. + +Lemma measurable_fun_leq D f g : measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x <= g x)%N. +Proof. +move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->. +- rewrite preimage_true [X in _ `&` X](_ : _ = + \bigcup_(i in range g) ([set y | f y <= i]%O `&` [set t | i <= g t]%O)). + rewrite setI_bigcupr; apply: bigcup_measurable => k fk. + rewrite setIIr; apply: measurableI => //. + + by rewrite -preimage_itv_infty_c; exact: mf. + + by rewrite -preimage_itv_c_infty; exact: mg. + apply/funext => n/=. + suff : (f n <= g n)%N <-> + (\bigcup_(i in range g) ([set y | f y <= i]%O `&` [set t | i <= g t]%O)) n. + by move/propext. + split=> [gfn|[k [t _ <- []]] /=]. + by exists (g n) => //; split => /=. + by move=> /leq_trans; apply. +- under eq_fun do rewrite leqNgt. + by rewrite preimage_false set_predC setCK; exact: measurable_fun_ltn. +- by rewrite preimage_set0 setI0. +- by rewrite preimage_setT setIT. +Qed. + +Lemma measurable_fun_eqn D f g : measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x == g x). +Proof. +move=> mf mg. +rewrite (_ : (fun x => f x == g x) = (fun x => (f x <= g x) && (g x <= f x))%N). + by apply: measurable_and; exact: measurable_fun_leq. +by under eq_fun do rewrite eq_le. +Qed. + +End measurable_fun_nat. + Section standard_emeasurable_fun. Variable R : realType. diff --git a/theories/measure.v b/theories/measure.v index 36f56b345..9f4b3f4cc 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1643,8 +1643,9 @@ by move=> mx my; apply: measurable_fun_if => //; Qed. Section measurable_fun_bool. +Implicit Types f g : T1 -> bool. -Let measurable_fun_TF D (f : T1 -> bool) : +Let measurable_fun_TF D f : measurable (D `&` f @^-1` [set true]) -> measurable (D `&` f @^-1` [set false]) -> measurable_fun D f. @@ -1658,7 +1659,7 @@ move: mY; have [-> _|-> _|-> _ |-> _] := subset_set2 YT. - by rewrite -setT_bool preimage_setT setIT. Qed. -Lemma measurable_fun_bool D (f : T1 -> bool) b : +Lemma measurable_fun_bool D f b : measurable (D `&` f @^-1` [set b]) -> measurable_fun D f. Proof. move=> mb mD; have mDb : measurable (D `&` f @^-1` [set ~~ b]). @@ -1667,12 +1668,9 @@ move=> mb mD; have mDb : measurable (D `&` f @^-1` [set ~~ b]). by rewrite -preimage_setC; exact: measurableID. by case: b => /= in mb mDb *; exact: measurable_fun_TF. Qed. +#[global] Arguments measurable_fun_bool {D f} _. -End measurable_fun_bool. -Arguments measurable_fun_bool {D f} _. - -Lemma measurable_and D (f : T1 -> bool) (g : T1 -> bool) : - measurable_fun D f -> measurable_fun D g -> +Lemma measurable_and D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (fun x => f x && g x). Proof. move=> mf mg mD; apply: (measurable_fun_bool true) => //. @@ -1682,6 +1680,26 @@ rewrite [X in measurable X](_ : _ = D `&` f @^-1` [set true] `&` by apply: measurableI; [exact: mf|exact: mg]. Qed. +Lemma measurable_neg D f : + measurable_fun D f -> measurable_fun D (fun x => ~~ f x). +Proof. +move=> mf mD; apply: (measurable_fun_bool true) => //. +rewrite [X in measurable X](_ : _ = (D `&` f @^-1` [set false])). + exact: mf. +by apply/seteqP; split => [x [Dx/= /negbTE]|x [Dx/= ->]]. +Qed. + +Lemma measurable_or D f g : measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x || g x). +Proof. +move=> mf mg. +rewrite [X in measurable_fun _ X](_ : _ = (fun x => ~~ (~~ f x && ~~ g x))). + by apply: measurable_neg; apply: measurable_and; exact: measurable_neg. +by apply/funext=> x; rewrite -negb_or negbK. +Qed. + +End measurable_fun_bool. + End measurable_fun_measurableType. #[global] Hint Extern 0 (measurable_fun _ (fun=> _)) => solve [apply: measurable_cst] : core. @@ -5218,7 +5236,7 @@ Context d (T : measurableType d) (R : realType). Implicit Types m : {measure set T -> \bar R}. Lemma measure_dominates_ae_eq m1 m2 f g E : measurable E -> - m2 `<< m1 -> ae_eq m1 E f g -> ae_eq m2 E f g. + m2 `<< m1 -> ae_eq m1 E f g -> ae_eq m2 E f g. Proof. by move=> mE m21 [A [mA A0 ?]]; exists A; split => //; exact: m21. Qed. End absolute_continuity_lemmas. From 49f72a9560d9906fae375b5d4c0be92dc6030ed7 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 29 Aug 2024 10:23:39 +0900 Subject: [PATCH 2/3] doc --- theories/lebesgue_measure.v | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index adde7caf0..fee500603 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -32,13 +32,17 @@ Require Export lebesgue_stieltjes_measure. (* ``` *) (* *) (* The modules RGenOInfty, RGenInftyO, RGenCInfty, RGenOpens provide proofs *) -(* of equivalence between the sigma-algebra generated by list of intervals *) -(* and the sigma-algebras generated by open rays, closed rays, and open *) -(* intervals. *) +(* of equivalence between the sigma-algebra generated by open-closed *) +(* intervals and the sigma-algebras generated by open rays, closed rays, and *) +(* open intervals. *) +(* *) +(* The module NGenCInfty provides a proof of equivalence between the *) +(* sigma-algebra for natural numbers and the sigma-algebra generated by *) +(* closed rays. *) (* *) (* The modules ErealGenOInfty, ErealGenCInfty, ErealGenInftyO provide proofs *) -(* of equivalence between emeasurable and the sigma-algebras generated open *) -(* rays and closed rays. *) +(* of equivalence between emeasurable and the sigma-algebras generated by *) +(* open rays and closed rays. *) (* *) (* ``` *) (* lebesgue_measure == the Lebesgue measure *) From cf8202d6208b664a6244a5c981b9a52851c10d93 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 13 Sep 2024 14:53:20 +0900 Subject: [PATCH 3/3] add meas_fun_indic, gen meas_fun_dirac --- CHANGELOG_UNRELEASED.md | 4 ++-- theories/lebesgue_measure.v | 36 ++++++++++++++++++++---------------- 2 files changed, 22 insertions(+), 18 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d50eb0350..4fb4d9236 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -56,8 +56,8 @@ + lemma `measurable_neg`, `measurable_or` - in `lebesgue_measure.v`: - + lemmas `measurable_fun_eqr`, `measurable_fun_dirac`, `measurable_fun_addn`, - `measurable_fun_maxn`, `measurable_fun_subn`, `measurable_fun_ltn`, + + lemmas `measurable_fun_eqr`, `measurable_fun_indic`, `measurable_fun_dirac`, + `measurable_fun_addn`, `measurable_fun_maxn`, `measurable_fun_subn`, `measurable_fun_ltn`, `measurable_fun_leq`, `measurable_fun_eqn` + module `NGenCInfty` * definition `G` diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index fee500603..4208007bb 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1067,25 +1067,24 @@ apply: (@measurable_fun_limn_sup _ h) => // t Dt. - by apply/bounded_fun_has_lbound/cvg_seq_bounded/cvg_ex; eexists; exact: f_f. Qed. -Lemma measurable_fun_dirac (U : set R) : measurable U -> - measurable_fun [set: _] (fun x : R => \d_x U : \bar R). -Proof. -move=> mU _ /= Y mY; rewrite setTI; - have [Y0|Y0] := pselect (Y 0%E); have [Y1|Y1] := pselect (Y 1%E). -- rewrite [X in measurable X](_ : _ = setT)//. - apply/seteqP; split => //= r _ /=. - by rewrite diracE; case: (_ \in _). -- rewrite [X in measurable X](_ : _ = ~` U)//; first exact: measurableC. - apply/seteqP; split => [//= r /= + Ur|r Ur]; rewrite /= diracE. +Lemma measurable_fun_indic D (U : set T) : measurable U -> + measurable_fun D (\1_U : _ -> R). +Proof. +move=> mU mD /= Y mY. +have [Y0|Y0] := pselect (Y 0%R); have [Y1|Y1] := pselect (Y 1%R). +- rewrite [X in measurable X](_ : _ = D)//. + by apply/seteqP; split => //= r Dr /=; rewrite indicE; case: (_ \in _). +- rewrite [X in measurable (_ `&` X)](_ : _ = ~` U)//. + by apply: measurableI => //; exact: measurableC. + apply/seteqP; split => [//= r /= + Ur|r Ur]; rewrite /= indicE. by rewrite mem_set. by rewrite memNset. -- rewrite [X in measurable X](_ : _ = U)//. - apply/seteqP; split => [//= r /=|r Ur]; rewrite /= diracE. +- rewrite [X in measurable (_ `&` X)](_ : _ = U); first exact: measurableI. + apply/seteqP; split => [//= r /=|r Ur]; rewrite /= indicE. by have [//|Ur] := pselect (U r); rewrite memNset. by rewrite mem_set. - rewrite [X in measurable X](_ : _ = set0)//. - apply/seteqP; split => //= r /=. - by rewrite diracE; case: (_ \in _). + by apply/seteqP; split => // r /= -[_]; rewrite indicE; case: (_ \in _). Qed. End measurable_fun_realType. @@ -1398,8 +1397,13 @@ congr (_ `&` _);rewrite eqEsubset; split=> [|? []/= _ /[swap] -[->//]]. by move=> ? ?; exact: preimage_image. Qed. -Lemma measurable_er_map d (T : measurableType d) (R : realType) (f : R -> R) - : measurable_fun setT f -> measurable_fun [set: \bar R] (er_map f). +Lemma measurable_fun_dirac + d {T : measurableType d} {R : realType} D (U : set T) : + measurable U -> measurable_fun D (fun x => \d_x U : \bar R). +Proof. by move=> /measurable_fun_indic/EFin_measurable_fun. Qed. + +Lemma measurable_er_map d (T : measurableType d) (R : realType) (f : R -> R) : + measurable_fun setT f -> measurable_fun [set: \bar R] (er_map f). Proof. move=> mf;rewrite (_ : er_map _ = fun x => if x \is a fin_num then (f (fine x))%:E else x); last first.