Helper

PrX_fstRV

Section proba_extra

Type Lemma

Proof Lines 17

Lemma PrX_fstRV (A B T : finType) (P : R.-fdist T) (X : {RV P -> A}) (Y : {RV P -> B}) (x : A) : \sum_(y : B) `Pr[[% X, Y] = (x, y)] = `Pr[X = x].

Marginalization: summing joint probabilities over Y yields marginal of X. Σ_y Pr[(X,Y) = (x,y)] = Pr[X = x]. Fundamental for deriving marginals.

This lemma does not use any other lemmas from the stats.

No lemmas in the stats use this lemma.

Loading source code...