proposition: Lemma emeasurable_funM D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \* g).
proof: Proof. move=> mf mg mD. have m0 : measurable ([set 0] : set (\bar R)) by []. have mC0 : measurable ([set~ 0] : set (\bar R)) by apply: measurableC. have mCoo : measurable (~` [set -oo; +oo] : set (\bar R)). exact/measurableC/measurableU. have mfg : measurable (D `&` [set x | f x *? g x]). suff -> : [set x | f x *? g x] = (f @^-1` (~` [set 0]) `|` g @^-1` (~` [set -oo; +oo])) `&` (g @^-1` (~` [set 0]) `|` f @^-1` (~` [set -oo; +oo])). by rewrite setIIr; apply: measurableI; rewrite setIUr; apply: measurableU; do ?[apply: mf|apply: mg]. apply/predeqP=> x; rewrite /preimage/= /mule_def !(negb_and, negb_or). rewrite !(rwP2 eqP idP) !(rwP2 negP idP) !(rwP2 orP idP). rewrite !(rwP2 negP idP) !(rwP2 orP idP) !(rwP2 andP idP). rewrite eqe_absl leey andbT (orbC (g x == +oo)). by rewrite eqe_absl leey andbT (orbC (f x == +oo)). wlog fg : D mD mf mg mfg / forall x, D x -> f x *? g x => [hwlogM|]; last first. have [f_ f_cvg] := approximation_sfun mD mf. have [g_ g_cvg] := approximation_sfun mD mg. apply: (emeasurable_fun_cvg (fun n x => (f_ n x * g_ n x)%:E)) => //. move=> n; apply/EFin_measurable_fun. by apply: measurable_funM => //; exact: measurable_funTS. move=> x Dx; under eq_fun do rewrite EFinM. exact: cvgeM (fg _ _) (f_cvg _ _) (g_cvg _ _). move=> A mA; wlog NA0: A mD mf mg mA / ~ (A 0) => [hwlogA|]. have [] := pselect (A 0); last exact: hwlogA. move=> /(@setD1K _ 0)<-; rewrite preimage_setU setIUr. apply: measurableU; last by apply: hwlogA=> //; [exact: measurableD|case => /=]. have -> : (fun x => f x * g x) @^-1` [set 0] = f @^-1` [set 0] `|` g @^-1` [set 0]. apply/seteqP; split=> x /= => [/eqP|[]]; rewrite /preimage/=. by rewrite mule_eq0 => /orP[] /eqP->; [left|right]. by move=> ->; rewrite mul0e. by move=> ->; rewrite mule0. by rewrite setIUr; apply: measurableU; [apply: mf|apply: mg]. have-> : D `&` (fun x => f x * g x) @^-1` A = (D `&` [set x | f x *? g x]) `&` (fun x => f x * g x) @^-1` A. rewrite -setIA; congr (_ `&` _). apply/seteqP; split=> x; rewrite /preimage/=; last by case. move=> Afgx; split=> //; apply: neq0_mule_def. by apply: contra_notT NA0; rewrite negbK => /eqP <-. have Dfg : D `&` [set x | f x *? g x] `<=` D by apply: subIset; left. apply: hwlogM => //. - by apply: (measurable_funS mD) => //; do ?exact: measurableI. - by apply: (measurable_funS mD) => //; do ?exact: measurableI. - by rewrite -setIA setIid. - by move=> ? []. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun