proposition: Lemma dK n m K (e : {fdist 'I_m}) j : e j = (\sum_(i < n) fdistmap K e i * d K e i j)%R.
proof: Proof. under eq_bigr => /= a _. have [Ka0|Ka0] := eqVneq (fdistmap K e a) 0%R. rewrite Ka0 mul0R. have <- : (e j * (a == K j)%:R = 0)%R. have [/eqP Kj|] := eqVneq a (K j); last by rewrite mulR0. move: Ka0; rewrite fdistE /=. by move/psumr_eq0P => -> //; rewrite ?(mul0R,inE) // eq_sym. over. rewrite FDistPart.dE // fdistE /= mulRCA mulRV ?mulR1; last by rewrite fdistE in Ka0. over. move=> /=. rewrite (bigD1 (K j)) //= eqxx mulR1. by rewrite big1 ?addR0 // => i /negbTE ->; rewrite 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