proposition: Lemma locally_integrableD D f g : locally_integrable D f -> locally_integrable D g -> locally_integrable D (f \+ g)%R.
proof: Proof. move=> [mf oD foo] [mg _ goo]; split => //; first exact: measurable_funD. move=> K KD cK. suff : lebesgue_measure.-integrable K ((EFin \o f) \+ (EFin \o g)). by case/integrableP. apply: integrableD => //=; first exact: compact_measurable. - apply/integrableP; split; last exact: foo. apply/EFin_measurable_fun; apply: measurable_funS mf => //. exact: open_measurable. - apply/integrableP; split; last exact: goo. apply/EFin_measurable_fun; apply: measurable_funS mg => //. exact: open_measurable. 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