proposition: Lemma intersection : P |= X _|_ Y | [% Z, W] -> P |= X _|_ W | [% Z, Y] -> P |= X _|_ [% Y, W] | Z.
proof: Proof. move=> H1 H2. suff : P |= X _|_ Y | Z by apply contraction. move=> a b c; apply/esym. rewrite -[in X in X * _ = _]cpr_eq_set1 [in X in X * _ = _](creasoning_by_cases _ W). under eq_bigr do rewrite setX1. under eq_bigr do rewrite cpr_eq_set1. rewrite big_distrl /=. have <- : \sum_(d <- fin_img W) `Pr[ [% X, Y] = (a, b) | Z = c] * `Pr[ W = d | Z = c] = \sum_(d <- fin_img W) `Pr[ [% X, W] = (a, d) | Z = c] * `Pr[ Y = b | Z = c]. suff H : forall d, `Pr[ [% X, Y] = (a, b) | Z = c] / `Pr[ Y = b | Z = c ] = `Pr[ [% X, W] = (a, d) | Z = c] / `Pr[ W = d | Z = c ]. apply eq_bigr => d _. rewrite -eqR_divr_mulr; last first. rewrite cpr_eqE divR_neq0' //. - by move: (P0 b c d); apply: contra => /eqP/(pr_eq_domin_RV2 W d) ->. - move: (P0 b c d); apply: contra => /eqP/(pr_eq_domin_RV2 [% Y, W] (b, d)). by rewrite pr_eq_pairCA pr_eq_pairA => ->. rewrite {1}/Rdiv mulRAC -/(Rdiv _ _) (H d) mulRAC eqR_divr_mulr //. rewrite cpr_eqE divR_neq0' //. - move: (P0 b c d); apply: contra => /eqP/(pr_eq_domin_RV2 Y b). by rewrite pr_eq_pairC pr_eq_pairA pr_eq_pairAC => ->. - move: (P0 b c d); apply: contra => /eqP/(pr_eq_domin_RV2 [% Y, W] (b, d)). by rewrite pr_eq_pairCA -pr_eq_pairA => ->. suff H : forall d, `Pr[ X = a | [% Y, Z] = (b, c)] = `Pr[ X = a | [% W, Z] = (d, c)]. move=> d. rewrite cpr_eq_product_rule (H d). rewrite [in RHS]cpr_eq_product_rule. rewrite {1}/Rdiv -mulRA mulRV; last first. rewrite cpr_eqE divR_neq0' //. - by move: (P0 b c d); apply: contra => /eqP/(pr_eq_domin_RV2 W d) ->. - move: (P0 b c d); apply: contra => /eqP/(pr_eq_domin_RV2 [% Y, W] (b, d)). by rewrite pr_eq_pairCA -pr_eq_pairA => ->. rewrite {1}/Rdiv -[in RHS]mulRA mulRV // cpr_eqE divR_neq0' //. - move: (P0 b c d); apply: contra => /eqP/(pr_eq_domin_RV2 Y b). by rewrite pr_eq_pairC pr_eq_pairA pr_eq_pairAC => ->. - move: (P0 b c d); apply: contra => /eqP/(pr_eq_domin_RV2 [% Y, W] (b, d)). by rewrite pr_eq_pairCA -pr_eq_pairA => ->. have {}H2 : forall d, `Pr[ X = a | [% Y, Z] = (b, c)] = `Pr[ X = a | [% W, Z, Y] = (d, c, b)]. move=> d; move: {H2}(H2 a d (c, b)). rewrite cpr_eq_product_rule. have /eqP H0 : `Pr[ W = d | [% Z, Y] = (c, b)] != 0. rewrite cpr_eqE pr_eq_pairA pr_eq_pairAC -pr_eq_pairA. rewrite pr_eq_pairC divR_neq0' //; first by rewrite pr_eq_pairC. by move: (P0 b c d); apply: contra => /eqP/(pr_eq_domin_RV2 W d) ->. move/eqR_mul2r => /(_ H0){H0}/esym. by rewrite [in LHS]cpr_eq_pairCr cpr_eq_pairAr. have {}H1 : forall d, `Pr[ X = a | [% W, Z] = (d, c)] = `Pr[ X = a | [% Y, W, Z] = (b, d, c)]. move=> d; move: {H1}(H1 a b (c, d)). rewrite cpr_eq_product_rule. have /eqP H0 : `Pr[ Y = b | [% Z, W] = (c, d)] != 0. rewrite cpr_eqE pr_eq_pairA divR_neq0' //. move: (P0 b c d); apply: contra => /eqP/(pr_eq_domin_RV2 Y b). by rewrite pr_eq_pairC -pr_eq_pairA => ->. move/eqR_mul2r => /(_ H0){H0}/esym. by rewrite [in LHS]cpr_eq_pairCr cpr_eq_pairAr cpr_eq_pairACr. by move=> d; rewrite {H2}(H2 d) {}H1 cpr_eq_pairCr cpr_eq_pairAr. rewrite -big_distrr /=. rewrite cPr_1 ?mulR1 //. move: (P0 b c D_not_empty); apply: contra. rewrite pr_eq_pairAC => /eqP/(pr_eq_domin_RV2 [% Y, W] (b, D_not_empty)). by rewrite 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