proposition: Lemma weak_union : P |= X _|_ [% Y, W] | Z -> P |= X _|_ Y | [% Z, W].
proof: Proof. move=> H a b [c d]. transitivity (`Pr[ X = a | [% Y, Z, W] = (b, c, d)] * `Pr[ Y = b | [% Z, W] = (c, d)]). by rewrite cpr_eq_product_rule cpr_eq_pairAr. transitivity (`Pr[ X = a | Z = c] * `Pr[ Y = b | [% Z, W] = (c, d)]). rewrite cpr_eq_pairACr. case/boolP : (`Pr[ [% Y, W, Z] = (b, d, c)] == 0) => [/eqP|] H0. - by rewrite [X in _ * X = _ * X]cpr_eqE pr_eq_pairA pr_eq_pairAC H0 div0R !mulR0. - by rewrite (cinde_alt _ H). case/boolP : (`Pr[ [% Z, W] = (c, d) ] == 0) => [/eqP|] ?. - by rewrite [X in _ * X = _ * X]cpr_eqE (pr_eq_pairC _ Y) (pr_eq_domin_RV2 Y) ?(div0R,mulR0). - have {}H : P |= X _|_ W | Z by move/cinde_drv_2C : H; apply decomposition. by rewrite [in X in _ = X * _]cpr_eq_pairCr (cinde_alt _ H) // pr_eq_pairC. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals mathcomp(Rstruct) ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba jfdist_cond