fixes #1080 (change sigma_finiteP)

CHANGELOG_UNRELEASED.md

@@ -10,6 +10,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`:

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.

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,58 +2058,56 @@ Qed.
 End lebesgue_regularity.
 
 Section egorov.
-
 Context d {R : realType} {T : measurableType d}.
 Context (mu : {measure set T -> \bar R}).
 
 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

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.