diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e4110708d..275d41394 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -13,6 +13,9 @@ + definition `mset`, `pset`, `pprobability` + lemmas `lt0_mset`, `gt1_mset` +- in `measure.v`: + + lemma `sigma_finiteP` generalized to an equivalence and changed to use `[/\ ..., .. & ....]` + ### Renamed - in `constructive_ereal.v`: diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 911e3d483..5cfbb9a79 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -4629,19 +4629,19 @@ Let B := [set A | measurable A /\ measurable_fun setT (phi A)]. Lemma measurable_fun_xsection A : measurable A -> measurable_fun setT (phi A). Proof. move: A; suff : measurable `<=` B by move=> + A => /[apply] -[]. -have /sigma_finiteP [F F_T [F_nd F_oo]] := sigma_finiteT m2 => X mX. +have /sigma_finiteP [F [F_T F_nd F_oo]] := sigma_finiteT m2 => X mX. have -> : X = \bigcup_n (X `&` (setT `*` F n)). by rewrite -setI_bigcupr -setM_bigcupr -F_T setMTT setIT. apply: xsection_ndseq_closed. move=> m n mn; apply/subsetPset; apply: setIS; apply: setSM => //. exact/subsetPset/F_nd. move=> n; rewrite -/B; have [? ?] := F_oo n. -pose m2Fn := [the measure _ _ of mrestr m2 (F_oo n).1]. +pose m2Fn := mrestr m2 (F_oo n).1. have m2Fn_bounded : exists M, forall X, measurable X -> (m2Fn X < M%:E)%E. exists (fine (m2Fn (F n)) + 1) => Y mY. rewrite [in ltRHS]EFinD lte_spadder// fineK; last first. - by rewrite ge0_fin_numE ?measure_ge0//= /mrestr/= setIid. - by rewrite /= /mrestr/= setIid le_measure// inE//; exact: measurableI. + by rewrite ge0_fin_numE ?measure_ge0//= /m2Fn /mrestr setIid. + by rewrite /m2Fn /mrestr/= setIid le_measure// inE//; exact: measurableI. pose phi' A := m2Fn \o xsection A. pose B' := [set A | measurable A /\ measurable_fun setT (phi' A)]. have subset_B' : measurable `<=` B' by exact: measurable_prod_subset_xsection. @@ -4664,14 +4664,14 @@ Let B := [set A | measurable A /\ measurable_fun setT (phi A)]. Lemma measurable_fun_ysection A : measurable A -> measurable_fun setT (phi A). Proof. move: A; suff : measurable `<=` B by move=> + A => /[apply] -[]. -have /sigma_finiteP[F F_T [F_nd F_oo]] := sigma_finiteT m1 => X mX. +have /sigma_finiteP[F [F_T F_nd F_oo]] := sigma_finiteT m1 => X mX. have -> : X = \bigcup_n (X `&` (F n `*` setT)). by rewrite -setI_bigcupr -setM_bigcupl -F_T setMTT setIT. apply: ysection_ndseq_closed. move=> m n mn; apply/subsetPset; apply: setIS; apply: setSM => //. exact/subsetPset/F_nd. move=> n; have [? ?] := F_oo n; rewrite -/B. -pose m1Fn := [the measure _ _ of mrestr m1 (F_oo n).1]. +pose m1Fn := mrestr m1 (F_oo n).1. have m1Fn_bounded : exists M, forall X, measurable X -> (m1Fn X < M%:E)%E. exists (fine (m1Fn (F n)) + 1) => Y mY. rewrite [in ltRHS]EFinD lte_spadder// fineK; last first. @@ -4761,8 +4761,8 @@ Variable m2 : {sigma_finite_measure set T2 -> \bar R}. Let product_measure_sigma_finite : sigma_finite setT (m1 \x m2). Proof. -have /sigma_finiteP[F TF [ndF Foo]] := sigma_finiteT m1. -have /sigma_finiteP[G TG [ndG Goo]] := sigma_finiteT m2. +have /sigma_finiteP[F [TF ndF Foo]] := sigma_finiteT m1. +have /sigma_finiteP[G [TG ndG Goo]] := sigma_finiteT m2. exists (fun n => F n `*` G n). rewrite -setMTT TF TG predeqE => -[x y]; split. move=> [/= [n _ Fnx] [k _ Gky]]; exists (maxn n k) => //; split. @@ -4784,8 +4784,8 @@ Lemma product_measure_unique forall X : set (T1 * T2), measurable X -> (m1 \x m2) X = m' X. Proof. move=> m'E. -have /sigma_finiteP[F TF [ndF Foo]] := sigma_finiteT m1. -have /sigma_finiteP[G TG [ndG Goo]] := sigma_finiteT m2. +have /sigma_finiteP[F [TF ndF Foo]] := sigma_finiteT m1. +have /sigma_finiteP[G [TG ndG Goo]] := sigma_finiteT m2. have UFGT : \bigcup_k (F k `*` G k) = setT. rewrite -setMTT TF TG predeqE => -[x y]; split. by move=> [n _ []/= ? ?]; split; exists n. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 0524dd5f7..c47842485 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -2029,8 +2029,8 @@ Lemma lebesgue_regularity_inner_sup (D : set R) : measurable D -> Proof. move=> mD; have [?|] := ltP (mu D) +oo. exact: lebesgue_regularity_innerE_bounded. -have /sigma_finiteP [F RFU [Fsub ffin]] := - sigma_finiteT (lebesgue_stieltjes_measure [the cumulative _ of @idfun R]). +have /sigma_finiteP [F [RFU Fsub ffin]] := + sigma_finiteT (lebesgue_stieltjes_measure (@idfun R)). rewrite leye_eq => /eqP /[dup] + ->. have {1}-> : D = \bigcup_n (F n `&` D) by rewrite -setI_bigcupl -RFU setTI. move=> FDp; apply/esym/eq_infty => M. @@ -2058,7 +2058,6 @@ Qed. End lebesgue_regularity. Section egorov. - Context d {R : realType} {T : measurableType d}. Context (mu : {measure set T -> \bar R}). @@ -2066,50 +2065,49 @@ Local Open Scope ereal_scope. (*TODO : this generalizes to any metric space with a borel measure*) Lemma pointwise_almost_uniform - (f_ : (T -> R)^nat) (g : T -> R) (A : set T) (eps : R): + (f_ : (T -> R)^nat) (g : T -> R) (A : set T) (eps : R) : (forall n, measurable_fun A (f_ n)) -> measurable_fun A g -> - measurable A -> mu A < +oo -> (forall x, A x -> f_ ^~ x @\oo --> g x) -> + measurable A -> mu A < +oo -> (forall x, A x -> f_ ^~ x @ \oo --> g x) -> (0 < eps)%R -> exists B, [/\ measurable B, mu B < eps%:E & - {uniform A `\` B, f_ @\oo --> g}]. + {uniform A `\` B, f_ @ \oo --> g}]. Proof. move=> mf mg mA finA fptwsg epspos; pose h q (z : T) : R := `|f_ q z - g z|%R. have mfunh q : measurable_fun A (h q). by apply: measurableT_comp; [exact: measurable_normr |exact: measurable_funB]. -pose E k n := \bigcup_(i in [set j : nat | (n <= j)%N ]) - (A `&` [set x | (h i x >= k.+1%:R^-1)%R]). +pose E k n := \bigcup_(i in [set j | n <= j]%N) + (A `&` [set x | h i x >= k.+1%:R^-1]%R). have Einc k : nonincreasing_seq (E k). move=> n m nm; apply/asboolP => z [i] /= /(leq_trans _) mi [? ?]. by exists i => //; apply: mi. have mE k n : measurable (E k n). apply: bigcup_measurable => q /= ?. - have -> : [set x | h q x >= k.+1%:R^-1]%R = (h q)@^-1` (`[k.+1%:R^-1, +oo[). - by rewrite eqEsubset; split => z; rewrite /= in_itv /= Bool.andb_true_r. + have -> : [set x | h q x >= k.+1%:R^-1]%R = h q @^-1` `[k.+1%:R^-1, +oo[. + by rewrite eqEsubset; split => z; rewrite /= in_itv /= andbT. exact: mfunh. have nEcvg x k : exists n, A x -> (~` (E k n)) x. - case : (pselect (A x)); last by move => ?; exists point. - move=> Ax; have [] := fptwsg _ Ax (interior (ball (g x) (k.+1%:R^-1))). + have [Ax|?] := pselect (A x); last by exists point. + have [] := fptwsg _ Ax (interior (ball (g x) k.+1%:R^-1)). by apply: open_nbhs_nbhs; split; [exact: open_interior|exact: nbhsx_ballx]. move=> N _ Nk; exists N.+1 => _; rewrite /E setC_bigcup => i /= /ltnW Ni. apply/not_andP; right; apply/negP; rewrite /h -real_ltNge // distrC. by case: (Nk _ Ni) => _/posnumP[?]; apply; exact: ball_norm_center. -have Ek0 k : (\bigcap_n (E k n)) = set0. - rewrite eqEsubset; split => // z /=; suff : (~` \bigcap_n E k n) z by done. - rewrite setC_bigcap; case : (pselect (A z)) => [Az | nAz]. +have Ek0 k : \bigcap_n (E k n) = set0. + rewrite eqEsubset; split => // z /=; suff : (~` \bigcap_n E k n) z by []. + rewrite setC_bigcap; have [Az | nAz] := pselect (A z). by have [N /(_ Az) ?] := nEcvg z k; exists N. by exists O; rewrite // /E setC_bigcup => n ? []. -have badn' : forall k, exists n, mu (E k n) < ((eps/2) / (2 ^ k.+1)%:R)%:E. - move=> k; pose ek :R := eps/2 / (2 ^ k.+1)%:R. - have : mu \o E k @\oo --> mu set0. +have badn' k : exists n, mu (E k n) < ((eps/2) / (2 ^ k.+1)%:R)%:E. + pose ek :R := eps/2 / (2 ^ k.+1)%:R. + have : mu \o E k @ \oo --> mu set0. rewrite -(Ek0 k); apply: nonincreasing_cvg_mu => //. - - apply: (le_lt_trans _ finA); apply: le_measure; rewrite ?inE //. - by move=> ? [? _ []]. - - by apply: bigcap_measurable => ?. - rewrite measure0; case/fine_cvg/(_ (interior (ball (0:R) ek))%R). + - by rewrite (le_lt_trans _ finA)// le_measure// ?inE// => ? [? _ []]. + - exact: bigcap_measurable. + rewrite measure0; case/fine_cvg/(_ (interior (ball 0 ek))%R). apply: open_nbhs_nbhs; split; first exact: open_interior. by apply: nbhsx_ballx; rewrite !divr_gt0. move=> N _ /(_ N (leqnn _))/interior_subset muEN; exists N; move: muEN. rewrite /ball /= distrC subr0 ger0_norm // -[x in x < _]fineK ?ge0_fin_numE//. - by apply:(le_lt_trans _ finA); apply: le_measure; rewrite ?inE// => ? [? _ []]. + by rewrite (le_lt_trans _ finA)// le_measure// ?inE// => ? [? _ []]. pose badn k := projT1 (cid (badn' k)); exists (\bigcup_k (E k (badn k))); split. - exact: bigcup_measurable. - apply: (@le_lt_trans _ _ (eps/2)%R%:E); first last. @@ -2124,10 +2122,10 @@ apply/uniform_restrict_cvg => /= U /=; rewrite !uniform_nbhsT. case/nbhs_ex => del /= ballU; apply: filterS; first by move=> ?; exact: ballU. have [N _ /(_ N)/(_ (leqnn _)) Ndel] := near_infty_natSinv_lt del. exists (badn N) => // r badNr x. -rewrite /patch; case xAB: (x \in A `\` _) => //; apply: (lt_trans _ Ndel). -move/set_mem: xAB; rewrite setDE; case => Ax; rewrite setC_bigcup => /(_ N I). -rewrite /E setC_bigcup => /(_ r) /=; rewrite /h => /(_ badNr) /not_andP [] //. -by move/negP; rewrite real_ltNge // distrC. +rewrite /patch; case: ifPn => // /set_mem xAB; apply: (lt_trans _ Ndel). +move: xAB; rewrite setDE => -[Ax]; rewrite setC_bigcup => /(_ N I). +rewrite /E setC_bigcup => /(_ r) /=; rewrite /h => /(_ badNr) /not_andP[]//. +by move/negP; rewrite ltNge // distrC. Qed. Lemma ae_pointwise_almost_uniform diff --git a/theories/measure.v b/theories/measure.v index 173a48072..7d82560d7 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -3243,7 +3243,7 @@ Context d (R : realFieldType) (T : ringOfSetsType d). Variable mu : {content set T -> \bar R}. Theorem Boole_inequality (A : (set T) ^nat) n : - (forall i, `I_n i -> measurable (A i)) -> + (forall i, (i < n)%N -> measurable (A i)) -> mu (\big[setU/set0]_(i < n) A i) <= \sum_(i < n) mu (A i). Proof. move=> Am; rewrite content_sub_additive// -bigcup_mkord. @@ -3257,21 +3257,20 @@ Section sigma_finite_lemma. Context d (T : ringOfSetsType d) (R : realFieldType) (A : set T) (mu : {content set T -> \bar R}). -Lemma sigma_finiteP : sigma_finite A mu -> - exists2 F, A = \bigcup_i F i & - nondecreasing_seq F /\ forall i, measurable (F i) /\ mu (F i) < +oo. -Proof. -move=> [S AS moo]; exists (fun n => \big[setU/set0]_(i < n.+1) S i). - rewrite AS predeqE => t; split => [[i _ Sit]|[i _]]. - by exists i => //; rewrite big_ord_recr /=; right. - by rewrite -bigcup_mkord => -[j /= ji Sjt]; exists j. -split=> [|i]. -- apply/nondecreasing_seqP => i; rewrite [in leRHS]big_ord_recr /=. - by apply/subsetPset; left. -- split; first by apply: bigsetU_measurable => j _; exact: (moo j).1. - rewrite (@le_lt_trans _ _ (\sum_(j < i.+1) mu (S j)))//. - by apply: Boole_inequality => j _; exact: (moo j).1. - by apply/lte_sum_pinfty => j _; exact: (moo j).2. +Lemma sigma_finiteP : sigma_finite A mu <-> + exists F, [/\ A = \bigcup_i F i, + nondecreasing_seq F & forall i, measurable (F i) /\ mu (F i) < +oo]. +Proof. +split=> [[F AUF mF]|[F [? ? ?]]]; last by exists F. +exists (fun n => \big[setU/set0]_(i < n.+1) F i); split. +- rewrite AUF; apply/seteqP; split. + by apply: subset_bigcup => i _; exact: bigsetU_sup. + by apply: bigcup_sub => i _; exact: bigsetU_bigcup. +- by move=> i j ij; exact/subsetPset/subset_bigsetU. +- move=> i; split; first by apply: bigsetU_measurable => j _; exact: (mF j).1. + rewrite (le_lt_trans (Boole_inequality _ _))//. + by move=> j _; exact: (mF _).1. + by apply/lte_sum_pinfty => j _; exact: (mF j).2. Qed. End sigma_finite_lemma.