lemmas about measurable from PR prob_lang

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_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`
+    * lemmas `measurable_itv_bounded`, `measurableE`
+
+### Changed
 
 ### Changed
 - in `topology.v`:

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                         *)
@@ -987,6 +991,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 +1067,26 @@ 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_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); 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)//.
+  by apply/seteqP; split => // r /= -[_]; rewrite indicE; 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 +1151,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.
 
@@ -1182,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.

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.