proposition: Lemma cinde_preim_ok1 (i j k : 'I_n) : cinde_preim [set i] [set j] [set k] <-> P |= (vars i) _|_ (vars j) | (vars k).
proof: Proof. rewrite /cinde_preim /preim_vars. split. - move=> Hpreim. apply/cinde_rv_events => a b c. set vals := set_val a (set_val c (set_val b vals0)). have vi : vals i = a by rewrite /vals set_val_hd. move: (erefl vals) {Hpreim} (Hpreim vals). rewrite {2}/vals /cinde_events; clearbody vals. rewrite !big_set1. wlog: c / vals k = c. case: (ord_eq_dec i k) c vi. move=> <- {k} c vi. case ac: (a == c). rewrite -(eqP ac); exact. move=> _ _ _. rewrite (proj2 (cPr_eq0 _ _ _)); last first. apply/Pr_set0P => u. by rewrite !inE => /andP [] /andP [] /= /eqP ->; rewrite ac. rewrite (proj2 (cPr_eq0 _ _ _)); last first. apply/Pr_set0P => u. by rewrite !inE => /andP [] /= /eqP ->; rewrite ac. by rewrite mul0R. move=> nik c vi HG Hvals; apply: HG => //. by rewrite Hvals set_val_tl // set_val_hd. move=> vk. wlog: b / vals j = b. case: (ord_eq_dec i j) b. move=> <- {j} b. case ab: (a == b). rewrite -(eqP ab); exact. move=> _ _. rewrite setIid vi vk. set x := (X in X = X * X). move/Rxx2 => [] Hx. rewrite -/x Hx. rewrite (proj2 (cPr_eq0 _ _ _)) ?mul0R //. apply/Pr_set0P => u. by rewrite !inE => /andP [] /andP [] /= /eqP ->; rewrite ab. rewrite /cPr. set den := (X in _ / X). case/boolP: (den == 0) => /eqP Hden. by rewrite setIC Pr_domin_setI // setIC Pr_domin_setI // !div0R mul0R. set num := (X in _ * (X / _)). case/boolP: (num == 0) => /eqP Hnum. by rewrite -setIA setIC Pr_domin_setI // Hnum !div0R mulR0. elim Hnum. apply/Pr_set0P => u. rewrite !inE => /andP [] /= Hi Hk. move: Hx; subst x. move/(f_equal (Rmult ^~ den)). move/eqP in Hden. rewrite /cPr /Rdiv -mulRA mulVR // mulR1 mul1R. move/(f_equal (Rminus den)). rewrite subRR setIC -Pr_diff => /Pr_set0P/(_ u). rewrite !inE (eqP Hi) Hk eq_sym ab; exact. case: (ord_eq_dec k j). move=> <- {j} ik b. case bc: (b == c). rewrite (eqP bc); exact. move=> _ _ _. rewrite (proj2 (cPr_eq0 _ _ _)); last first. apply/Pr_set0P => u. by rewrite !inE => /andP [] /andP [] _ /= /eqP ->; rewrite bc. rewrite mulRC (proj2 (cPr_eq0 _ _ _)) ?mul0R //. by apply/Pr_set0P => u; rewrite !inE => /andP [] /= /eqP ->; rewrite bc. move=> nkj nij b HG Hvals; apply: HG => //. by rewrite Hvals set_val_tl // set_val_tl // set_val_hd. by rewrite vi vk => -> _. - move=> Hdrv vals. move/cinde_rv_events/(_ (vals i) (vals j) (vals k)): Hdrv. by rewrite !big_set1. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba