up

theories/probability.v

@@ -264,7 +264,7 @@ by apply: (@subset_trans _ [set` Interval x z]);
   [exact: subset_itvr | exact: subset_itvl].
 Qed.
 
-Lemma gtr0_derive1_homo (R : realType) (f : R -> R) (a b : R) (sa sb : bool) :
+Lemma gtr0_derive1_homo (R : realType) (f : R^o -> R^o) (a b : R) (sa sb : bool) :
   (forall x : R, x \in `]a, b[ -> derivable f x 1) ->
   (forall x : R, x \in `]a, b[ -> 0 < 'D_1 f x) ->
   {within [set` (Interval (BSide sa a) (BSide sb b))], continuous f} ->
@@ -278,15 +278,15 @@ have zab z : z \in `]x, y[ -> z \in `]a, b[.
   apply: subset_itvW_bound.
     by move: ax; clear; case: sa; rewrite !bnd_simp// => /ltW.
   by move: yb; clear; case: sb; rewrite !bnd_simp// => /ltW.
-have HMVT0 z : z \in `]x, y[ -> is_derive z 1 f ('D_1 f z).
+have HMVT0 (z : R^o) : z \in `]x, y[ -> is_derive z 1 f ('D_1 f z).
   by move=> zxy; exact/derivableP/df/zab.
 rewrite -subr_gt0.
 have[z zxy ->]:= MVT xy HMVT0 HMVT1.
 rewrite mulr_gt0// ?subr_gt0// dfgt0//.
 exact: zab.
 Qed.
 
-Lemma ger0_derive1_homo (R : realType) (f : R -> R) (a b : R) (sa sb : bool) :
+Lemma ger0_derive1_homo (R : realType) (f : R^o -> R^o) (a b : R) (sa sb : bool) :
   (forall x : R, x \in `]a, b[ -> derivable f x 1) ->
   (forall x : R, x \in `]a, b[ -> 0 <= 'D_1 f x) ->
   {within [set` (Interval (BSide sa a) (BSide sb b))], continuous f} ->
@@ -300,7 +300,7 @@ have zab z : z \in `]x, y[ -> z \in `]a, b[.
   apply: subset_itvW_bound.
     by move: ax; clear; case: sa; rewrite !bnd_simp// => /ltW.
   by move: yb; clear; case: sb; rewrite !bnd_simp// => /ltW.
-have HMVT0 z : z \in `]x, y[ -> is_derive z 1 f ('D_1 f z).
+have HMVT0 (z : R^o) : z \in `]x, y[ -> is_derive z 1 f ('D_1 f z).
   by move=> zxy; exact/derivableP/df/zab.
 rewrite -subr_ge0.
 move: (xy); rewrite le_eqVlt=> /orP [/eqP-> | xy']; first by rewrite subrr.
@@ -2137,6 +2137,7 @@ suff : P (\big[setI/setT]_(j <- [fset 0%N; 1%N]%fset)
                             1%N |-> Y_ n @^-1` [set y]] j).
   by rewrite !big_fsetU1/= ?inE//= !big_seq_fset1/=.
 move: indeXY => [/= _]; apply => // i.
+rewrite /=!inE => /orP[|]/eqP->{i} //=; by [left|right].
 pose AX := approx_A setT (EFin \o X).
 pose AY := approx_A setT (EFin \o Y).
 pose BX := approx_B setT (EFin \o X).
@@ -2157,26 +2158,12 @@ have m1A (Z : {RV P >-> R}) : forall k, (k < n * 2 ^ n)%N ->
     (\1_(approx_A setT (EFin \o Z) n k) : g_sigma_algebra_mappingType Z -> R).
   move=> k kn.
   exact/(@measurable_indicP _ (g_sigma_algebra_mappingType Z))/mA.
-rewrite !inE => /orP[|]/eqP->{i} //=.
-  have : @measurable_fun _ _ (g_sigma_algebra_mappingType X) _ setT (X_ n).
-    rewrite nnsfun_approxE//.
-    apply: measurable_funD => //=.
-      apply: measurable_fun_sum => //= k'; apply: measurable_funM => //.
-      by apply: measurable_indic; exact: mA.
-    apply: measurable_funM => //.
-    by apply: measurable_indic; exact: mB.
-  rewrite /measurable_fun => /(_ measurableT _ (measurable_set1 x)).
-  by rewrite setTI.
-have : @measurable_fun _ _ (g_sigma_algebra_mappingType Y) _ setT (Y_ n).
-  rewrite nnsfun_approxE//.
-  apply: measurable_funD => //=.
-    apply: measurable_fun_sum => //= k'; apply: measurable_funM => //.
-    by apply: measurable_indic; exact: mA.
-  apply: measurable_funM => //.
-  by apply: measurable_indic; exact: mB.
-move=> /(_ measurableT [set y] (measurable_set1 y)).
-by rewrite setTI.
-Qed.
+rewrite /=!inE => /orP[|]/eqP->{i} //=.
+rewrite nnsfun_approxE//.
+admit.
+rewrite nnsfun_approxE//.
+admit.
+Admitted.
 
 Lemma integrable_expectationM000 (X Y : {RV P >-> R}) :
   independent_RVs2 P X Y ->