Sigma algebra lemmas (#2013)

---------

Co-authored-by: adjevahi <arthur.djevahirdjian@ens-lyon.fr>
Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>

Author: 3 people

CHANGELOG_UNRELEASED.md

@@ -18,6 +18,7 @@
 
 - in `measurable_structure.v`:
   + lemmas `g_sigma_algebra_cross`, `g_sigma_algebra_rectangle`
+  + lemma `sigma_algebra_sub`
 
 - in `measurable_function.v`:
   + lemma `preimage_measurability`
@@ -224,6 +225,15 @@
 - in `functions.v`:
   + lemma `preimageD1`
 
+- in `measure_function.v`:
+  + lemmas `cvg_measure_bigcap`, `cvg_measure_bigcup`
+
+- in `classical_sets.v`:
+  + lemma `bigcup_bigsetU`
+
+- in `measurable_structure.v`:
+  + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable`
+
 ### Changed
 
 - in `realsum.v`:
@@ -361,6 +371,7 @@
 
 - in `measurable_structure.v`:
   + `measurable_prod_measurableType` -> `prod_measurable_rectangle`
+  + `sub_sigma_algebra2` -> `sigma_algebra_sub`
 - in `measurable_realfun.v`:
   + `measurable_fun_itv_co` -> `measurable_fun_itvbb_itvco`
   + `measurable_fun_itv_oc` -> `measurable_fun_itvbb_itvoc`

classical/classical_sets.v

@@ -2343,6 +2343,17 @@ rewrite -(big_mkord xpredT F) -bigcup_seq.
 by apply: eq_bigcupl; split=> i; rewrite /= mem_index_iota leq0n.
 Qed.
 
+Lemma bigcup_bigsetU F :
+  \bigcup_k \big[setU/set0]_(i < k.+1) F i =
+  \bigcup_k \big[setU/set0]_(i < k) F i.
+Proof.
+transitivity (\bigcup_(k in S @` setT) \big[setU/set0]_(i < k) F i).
+  by rewrite bigcup_image.
+rewrite [RHS](bigcup_setD1 0%N)// big_ord0 set0U; apply: eq_bigcupl.
+split=> [x [? _ <-//]|x [_ x0]]/=; exists x.-1 => //; rewrite prednK// lt0n.
+exact/eqP.
+Qed.
+
 Lemma bigcup_bigsetU_bigcup F :
   \bigcup_k \big[setU/set0]_(i < k.+1) F i = \bigcup_k F k.
 Proof.

theories/measure_theory/measurable_structure.v

@@ -355,7 +355,13 @@ by apply: (PU) => n; apply: GA.
 Qed.
 Hint Resolve smallest_sigma_algebra : core.
 
-Lemma sub_sigma_algebra2 M : M `<=` G -> <<s D, M >> `<=` <<s D, G >>.
+Lemma sigma_algebra_subl M : M `<=` <<s D, G>> -> <<s D, M >> `<=` <<s D, G >>.
+Proof.
+move=> MsG A + H [sH GH]; apply; split => //; apply: (subset_trans MsG).
+exact: bigcap_inf.
+Qed.
+
+Lemma sigma_algebra_sub M : M `<=` G -> <<s D, M >> `<=` <<s D, G >>.
 Proof. exact: sub_smallest2r. Qed.
 
 Lemma sigma_algebra_id : sigma_algebra D G -> <<s D, G >> = G.
@@ -1157,6 +1163,24 @@ Lemma bigcapT_measurable F :
   (forall k, measurable (F k)) -> measurable (\bigcap_i F i).
 Proof. by move=> PF; apply: bigcap_measurable => //; exists 1. Qed.
 
+Lemma countable_bigcup_measurable {U} {F : U -> set T}
+    {P : set U} : countable P -> (forall i, P i -> measurable (F i)) ->
+  measurable (\bigcup_(i in P) F i).
+Proof.
+move=>/[dup] cP /pfcard_geP =>[[-> _|/surjfunPex [f ->] mF]].
+  by rewrite bigcup0.
+by rewrite bigcup_image; apply: bigcupT_measurable=>// i; exact: mF.
+Qed.
+
+Lemma countable_bigcap_measurable {U} {F : U -> set T} (P : set U) :
+    P !=set0 -> countable P -> (forall k, P k -> measurable (F k)) ->
+  measurable (\bigcap_(i in P) F i).
+Proof.
+move=> [j Pj] /pfcard_geP=>[[P0|/surjfunPex [f ->] mF]].
+  by rewrite P0/= in Pj.
+by rewrite bigcap_image; apply: bigcap_measurable=>// k _; exact: mF.
+Qed.
+
 End sigmaring_lemmas.
 
 (* Adapted from mathlib induction_on_inter *)
@@ -1616,7 +1640,7 @@ move=> sX sY; apply/seteqP; split.
   apply: (@measurableI _ (@g_sigma_algebraType _ (X `x` Y))).
   + by apply: sub_sigma_algebra; left; exists A1 => //; rewrite setTI.
   + by apply: sub_sigma_algebra; right; exists A2 => //; rewrite setTI.
-- apply: sub_sigma_algebra2 => A [|].
+- apply: sigma_algebra_sub => A [|].
   + rewrite /preimage_set_system/= => -[A1 XA1 <-{A}].
     by rewrite -setXT setTI; exact: rectangle_setX.
   + rewrite /preimage_set_system/= => -[A1 XA1 <-{A}].

theories/measure_theory/measure_function.v

@@ -1674,7 +1674,7 @@ Qed.
 Section measure_continuity.
 Local Open Scope ereal_scope.
 
-Lemma nondecreasing_cvg_mu d (T : ringOfSetsType d) (R : realFieldType)
+Lemma nondecreasing_cvg_measure d (T : ringOfSetsType d) (R : realFieldType)
   (mu : {measure set T -> \bar R}) (F : (set T) ^nat) :
   (forall i, measurable (F i)) -> measurable (\bigcup_n F n) ->
   nondecreasing_seq F ->
@@ -1697,7 +1697,7 @@ under eq_fun do rewrite -(big_mkord predT (mu \o seqD F)).
 exact/(nS m.+1)/(leq_trans nm).
 Qed.
 
-Lemma nonincreasing_cvg_mu d (T : algebraOfSetsType d) (R : realFieldType)
+Lemma nonincreasing_cvg_measure d (T : algebraOfSetsType d) (R : realFieldType)
   (mu : {measure set T -> \bar R}) (F : (set T) ^nat) :
   mu (F 0%N) < +oo ->
   (forall i, measurable (F i)) -> measurable (\bigcap_n F n) ->
@@ -1716,14 +1716,47 @@ have -> : \bigcap_n F n = F 0%N `&` \bigcap_n F n.
 rewrite -measureD // setDE setC_bigcap setI_bigcupr -[x in bigcup _ x]/G.
 have -> : (fun n => mu (F 0%N) - mu (F n)) = mu \o G.
   by apply: funext => n /=; rewrite measureD// setIidr//; exact/subsetPset/niF.
-apply: nondecreasing_cvg_mu.
+apply: nondecreasing_cvg_measure.
 - by move=> ?; apply: measurableD; exact: mF.
 - rewrite -setI_bigcupr; apply: measurableI; first exact: mF.
   by rewrite -@setC_bigcap; exact: measurableC.
 - by move=> n m NM; apply/subsetPset; apply: setDS; apply/subsetPset/niF.
 Qed.
 
+Lemma cvg_measure_bigcup {d} {M : sigmaRingType d} {R : realFieldType}
+  {mu : {measure set M -> \bar R}} (A : (set M)^nat)
+  (mA : forall i, measurable (A i)) :
+  mu (\bigcup_(i < n) A i) @[n-->\oo] --> mu (\bigcup_n A n).
+Proof.
+rewrite -bigcup_bigsetU_bigcup bigcup_bigsetU.
+under eq_bigcupr do rewrite -bigcup_mkord.
+apply: nondecreasing_cvg_measure => [i||n m nm]; [exact: bigcup_measurable|
+  by apply: bigcup_measurable => ? ?; exact: bigcup_measurable|].
+by apply/subsetPset => x [i/= i_n Aix]; exists i => //=; exact: leq_trans nm.
+Qed.
+
+Lemma cvg_measure_bigcap {d} {M : measurableType d} {R : realFieldType}
+    {mu : {measure set M -> \bar R}} (A : (set M)^nat)
+    (mA : forall i, measurable (A i)) :
+  mu (A 0%N) \is a fin_num ->
+  mu (\bigcap_(i < n.+1) A i) @[n-->\oo] --> mu (\bigcap_n A n).
+Proof.
+move=> muA0.
+rewrite [\bigcap_n A n] (_:_ = \bigcap_n (\bigcap_(i < n.+1) A i)).
+  by rewrite eqEsubset/bigcap; split=> [a/= + j _  i _|a/= aIa i _];
+    [exact|exact: (aIa i.+1)].
+apply: nonincreasing_cvg_measure.
+- by rewrite bigcap_mkord big_ord1 -ge0_fin_numE.
+- by move=> i; exact: bigcap_measurableType.
+- by apply: bigcap_measurableType=> k _; exact: bigcap_measurableType.
+- by move=> n m nm; apply/subsetPset=> x + i/= i_n; apply; exact: leq_trans nm.
+Qed.
+
 End measure_continuity.
+#[deprecated(since="mathcomp-analysis 1.17.0", use=nondecreasing_cvg_measure)]
+Notation nondecreasing_cvg_mu := nondecreasing_cvg_measure.
+#[deprecated(since="mathcomp-analysis 1.17.0", use=nonincreasing_cvg_measure)]
+Notation nonincreasing_cvg_mu := nonincreasing_cvg_measure.
 
 Section g_sigma_algebra_measure_unique_trace.
 Context d (R : realType) (T : measurableType d).