broken

theories/borel_hierarchy.v

@@ -47,6 +47,8 @@ Proof. by exists (fun=> S)=> //; rewrite bigcup_const. Qed.
 
 End Gdelta_Fsigma.
 
+Import OcitvMeasurable.
+
 Lemma Gdelta_measurable {R : realType} (S : set R) : Gdelta S -> measurable S.
 Proof.
 move=> [] B oB ->; apply: bigcapT_measurable => i.

theories/ftc.v

@@ -68,6 +68,8 @@ Notation mu := (@lebesgue_measure R).
 Local Open Scope ereal_scope.
 Implicit Types (f : R -> R) (a : itv_bound R).
 
+Import OcitvMeasurable.
+
 Let FTC0 f a : mu.-integrable setT (EFin \o f) ->
   let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) f t)%R in
   forall x, a < BRight x -> lebesgue_pt f x ->
@@ -83,7 +85,7 @@ apply: (@cvg_at_right_left_dnbhs _ R^o).
     rewrite /E lebesgue_measure_itv/= lte_fin ltrDl d_gt0.
     by rewrite -EFinD -addrA subrKC.
   have nice_E y : nicely_shrinking y (E y).
-    split=> [n|]; first exact: measurable_itv.
+    split=> [n|]; first exact: newmeasurable_itv.
     exists (2%R, fun n => PosNum (d_gt0 n)); split => //= [n z|n].
       rewrite /E/= in_itv/= /ball/= ltr_distlC => /andP[yz ->].
       by rewrite (lt_le_trans _ yz)// ltrBlDr ltrDl.
@@ -134,7 +136,7 @@ apply: (@cvg_at_right_left_dnbhs _ R^o).
     rewrite /E lebesgue_measure_itv/= lte_fin -ltrBrDr.
     by rewrite ltrDl Nd_gt0 -EFinD opprD addNKr.
   have nice_E y : nicely_shrinking y (E y).
-    split=> [n|]; first exact: measurable_itv.
+    split=> [n|]; first exact: newmeasurable_itv.
     exists (2%R, (fun n => PosNum (Nd_gt0 n))); split => //=.
       by rewrite -oppr0; exact: cvgN.
     move=> n z.
@@ -328,6 +330,8 @@ End FTC.
 #[deprecated(since="mathcomp-analysis 1.17.0", note="renamed to `integrable_locally_restrict`")]
 Notation integrable_locally := integrable_locally_restrict (only parsing).
 
+Import OcitvMeasurable.
+
 Definition parameterized_integral {R : realType}
     (mu : {measure set (measurableTypeR R) -> \bar R})
     a x (f : R -> R) : R :=
@@ -352,7 +356,7 @@ have /ifab : (mu `[a, c] < d%:E)%E.
   rewrite lebesgue_measure_itv/= lte_fin.
   case: ifPn => // {}ac; rewrite -EFinD lte_fin.
   by move: ac; near: c; exact: nbhs_right_ltDr.
-move=> /(_ (measurable_itv _)) {ifab}.
+move=> /(_ (newmeasurable_itv _)) {ifab}.
 apply: le_lt_trans.
 have acbc : `[a, c] `<=` `[a, b].
   apply: subset_itvl; rewrite bnd_simp; move: ac; near: c.
@@ -524,6 +528,8 @@ rewrite mem_set ?mulr1 /=; first exact: subset_itv_oo_cc.
 exact: cvg_patch.
 Qed.
 
+Import OcitvMeasurable.
+
 Corollary continuous_FTC2 f F a b : (a < b)%R ->
   {within `[a, b], continuous f} ->
   derivable_oo_LRcontinuous F a b ->
@@ -772,6 +778,8 @@ Notation mu := lebesgue_measure.
 Local Open Scope ereal_scope.
 Implicit Types (F G f g : R -> R) (a b : R).
 
