Helper

jproduct_ruleRV

File dumas2017dual/lib/extra_proba.v

Section proba_extra

Type Lemma

Proof Lines 10

Signature

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

Description

Joint probability product rule: Pr[(X,Y) = (x,y)] = Pr[Y=y] * Pr[X=x|Y=y]. This is Bayes' theorem in product form, fundamental for decomposing joint distributions into marginal × conditional.

Uses (0)

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

Used By (0)

No lemmas in the stats use this lemma.

Coq Source Code

View on GitHub

Loading source code...

← Back to Stats