proposition: Lemma summable_integral_dirac (a : nat -> \bar R) : summable setT a -> \sum_(n <oo) `|\int[\d_ n]_x a x| < +oo.
proof: Proof. move=> sa. apply: (@le_lt_trans _ _ (\sum_(i <oo) `|fine (a i)|%:E)). apply: lee_nneseries => // n _; rewrite integral_dirac//. move: (@summable_pinfty _ _ _ _ sa n Logic.I). by case: (a n) => //= r _; rewrite indicE/= mem_set// mul1r. move: (sa); rewrite /summable -fun_true -nneseries_esum//; apply: le_lt_trans. by apply lee_nneseries => // n _ /=; case: (a n) => //; rewrite leey. 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