diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v index e4efb00d0..36492890e 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v +++ b/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. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v index 6803c75dc..ae0c1570d 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v +++ b/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. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 4894aa3f3..8d55c854e 100644 --- a/theories/lebesgue_measure.v +++ b/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. diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index c82beeb32..ef6c2c0e7 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/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). diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 002dcfe9e..1fdbbb44f 100644 --- a/theories/measurable_realfun.v +++ b/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))).