Removed double measurable for reals+changed deprecated lemmas

theories/lebesgue_integral_theory/lebesgue_integral_definition.v

@@ -338,7 +338,7 @@ apply: cvgeZl => //=; rewrite [X in _ --> X](_ : _ =
     mu (\bigcup_n (f @^-1` [set r] `&` fleg c n))).
   by rewrite -setI_bigcupr bigcup_fleg// setIT.
 have ? k i : measurable (f @^-1` [set k] `&` fleg c i) by exact: measurableI.
-apply: nondecreasing_cvg_mu; [by []|exact: bigcupT_measurable|].
+apply: nondecreasing_cvg_measure; [by []|exact: bigcupT_measurable|].
 move=> n m nm; apply/subsetPset; apply: setIS.
 by move/(nd_fleg c) : nm => /subsetPset.
 Unshelve. all: by end_near. Qed.

theories/lebesgue_integral_theory/lebesgue_integral_fubini.v

@@ -69,7 +69,7 @@ Proof.
 move=> F ndF; rewrite /B /= => BF; split.
   by apply: bigcupT_measurable => n; have [] := BF n.
 have phiF x : phi (F i) x @[i \oo] --> phi (\bigcup_i F i) x.
-  rewrite /phi /= xsection_bigcup; apply: nondecreasing_cvg_mu.
+  rewrite /phi /= xsection_bigcup; apply: nondecreasing_cvg_measure.
   - by move=> n; apply: measurable_xsection; case: (BF n).
   - by apply: bigcupT_measurable => i; apply: measurable_xsection; case: (BF i).
   - by move=> m n mn; exact/subsetPset/le_xsection/subsetPset/ndF.
@@ -89,7 +89,7 @@ Proof.
 move=> F ndF; rewrite /B /= => BF; split.
   by apply: bigcupT_measurable => n; have [] := BF n.
 have psiF x : psi (F i) x @[i \oo] --> psi (\bigcup_i F i) x.
-  rewrite /psi /= ysection_bigcup; apply: nondecreasing_cvg_mu.
+  rewrite /psi /= ysection_bigcup; apply: nondecreasing_cvg_measure.
   - by move=> n; apply: measurable_ysection; case: (BF n).
   - by apply: bigcupT_measurable => i; apply: measurable_ysection; case: (BF i).
   - by move=> m n mn; exact/subsetPset/le_ysection/subsetPset/ndF.

theories/lebesgue_measure.v

@@ -630,7 +630,7 @@ Let lebesgue_measure_itvoo_subr1 (a : R) :
 Proof.
 rewrite itv_bnd_open_bigcup//; transitivity (limn (lebesgue_measure \o
     (fun k => `]a - 1, a - k.+1%:R^-1]%classic : set R))).
-  apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu.
+  apply/esym/cvg_lim => //; apply: nondecreasing_cvg_measure.
   - by move=> ?; exact: measurable_itv.
   - by apply: bigcup_measurable => k _; exact: measurable_itv.
   - move=> n m nm; apply/subsetPset => x /=; rewrite !in_itv/= => /andP[->/=].
@@ -728,7 +728,7 @@ Let lebesgue_measure_itv_bnd_infty x (a : R) :
 Proof.
 rewrite itv_bndy_bigcup_BRight; transitivity (limn (lebesgue_measure \o
     (fun k => [set` Interval (BSide x a) (BRight (a + k%:R))] : set R))).
-  apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu.
+  apply/esym/cvg_lim => //; apply: nondecreasing_cvg_measure.
   + by move=> k; exact: measurable_itv.
   + by apply: bigcup_measurable => k _; exact: measurable_itv.
   + move=> m n mn; apply/subsetPset => r/=; rewrite !in_itv/= => /andP[->/=].
@@ -744,7 +744,7 @@ Let lebesgue_measure_itv_infty_bnd y (b : R) :
 Proof.
 rewrite itvNy_bnd_bigcup_BLeft; transitivity (limn (lebesgue_measure \o
     (fun k => [set` Interval (BLeft (b - k%:R)) (BSide y b)] : set R))).
-  apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu.
+  apply/esym/cvg_lim => //; apply: nondecreasing_cvg_measure.
   + by move=> k; exact: measurable_itv.
   + by apply: bigcup_measurable => k _; exact: measurable_itv.
   + move=> m n mn; apply/subsetPset => r/=; rewrite !in_itv/= => /andP[+ ->].
@@ -981,7 +981,7 @@ Proof.
 move=> mD Dfin epspos; pose Dn n := D `&` [set` `[-(n%:R), n%:R]]%R.
 have mDn n : measurable (Dn n) by exact: measurableI.
 have : mu \o Dn @ \oo --> mu (\bigcup_n Dn n).
-  apply: nondecreasing_cvg_mu => //.
+  apply: nondecreasing_cvg_measure => //.
   - by apply: bigcup_measurable => // ? _; exact: mDn.
   - move=> n m nm; apply/subsetPset; apply: setIS => z /=; rewrite !in_itv/=.
     move=> /andP[nz zn]; rewrite (le_trans _ nz)/= ?(le_trans zn) ?ler_nat//.
@@ -1076,7 +1076,7 @@ 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.
 have : (fun n => mu (F n `&` D)) @ \oo --> +oo.
-  rewrite -FDp; apply: nondecreasing_cvg_mu.
+  rewrite -FDp; apply: nondecreasing_cvg_measure.
   - by move=> i; apply: measurableI => //; exact: (ffin i).1.
   - by apply: bigcup_measurable => i _; exact: (measurableI _ _ (ffin i).1).
   - by move=> n m nm; apply/subsetPset; apply: setSI; exact/subsetPset/Fsub.

theories/lebesgue_stieltjes_measure.v

@@ -514,14 +514,15 @@ End wlength_extension.
 Arguments lebesgue_stieltjes_measure {R}.
 
 Definition measurableTypeR (R : realType) :=
-  g_sigma_algebraType R.-ocitv.-measurable.
+  g_sigma_algebraType (@ocitv R).
 
 Section lebesgue_stieltjes_measure.
 Context {R : realType}.
 
-Definition lebesgue_display : measure_display := (R.-ocitv.-measurable).-sigma.
-Definition measurableR : set_system R :=
-  (R.-ocitv.-measurable).-sigma.-measurable.
+Definition lebesgue_display : measure_display :=
+  (@ocitv R).-sigma.
+Definition measurableR : set (set R) :=
+  (@ocitv R).-sigma.-measurable.
 
 HB.instance Definition _ : Measurable lebesgue_display (measurableTypeR R) :=
    Measurable.on (measurableTypeR R).

theories/measurable_realfun.v

@@ -496,7 +496,6 @@ Qed.
 
 End rgenopens.
 End RGenOpens.
-
 Section erealwithrays.
 Variable R : realType.
 Implicit Types (x y z : \bar R) (r s : R).
@@ -1729,7 +1728,7 @@ have Ek0 k : \bigcap_n (E k n) = 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)%R.
   have : mu \o E k @ \oo --> mu set0.
-    rewrite -(Ek0 k); apply: nonincreasing_cvg_mu => //.
+    rewrite -(Ek0 k); apply: nonincreasing_cvg_measure => //.
     - by rewrite (le_lt_trans _ finA)// le_measure// ?inE// => ? [? _ []].
     - exact: bigcap_measurable.
   rewrite measure0; case/fine_cvg/(_ (interior (ball 0%R ek))).