proposition: Lemma integral_dirac (f : T -> \bar R) (mf : measurable_fun D f) : \int[\d_ a]_(x in D) f x = \d_a D * f a.
proof: Proof. have [/[!inE] aD|aD] := boolP (a \in D). rewrite integralE ge0_integral_dirac//; last exact/measurable_funepos. rewrite ge0_integral_dirac//; last exact/measurable_funeneg. by rewrite [in RHS](funeposneg f) diracE mem_set// mul1e. rewrite diracE (negbTE aD) mul0e -(integral_measure_zero D f)//. apply: eq_measure_integral => //= S mS DS; rewrite /dirac indicE memNset//. by move=> /DS/mem_set; exact/negP. 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