proposition: Lemma distribution_dRV A : measurable A -> distribution P X A = \sum_(k <oo) enum_prob X k * \d_ (dRV_enum X k) A.
proof: Proof. move=> mA; rewrite /distribution /pushforward. have mAX i : dRV_dom X i -> measurable (X @^-1` (A `&` [set dRV_enum X i])). move=> _; rewrite preimage_setI; apply: measurableI => //. exact/measurable_sfunP. have tAX : trivIset (dRV_dom X) (fun k => X @^-1` (A `&` [set dRV_enum X k])). under eq_fun do rewrite preimage_setI; rewrite -/(trivIset _ _). apply: trivIset_setIl; apply/trivIsetP => i j iX jX /eqP ij. rewrite -preimage_setI (_ : _ `&` _ = set0)//. by apply/seteqP; split => //= x [] -> {x} /inj; rewrite inE inE => /(_ iX jX). have := measure_bigcup P _ (fun k => X @^-1` (A `&` [set dRV_enum X k])) mAX tAX. rewrite -preimage_bigcup => {mAX tAX}PXU. rewrite -{1}(setIT A) -(setUv (\bigcup_(i in dRV_dom X) [set dRV_enum X i])). rewrite setIUr preimage_setU measureU; last 3 first. - rewrite preimage_setI; apply: measurableI => //. exact: measurable_sfunP. by apply: measurable_sfunP; exact: bigcup_measurable. - apply: measurable_sfunP; apply: measurableI => //. by apply: measurableC; exact: bigcup_measurable. - rewrite 2!preimage_setI setIACA -!setIA -preimage_setI. by rewrite setICr preimage_set0 2!setI0. rewrite [X in _ + X = _](_ : _ = 0) ?adde0; last first. rewrite (_ : _ @^-1` _ = set0) ?measure0//; apply/disjoints_subset => x AXx. rewrite setCK /bigcup /=; exists ((dRV_enum X)^-1 (X x))%function. exact: funS. by rewrite invK// inE. rewrite setI_bigcupr; etransitivity; first exact: PXU. rewrite eseries_mkcond; apply: eq_eseriesr => k _. rewrite /enum_prob patchE; case: ifPn => nX; rewrite ?mul0e//. rewrite diracE; have [kA|] := boolP (_ \in A). by rewrite mule1 setIidr// => _ /= ->; exact: set_mem. rewrite notin_set => kA. rewrite mule0 (disjoints_subset _ _).2 ?preimage_set0 ?measure0//. by apply: subsetCr; rewrite sub1set inE. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) HB(structures) exp numfun lebesgue_measure lebesgue_integral reals ereal signed topology normedtype sequences esum measure exp numfun lebesgue_measure lebesgue_integral