proposition: Lemma measurable_normr D : measurable_fun D (@normr _ R).
proof: Proof. move=> mD; apply: (measurability (RGenOInfty.measurableE R)) => //. move=> /= _ [_ [x ->] <-]; apply: measurableI => //. have [x0|x0] := leP 0 x. rewrite [X in measurable X](_ : _ = `]-oo, (- x)[ `|` `]x, +oo[)%classic. by apply: measurableU; apply: measurable_itv. rewrite predeqE => r; split => [|[|]]; rewrite preimage_itv ?in_itv ?andbT/=. - have [r0|r0] := leP 0 r; [rewrite ger0_norm|rewrite ltr0_norm] => // xr; rewrite 2!in_itv/=. + by right; rewrite xr. + by left; rewrite ltrNr. - move=> rx /=. by rewrite ler0_norm 1?ltrNr// (le_trans (ltW rx))// lerNl oppr0. - by rewrite in_itv /= andbT => xr; rewrite (lt_le_trans _ (ler_norm _)). rewrite [X in measurable X](_ : _ = setT)// predeqE => r. by split => // _; rewrite /= in_itv /= andbT (lt_le_trans x0). 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