proposition: Lemma ConvnDr n (p : {prob R}) (x : T) (g : 'I_n -> T) (d : {fdist 'I_n}) : x <|p|> <|>_d g = <|>_d (fun i => x <|p|> g i).
proof: Proof. elim: n p x g d => [? ? ? d|n IHn p x g d]; first by move/fdistI0_False: (d). have [d01|d0n1] := eqVneq (d ord0) 1%coqR. by rewrite (Convn_proj g d01) (Convn_proj (fun i => x <|p|> g i) d01). by rewrite !ConvnIE !IHn; congr (<|>_ _ _); apply funext=> i; rewrite convDr. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist