proposition: Lemma measurable_funD D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \+ g).
proof: Proof. move=> mf mg mD; apply: (measurability (RGenOInfty.measurableE R)) => //. move=> /= _ [_ [a ->] <-]; rewrite preimage_itv_o_infty. rewrite [X in measurable X](_ : _ = \bigcup_(q : rat) ((D `&` [set x | ratr q < f x]) `&` (D `&` [set x | a - ratr q < g x]))). apply: bigcupT_measurable_rat => q; apply: measurableI. - by rewrite -preimage_itv_o_infty; apply: mf => //; apply: measurable_itv. - by rewrite -preimage_itv_o_infty; apply: mg => //; apply: measurable_itv. rewrite predeqE => x; split => [|[r _] []/= [Dx rfx]] /= => [[Dx]|[_]]. rewrite -ltrBlDr => /rat_in_itvoo[r]; rewrite inE /= => /itvP h. exists r => //; rewrite setIACA setIid; split => //; split => /=. by rewrite h. by rewrite ltrBlDr addrC -ltrBlDr h. by rewrite ltrBlDr=> afg; rewrite (lt_le_trans afg)// addrC lerD2r ltW. 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