proposition: Lemma affine_map_scaled : affine map_scaled.
proof: Proof. move=> p [q x|] [r y|] /=; rewrite 2!convptE ?scalept0 //. - rewrite !(scalept_Scaled (Prob.p p)) !(scalept_Scaled (Prob.p p).~) /= /scalept /=. case: Rlt_dec => Hpq; case: Rlt_dec => Hpr //=; congr (_ *: _). by rewrite affine_conv. - by rewrite !addpt0 !(scalept_Scaled (Prob.p p)) /= /scalept /=; case: Rlt_dec. - by rewrite !add0pt !(scalept_Scaled (Prob.p p).~) /= /scalept/=; case: Rlt_dec. 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