proposition: Lemma measurable_funM D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \* g).
proof: Proof. move=> mf mg; rewrite (_ : (_ \* _) = (fun x => 2%:R^-1 * (f x + g x) ^+ 2) \- (fun x => 2%:R^-1 * (f x ^+ 2)) \- (fun x => 2%:R^-1 * (g x ^+ 2))). apply: measurable_funB; first apply: measurable_funB. - apply: measurableT_comp => //. by apply: measurableT_comp (measurable_exprn _) _; exact: measurable_funD. - apply: measurableT_comp => //. exact: measurableT_comp (measurable_exprn _) _. - apply: measurableT_comp => //. exact: measurableT_comp (measurable_exprn _) _. rewrite funeqE => x /=; rewrite -2!mulrBr sqrrD (addrC (f x ^+ 2)) -addrA. rewrite -(addrA (f x * g x *+ 2)) -opprB opprK (addrC (g x ^+ 2)) addrK. by rewrite -(mulr_natr (f x * g x)) -(mulrC 2) mulrA mulVr ?mul1r// unitfE. 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