proposition: Lemma integralD : \int[mu]_(x in D) (f1 x + f2 x) = \int[mu]_(x in D) f1 x + \int[mu]_(x in D) f2 x.
proof: Proof. pose A := D `&` [set x | f1 x \is a fin_num]. pose B := D `&` [set x | f2 x \is a fin_num]. have mA : measurable A by exact: emeasurable_fin_num. have mB : measurable B by exact: emeasurable_fin_num. have mAB : measurable (A `&` B) by apply: measurableI. pose g1 := (fine \o f1 \_ (A `&` B))%R. pose g2 := (fine \o f2 \_ (A `&` B))%R. have ig1 : mu.-integrable D (EFin \o g1). rewrite (_ : _ \o _ = f1 \_ (A `&` B)) //. apply: (integrableS measurableT)=>//; apply/(integrable_mkcond _ _).1 => //. by apply: integrableS if1=>//; rewrite -setIAC -setIA; apply: subIset; left. rewrite /g1 funeqE => x //=; rewrite !/restrict; case: ifPn => //. rewrite 2!in_setI => /andP[/andP[xA f1xfin] _] /=. by rewrite fineK//; rewrite inE in f1xfin. have mg1 := measurable_int ig1. have ig2 : mu.-integrable D (EFin \o g2). rewrite (_ : _ \o _ = f2 \_ (A `&` B)) //. apply: (integrableS measurableT)=>//; apply/(integrable_mkcond _ _).1 => //. by apply: integrableS if2=>//; rewrite -setIAC -setIA; apply: subIset; left. rewrite /g2 funeqE => x //=; rewrite !/restrict; case: ifPn => //. rewrite in_setI => /andP[_]; rewrite in_setI => /andP[xB f2xfin] /=. by rewrite fineK//; rewrite inE in f2xfin. have mg2 := measurable_int ig2. transitivity (\int[mu]_(x in D) (EFin \o (g1 \+ g2)%R) x). apply: ae_eq_integral => //. - exact: emeasurable_funD. - rewrite (_ : _ \o _ = (EFin \o g1) \+ (EFin \o g2))//. exact: emeasurable_funD. - apply: (filterS2 _ _ (integrable_ae mD if1) (integrable_ae mD if2)). move=> x + + Dx => /(_ Dx) f1fin /(_ Dx) f2fin /=. rewrite EFinD /g1 /g2 /restrict /=; have [|] := boolP (x \in A `&` B). by rewrite in_setI => /andP[xA xB] /=; rewrite !fineK. by rewrite in_setI negb_and => /orP[|]; rewrite in_setI negb_and /= (mem_set Dx)/= notin_set/=. - rewrite (_ : _ \o _ = (EFin \o g1) \+ (EFin \o g2))// integralD_EFin//. congr (_ + _); apply: ae_eq_integral => //. + apply: (filterS2 _ _ (integrable_ae mD if1) (integrable_ae mD if2)). move=> x + + Dx => /(_ Dx) f1fin /(_ Dx) f2fin /=; rewrite /g1 /restrict /=. have [/=|] := boolP (x \in A `&` B); first by rewrite fineK. by rewrite in_setI negb_and => /orP[|]; rewrite in_setI negb_and /= (mem_set Dx) /= notin_set/=. + apply: (filterS2 _ _ (integrable_ae mD if1) (integrable_ae mD if2)). move=> x + + Dx => /(_ Dx) f1fin /(_ Dx) f2fin /=; rewrite /g2 /restrict /=. have [/=|] := boolP (x \in A `&` B); first by rewrite fineK. by rewrite in_setI negb_and => /orP[|]; rewrite in_setI negb_and /= (mem_set Dx) /= notin_set. 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