proposition: Lemma cinde_events_cPr1 (i : 'I_n) : let vals := set_vals C (set_vals A (set_vals B vals0)) in (forall x : 'I_n, x \in e -> vals x = set_vals A vals0 x) -> i \in e -> i \in f -> i \notin g -> set_vals A vals0 i <> set_vals B vals0 i -> `Pr_P[(preim_vars (e :&: f) vals) | (preim_vars g vals)] = 1 -> cinde_events P [set x | preim (prod_vars e) (pred1 A) x] [set x | preim (prod_vars f) (pred1 B) x] [set x | preim (prod_vars g) (pred1 C) x].
proof: Proof. move=> vals He Hie Hif Hig Hvi. rewrite /cinde_events /cPr. set den := (X in _ / X). case/boolP: (den == 0) => [/eqP|] Hden. by rewrite setIC Pr_domin_setI // ?div0R => /esym/R1_neq_R0. set num := Pr _ _ => Hnum. have {}Hnum : num = den. by rewrite -[RHS]mul1R -Hnum /Rdiv -mulRA mulVR // mulR1. rewrite -Hnum in Hden. rewrite (proj2 (Pr_set0P _ _)); last first. move=> u; rewrite !inE => /andP[] /andP[] /eqP HA /eqP HB. by rewrite -HA -HB !set_vals_prod_vars in Hvi. suff : `Pr_P[finset (prod_vars f @^-1 B) | finset (prod_vars g @^-1 C)] = 0. by rewrite /cPr => ->; rewrite mulR0 div0R. apply/cPr_eq0/Pr_set0P => u. rewrite !inE => /andP [] /eqP HB /eqP HC. move: Hnum; rewrite /den. have -> : g = (e :&: f :|: g) :\: ((e :&: f) :\: g). by apply/setP => j; cases_in j. rewrite Pr_preim_vars_sub; last by apply/subsetP => j; cases_in j. have : prod_vals ((e :&: f) :\: g) vals \in fin_img (prod_vars ((e :&: f) :\: g)). case/boolP: (_ \in _) => // /negP HA. elim: (negP Hden); rewrite /num -preim_vars_inter. have -> : e :&: f :|: g = (e :&: f :\: g) :|: g. apply/setP => k; by cases_in k. apply/eqP/Pr_set0P => v. rewrite preim_vars_inter inE => /andP [/preim_varsP /= HA']. elim: HA; apply/fin_imgP. exists v; apply/ffunP => k. apply/prod_vals_eq => /HA' <-. by rewrite ffunE. case/fin_imgP => v Hv {Hden}. set a := map_fin_img (prod_vars ((e :&: f) :\: g)) v. rewrite (bigD1 a) //= nth_fin_imgK -Hv. rewrite /num (@preim_vars_vals _ (prod_vals (e :&: f :|: g) vals) _ vals); last by move=> j; rewrite set_vals_prod_vals_id. rewrite -preim_vars_inter addRC => /subR_eq; rewrite subRR => /esym Hnum. have : Pr P (preim_vars (e :&: f :|: g) (set_vals (prod_vals (e :&: f :\: g) (set_vals B vals)) vals)) = 0. rewrite (_ : prod_vals _ _ = prod_vars (e :&: f :\: g) u); last first. apply/ffunP => k; apply/prod_vals_eq => Hk. rewrite -HB set_vals_prod_vars ?ffunE //. move: Hk; cases_in k. rewrite -(@nth_fin_imgK U). move/psumr_eq0P: Hnum; apply; first by move => *; exact/RleP. apply/eqP => /(f_equal (fun x => nth_fin_img x)). rewrite !nth_fin_imgK => /(prod_types_app i) /prod_vals_eqP Hi. elim: Hvi; rewrite -He //. have iefg : i \in e :&: f :\: g by move: Hif Hig Hie; cases_in i. move/(prod_types_app i)/prod_vals_eqP: Hv => -> //. by rewrite -HB set_vals_prod_vars // -Hi // ffunE. move/Pr_set0P; apply. apply/preim_varsP => j Hj. case/boolP: (j \in g) => jg. by rewrite set_vals_tl ?inE ?jg // /vals -HC set_vals_prod_vars. rewrite inE (negbTE jg) orbF in Hj. rewrite -HB set_vals_prod_vals ?set_vals_prod_vars //. move: Hj; by rewrite inE => /andP[]. by rewrite inE Hj jg. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba