proposition: Lemma measurable_ln (R : realType) : measurable_fun [set~ (0:R)] (@ln R).
proof: Proof. rewrite (_ : [set~ 0] = `]-oo, 0[ `|` `]0, +oo[); last first. by rewrite -(setCitv `[0, 0]); apply/seteqP; split => [|]x/=; rewrite in_itv/= -eq_le eq_sym; [move/eqP/negbTE => ->|move/negP/eqP]. apply/measurable_funU => //; split. - apply/(@measurable_restrict _ _ _ _ _ setT) => //. rewrite (_ : _ \_ _ = cst (0:R))//; apply/funext => y; rewrite patchE. by case: ifPn => //; rewrite inE/= in_itv/= => y0; rewrite ln0// ltW. - have : {in `]0, +oo[%classic, continuous (@ln R)}. by move=> x; rewrite inE/= in_itv/= andbT => x0; exact: continuous_ln. rewrite -continuous_open_subspace; last exact: interval_open. by move/subspace_continuous_measurable_fun; apply; exact: measurable_itv. 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