proposition: Lemma emeasurable_funD D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \+ g).
proof: Proof. move=> mf mg mD. have Cnoom : measurable (~` [set -oo] : set (\bar R)) by apply: measurableC. have Cpoom : measurable (~` [set +oo] : set (\bar R)) by apply: measurableC. have mfg : measurable (D `&` [set x | f x +? g x]). suff -> : [set x | f x +? g x] = (f @^-1` (~` [set +oo]) `|` g @^-1` (~` [set -oo])) `&` (f @^-1` (~` [set -oo]) `|` g @^-1` (~` [set +oo])). by rewrite setIIr; apply: measurableI; rewrite setIUr; apply: measurableU; do ?[apply: mf|apply: mg]. apply/predeqP=> x; rewrite /preimage/= /adde_def !(negb_and, negb_or). by rewrite !(rwP2 eqP idP) !(rwP2 negP idP) !(rwP2 orP idP) !(rwP2 andP idP). wlog fg : D mD mf mg mfg / forall x, D x -> f x +? g x => [hwlogD|]; 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)) => //. by move=> n; apply/EFin_measurable_fun/measurable_funTS/measurable_funD. move=> x Dx; under eq_fun do rewrite EFinD. exact: cvgeD (fg _ _) (f_cvg _ _) (g_cvg _ _). move=> A mA; wlog NAnoo: A mD mf mg mA / ~ (A -oo) => [hwlogA|]. have [] := pselect (A -oo); last exact: hwlogA. move=> /(@setD1K _ -oo)<-; rewrite preimage_setU setIUr. apply: measurableU; last by apply: hwlogA=> //; [exact: measurableD|case=>/=]. have -> : (f \+ g) @^-1` [set -oo] = f @^-1` [set -oo] `|` g @^-1` [set -oo]. apply/seteqP; split=> x /= => [/eqP|[]]; rewrite /preimage/=. - by rewrite adde_eq_ninfty => /orP[] /eqP->; [left|right]. - by move->. - by move->; rewrite addeC. by rewrite setIUr; apply: measurableU; [apply: mf|apply: mg]. have-> : D `&` (f \+ g) @^-1` A = (D `&` [set x | f x +? g x]) `&` (f \+ g) @^-1` A. rewrite -setIA; congr (_ `&` _). apply/seteqP; split=> x; rewrite /preimage/=; last by case. move=> Afgx; split=> //. by case: (f x) (g x) Afgx => [rf||] [rg||]. have Dfg : D `&` [set x | f x +? g x] `<=` D by apply: subIset; left. apply: hwlogD => //. - 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