proposition: Lemma measurable_powR (R : realType) p : measurable_fun [set: R] (@powR R ^~ p).
proof: Proof. apply: measurable_fun_if => //. - apply: (measurable_fun_bool true); rewrite (_ : _ @^-1` _ = [set 0])//. by apply/seteqP; split => [_ /eqP ->//|_ -> /=]; rewrite eqxx. - rewrite setTI; apply: measurableT_comp => //. rewrite (_ : _ @^-1` _ = [set~ 0]); first exact: measurableT_comp. by apply/seteqP; split => [x /negP/negP/eqP|x x0]//=; exact/negbTE/eqP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology numfun normedtype HB(structures) sequences esum measure real_interval realfun exp lebesgue_stieltjes_measure