proposition: Lemma counting_dirac (A : set nat) : counting A = \sum_(n <oo) \d_ n A :> \bar R.
proof: Proof. have -> : \sum_(n <oo) \d_ n A = \esum_(i in A) \d_ i A :> \bar R. rewrite nneseries_esum// (_ : [set _ | _] = setT); last exact/seteqP. rewrite [in LHS](esumID A)// !setTI [X in _ + X](_ : _ = 0) ?adde0//. by apply: esum1 => i Ai; rewrite /= /dirac indicE memNset. rewrite /counting/=; case: ifPn => /asboolP finA. by rewrite -finite_card_dirac. by rewrite infinite_card_dirac. 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