Helper

marginal_swap_YZ

Section perm_extra

Type Lemma

Proof Lines 4

Lemma marginal_swap_YZ (V W : finType) (Y : {RV P -> V}) (Z : {RV P -> W}) : forall y : V, (`p_[% Z, Y])`2 y = (`p_[% Y, Z])`1 y.

Marginal equivalence under swap: the 2nd marginal of (Z,Y) equals the 1st marginal of (Y,Z). Both give the distribution of Y.

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

No lemmas in the stats use this lemma.

Loading source code...