proposition: Lemma locally_integrableN D f : locally_integrable D f -> locally_integrable D (\- f)%R.
proof: Proof. move=> [mf oD foo]; split => //; first exact: measurableT_comp. by move=> K KD cK; under eq_integral do rewrite normrN; exact: foo. 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