proposition: Lemma measurable_fun_mnormalize d d' (X : measurableType d) (Y : measurableType d') (R : realType) (k : R.-ker X ~> Y) : measurable_fun [set: X] (fun x => [the probability _ _ of mnormalize (k x) point] : pprobability Y R).
proof: Proof. apply: (@measurability _ _ _ _ _ _ (@pset _ _ _ : set (set (pprobability Y R)))) => //. move=> _ -[_ [r r01] [Ys mYs <-]] <-. rewrite /mnormalize /mset /preimage/=. apply: emeasurable_fun_infty_o => //. rewrite /mnormalize/=. rewrite (_ : (fun x => _) = (fun x => if (k x setT == 0) || (k x setT == +oo) then \d_point Ys else k x Ys * ((fine (k x setT))^-1)%:E)); last first. by apply/funext => x/=; case: ifPn. apply: measurable_fun_if => //. - apply: (measurable_fun_bool true) => //. rewrite (_ : _ @^-1` _ = [set t | k t setT == 0] `|` [set t | k t setT == +oo]); last first. by apply/seteqP; split=> x /= /orP//. by apply: measurableU; exact: kernel_measurable_eq_cst. - apply/emeasurable_funM; first exact/measurable_funTS/measurable_kernel. apply/EFin_measurable_fun; rewrite setTI. apply: (@measurable_comp _ _ _ _ _ _ [set r : R | r != 0%R]). + exact: open_measurable. + by move=> /= _ [x /norP[s0 soo]] <-; rewrite -eqe fineK ?ge0_fin_numE ?ltey. + apply: open_continuous_measurable_fun => //; apply/in_setP => x /= x0. exact: inv_continuous. + by apply: measurableT_comp => //; exact/measurable_funS/measurable_kernel. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology normedtype sequences esum measure numfun lebesgue_measure lebesgue_integral