+Import OcitvMeasurable.
+
 Lemma integration_by_parts F G f g a b : (a < b)%R ->
     {within `[a, b], continuous f} ->
     derivable_oo_LRcontinuous F a b ->
@@ -824,6 +832,8 @@ Context {R : realType}.
 Notation mu := lebesgue_measure.
 Implicit Types (F G f g : R -> R) (a b : R).
 
+Import OcitvMeasurable.
+
 Lemma Rintegration_by_parts F G f g a b :
     (a < b)%R ->
     {within `[a, b], continuous f} ->
@@ -1030,6 +1040,8 @@ Context {R : realType}.
 Notation mu := lebesgue_measure.
 Implicit Types (F G f : R -> R) (a b : R).
 
+Import OcitvMeasurable.
+
 Lemma integration_by_substitution_decreasing F G a b : (a <= b)%R ->
   {in `[a, b] &, {homo F : x y /~ (x < y)%R}} ->
   {in `]a, b[, continuous F^`()} ->
@@ -1046,7 +1058,7 @@ have cF := derivable_oo_LRcontinuous_within Fab.
 have FbFa : (F b < F a)%R by apply: decrF; rewrite //= in_itv/= (ltW ab) lexx.
 have mGFF' : measurable_fun `]a, b[ ((G \o F) * F^`())%R.
   apply: measurable_funM.
-  - apply: (measurable_comp (measurable_itv `]F b, F a[)).
+  - apply: (measurable_comp (newmeasurable_itv `]F b, F a[)).
     + exact: decreasing_image_oo.
     + apply: subspace_continuous_measurable_fun => //.
       by apply: continuous_subspaceW cG; exact/subset_itv_oo_cc.
@@ -1359,7 +1371,7 @@ transitivity (limn (fun n =>
   - exact: iota_uniq.
   - exact: (@sub_trivIset _ _ _ [set: nat]).
   - apply/measurable_EFinP.
-    apply: (measurable_funS (measurable_itv `]a, (a + n.+1%:R)%R[)).
+    apply: (measurable_funS (newmeasurable_itv `]a, (a + n.+1%:R)%R[)).
       rewrite big_mkord -bigsetU_seqDU.
       rewrite -(bigcup_mkord _ (fun k => `]a, (a + k.+1%:R)%R[%classic)).
       apply: bigcup_sub => k/= kn.
@@ -1510,7 +1522,7 @@ have mF' : measurable_fun `]a, +oo[ (- F)%R^`().
   exact: near_in_itvoy.
 rewrite -!integral_itvob_itvcb.
 - apply/measurable_EFinP; apply: measurable_funM; last exact: measurableT_comp.
-  apply: (measurable_comp (measurable_itv `]-oo, (- F a)%R[)).
+  apply: (measurable_comp (newmeasurable_itv `]-oo, (- F a)%R[)).
   - move=> _ /= [x + <-] => ax.
     by rewrite in_itv/= ltrN2 incrF ?in_itv/= ?lexx//= (itvP ax).
   - apply: open_continuous_measurable_fun; first exact: interval_open.
@@ -1776,11 +1788,12 @@ Qed.
 
 End integration_by_substitution.
 
-
 Section ge0_integration_by_substitution_shift.
 Context {R : realType}.
 Notation mu := (@lebesgue_measure R).
 
+Import OcitvMeasurable.
+
 Lemma ge0_integration_by_substitution_shift_itvy (f : R -> R) (r e : R) :
   {within `[r + e, +oo[, continuous f} ->
   {in `]r + e, +oo[, forall x : R, 0 <= f x} ->
@@ -1828,6 +1841,8 @@ Context {R : realType}.
 Let mu := (@lebesgue_measure R).
 Local Open Scope ereal_scope.
 
