proposition: Lemma dE j : fdistmap K e i != 0%coqR -> d j = (e j * (i == K j)%:R / \sum_(j | K j == i) e j)%coqR.
proof: Proof. rewrite -denE => NE. rewrite jfdist_condE // {NE} /jcPr /proba.Pr. rewrite (big_pred1 (j,i)); last first. by move=> k; rewrite !inE [in RHS](surjective_pairing k) xpair_eqE. rewrite (big_pred1 i); last by move=> k; rewrite !inE. rewrite !fdistE big_mkcond [in RHS]big_mkcond /=. rewrite -RmultE -INRE. congr (_ / _)%R. under eq_bigr => k do rewrite {2}(surjective_pairing k). rewrite -(pair_bigA _ (fun k l => if l == i then e `X (fun j0 : 'I_m => fdist1 (K j0)) (k, l) else R0))%R /=. apply eq_bigr => k _. rewrite -big_mkcond /= big_pred1_eq !fdistE /= eq_sym. by case: ifP; rewrite (mulr1,mulr0). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets) Reals mathcomp(Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext ssralg_ext fdist jfdist_cond fsdist convex