proposition: Lemma infinite_card_dirac (A : set T) : infinite_set A -> \esum_(i in A) \d_ i A = +oo :> \bar R.
proof: Proof. move=> infA; apply/eqyP => r r0. have [B BA Br] := infinite_set_fset `|ceil r| infA. apply: esum_ge; exists [set` B] => //; apply: (@le_trans _ _ `|ceil r|%:R%:E). by rewrite lee_fin natr_absz gtr0_norm ?ceil_gt0// ceil_ge. move: Br; rewrite -(@ler_nat R) -lee_fin => /le_trans; apply. rewrite (eq_fsbigr (cst 1))/=; last first. by move=> i /[!inE] /BA /mem_set iA; rewrite diracE iA. by rewrite fsbig_finite//= card_fset_sum1 sumEFin natr_sum// set_fsetK. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)