+Import OcitvMeasurable.
+
 Lemma integration_by_substitution_onem (G : R -> R) (r : R) :
   (0 <= r <= 1)%R ->
   {within `[0%R, r], continuous G} ->
@@ -1869,6 +1884,8 @@ Context {R : realType}.
 Let mu := @lebesgue_measure R.
 Local Open Scope ereal_scope.
 
+Import OcitvMeasurable.
+
 Lemma ge0_symfun_integralT (f : R -> R) : (forall x, 0 <= f x)%R ->
   continuous f -> f =1 f \o -%R ->
   \int[mu]_x (f x)%:E = 2%:E * \int[mu]_(x in [set x | (0 <= x)%R]) (f x)%:E.

theories/gauss_integral.v

@@ -41,6 +41,8 @@ by apply: (cvg_comp (fun x => x ^+ 2) (fun x => expR (- x)));
   [exact: cvgr_expr2|exact: cvgr_expR].
 Qed.
 
+Import OcitvMeasurable.
+
 Lemma measurable_gauss_fun : measurable_fun setT gauss_fun.
 Proof. by apply: measurableT_comp => //; exact: measurableT_comp. Qed.
 
@@ -63,6 +65,8 @@ Implicit Type x : R.
 
 Let mu : {measure set _ -> \bar R} := @lebesgue_measure R.
 
+Import OcitvMeasurable.
+
 Definition integral0y_gauss := \int[mu]_(x in `[0%R, +oo[) gauss_fun x.
 
 Let integral0y_gauss_ge0 : 0 <= integral0y_gauss.
@@ -350,6 +354,8 @@ Context {R : realType}.
 Import gauss_integral_proof.
 Let mu := @lebesgue_measure R.
 
+Import OcitvMeasurable.
+
 Lemma integral0y_gauss :
   (\int[mu]_(x in `[0%R, +oo[) (gauss_fun x)%:E)%E = (Num.sqrt pi / 2)%:E.
 Proof.

theories/hoelder.v

@@ -362,6 +362,8 @@ Variable mu : {measure set T -> \bar R}.
 Local Open Scope ereal_scope.
 Implicit Types (p q : R) (f g : T -> R).
 
+Import OcitvMeasurable.
+
 Let measurableT_comp_powR f p :
   measurable_fun [set: T] f -> measurable_fun setT (fun x => f x `^ p)%R.
 Proof. exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)). Qed.
@@ -498,6 +500,8 @@ Section hoelder2.
 Context {R : realType}.
 Local Open Scope ring_scope.
 
+Import OcitvMeasurable.
+
 Lemma hoelder2 (a1 a2 b1 b2 : R) (p q : R) :
   0 <= a1 -> 0 <= a2 -> 0 <= b1 -> 0 <= b2 ->
   0 < p -> 0 < q -> p^-1 + q^-1 = 1 ->
@@ -534,6 +538,8 @@ Context {R : realType}.
 Local Open Scope ring_scope.
 Local Open Scope convex_scope.
 
+Import OcitvMeasurable.
+
 Lemma convex_powR p : 1 <= p ->
   convex_function (`[0, +oo[%classic : set R) (@powR R ^~ p).
 Proof.
@@ -595,6 +601,8 @@ by apply: (convex_powR p1 (Itv01 _ _)) => //=;
   rewrite ?inE/= ?in_itv/= ?normr_ge0// ?invr_ge0// invf_le1 ?ler1n.
 Qed.
 
+Import OcitvMeasurable.
+
 Let measurableT_comp_powR f p :
   measurable_fun setT f -> measurable_fun setT (fun x => f x `^ p)%R.
 Proof. exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)). Qed.
@@ -788,6 +796,8 @@ Definition finite_norm d (T : measurableType d) (R : realType)
     (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> R) :=
   ('N[ mu ]_p [ EFin \o f ] < +oo)%E.
 
+Import OcitvMeasurable.
+
 HB.mixin Record isLfunction d (T : measurableType d) (R : realType)
     (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E) (f : T -> R)
   & @MeasurableFun d _ T R f := {

theories/independence.v

@@ -440,6 +440,8 @@ Context {R : realType} d d' (T : measurableType d) (T' : measurableType d').
 Variable P : probability T R.
 Local Open Scope ring_scope.
 
+Import OcitvMeasurable.
+
 Lemma independent_RVs2_comp (X Y : {RV P >-> R}) (f g : {mfun R >-> R}) :
   independent_RVs2 P X Y -> independent_RVs2 P (f \o X) (g \o Y).
 Proof.
@@ -521,6 +523,8 @@ Context {R : realType} d (T : measurableType d).
 Variable P : probability T R.
 Local Open Scope ereal_scope.
 
+Import OcitvMeasurable.
+
 Lemma independent_RVs2_setI_preimage (X Y : {mfun T >-> R}) (A1 A2 : set R) :
   measurable A1 -> measurable A2 ->
   independent_RVs2 P X Y ->
@@ -555,6 +559,8 @@ Context {R : realType} d (T : measurableType d).
 Variable P : probability T R.
 Local Open Scope ereal_scope.
 
+Import OcitvMeasurable.
+
 Lemma independent_Lfun1_expectation_product_measure_lty (X Y : {RV P >-> R}) :
   independent_RVs2 P X Y ->
   (X : _ -> _) \in Lfun P 1 -> (Y : _ -> _) \in Lfun P 1 ->
@@ -603,6 +609,7 @@ Variable P : probability T R.
 Local Open Scope ereal_scope.
 
 Import HBNNSimple.
+Import OcitvMeasurable.
 
 #[local] Lemma expectationM_nnsfun (f g : {nnsfun T >-> R}) :
   (forall y y', y \in range f -> y' \in range g ->
@@ -760,14 +767,14 @@ rewrite !inE => /orP[|]/eqP->{i} //=.
       by apply: measurable_indic; exact: mA.
     apply: measurable_funM => //.
     by apply: measurable_indic; exact: mB.
-  rewrite /measurable_fun => /(_ measurableT _ (measurable_set1 x)).
+  rewrite /measurable_fun => /(_ measurableT _ (newmeasurable_set1 x)).
   by rewrite setTI.
 - have : @measurable_fun _ _ (g_sigma_algebra_preimageType Y) _ setT (Y_ n).
     rewrite nnsfun_approxE//; apply: measurable_funD => //=.
       apply: measurable_sum => //= k'; apply: measurable_funM => //.
       by apply: measurable_indic; exact: mA.
     by apply: measurable_funM => //; apply: measurable_indic; exact: mB.
-  by move=> /(_ measurableT [set y] (measurable_set1 y)); rewrite setTI.
+  by move=> /(_ measurableT [set y] (newmeasurable_set1 y)); rewrite setTI.
 Qed.
 
 End expectationM.
@@ -778,6 +785,7 @@ Variable P : probability T R.
 Local Open Scope ereal_scope.
 
 Import HBNNSimple.
+Import OcitvMeasurable.
 
 Lemma independent_Lfun1_expectationM_lty (X Y : {RV P >-> R}) :
   independent_RVs2 P X Y ->

theories/kernel.v

@@ -659,6 +659,7 @@ Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
 Variable k : X * Y -> \bar R.
 
 Import HBNNSimple.
+Import OcitvMeasurable.
 
 Lemma measurable_fun_xsection_integral
     (l : X -> {measure set Y -> \bar R})
@@ -763,6 +764,8 @@ Definition kdirac (mf : measurable_fun [set: X] f) (x : X) :
 
 Hypothesis mf : measurable_fun [set: X] f.
 
+Import OcitvMeasurable.
+
 Let measurable_fun_kdirac U : measurable U ->
   measurable_fun [set: X] (kdirac mf ^~ U).
 Proof.
@@ -885,6 +888,8 @@ Variable f : R.-ker X ~> Y.
 Definition knormalize (P : probability Y R) : X -> {measure set Y -> \bar R} :=
   fun x => mnormalize (f x) P.
 
+Import OcitvMeasurable.
+
 Let measurable_knormalize (P : probability Y R) U :
   measurable U -> measurable_fun [set: X] (knormalize P ^~ U).
 Proof.
@@ -926,6 +931,8 @@ HB.instance Definition _ (P : probability Y R):=
 
 End knormalize.
 
+Import OcitvMeasurable.
+
 Lemma measurable_fun_mnormalize d d' (X : measurableType d)
     (Y : pmeasurableType d') (R : realType) (k : R.-ker X ~> Y) :
   measurable_fun [set: X] (fun x => mnormalize (k x) point : pprobability Y R).

theories/lebesgue_integral_theory/giry.v

@@ -101,6 +101,7 @@ Context d (T : measurableType d) (R : realType).
 Definition giry_int (mu : giry T R) (f : T -> \bar R) := \int[mu]_x f x.
 
 Import HBNNSimple.
+Import OcitvMeasurable.
 
 (**md The idea is to reconstruct f from simple functions, then use measurability
   of giry_ev. Reference: Tom Avery. Codensity and the Giry monad.
@@ -287,6 +288,7 @@ by apply: measurable_giry_int => //; exact: measurable_giry_ev.
 Qed.
 
 Import HBNNSimple.
+Import OcitvMeasurable.
 
 Lemma sintegral_giry_join (M : giry (giry T R) R) (h : {nnsfun T >-> R}) :
   sintegral (giry_join M) h = \int[M]_mu sintegral mu h.

theories/lebesgue_integral_theory/lebesgue_Rintegral.v

@@ -106,6 +106,8 @@ Lemma Rintegral_ge0 D f : (forall x, D x -> 0 <= f x) ->
   0 <= \int[mu]_(x in D) f x.
 Proof. by move=> f0; rewrite fine_ge0// integral_ge0. Qed.
 
+Import OcitvMeasurable.
+
 Lemma le_normr_Rintegral D f : measurable D -> mu.-integrable D (EFin \o f) ->
   `|\int[mu]_(t in D) f t| <= \int[mu]_(t in D) `|f t|.
 Proof.
@@ -197,6 +199,8 @@ Context {R : realType}.
 Notation mu := (@lebesgue_measure R).
 Implicit Type f : R -> R.
 
+Import OcitvMeasurable.
+
 Lemma Rintegral_itvbo_itvbc (a : itv_bound R) (r : R) f :
   mu.-integrable [set` Interval a (BLeft r)] (EFin \o f) ->
    \int[mu]_(x in [set` Interval a (BLeft r)]) (f x) =

theories/lebesgue_integral_theory/lebesgue_integrable.v

@@ -283,6 +283,8 @@ case: fi => mf; apply: le_lt_trans; apply: ge0_le_integral => //.
 - by move=> x Dx; rewrite -/((abse \o f) x) -funeposDneg leeDl.
 Qed.
 
+Import OcitvMeasurable.
+
 Lemma integrableMr (h : T -> R) g :
   measurable_fun D h -> [bounded h x | x in D] ->
   mu_int g -> mu_int ((EFin \o h) \* g).
@@ -350,6 +352,8 @@ Context d {T : measurableType d} {R : realType}.
 Variable mu : {measure set T -> \bar R}.
 Implicit Types (D A B : set T) (f : T -> R).
 
+Import OcitvMeasurable.
+
 Lemma integrable_norm D f : mu.-integrable D (EFin \o f) ->
   mu.-integrable D (EFin \o (normr \o f)).
 Proof.
@@ -380,6 +384,8 @@ Proof. by move/integrable_funeneg => /[apply]; rewrite funerneg. Qed.
 
 End Rintegrable.
 
+Import OcitvMeasurable.
+
 Lemma integrable_indic_itv {R : realType} (a b : R) (b0 b1 : bool) :
   let mu := lebesgue_measure in
   mu.-integrable setT (EFin \o \1_[set` Interval (BSide b0 a) (BSide b1 b)]).