proposition: Lemma S1_Convn_proj n (g : 'I_n -> T) d : S1 (prj (<|>_d g)) = \ssum_(i < n) scalept (d i) (S1 (prj (g i))).
proof: Proof. elim: n g d => [|n IH] g d. by move: (FDist.f1 d); rewrite /= big_ord0 => /Rlt_not_eq; case. rewrite /=; case: Bool.bool_dec => [/eqP|/Bool.eq_true_not_negb]Hd. rewrite (bigD1 ord0) //= Hd big1 /=. rewrite addpt0 (@scalept_gt0 _ 1). by congr (_ *: _); apply val_inj; rewrite /= mulR1. move=> i Hi; have := FDist.f1 d. rewrite (bigD1 ord0) ?inE // Hd /= -RplusE addRC => /(f_equal (Rminus^~ R1)). rewrite addRK subRR => /eqP. rewrite psumr_eq0// => /allP/= => /(_ i). by rewrite mem_index_enum Hi implyTb => /(_ isT)/eqP ->; rewrite scale0pt. set d' := fdist_del Hd. set g' := fun i => g (fdist_del_idx ord0 i). rewrite /index_enum -enumT (bigD1_seq ord0) ?enum_uniq ?mem_enum //=. rewrite -big_filter (perm_big (map (lift ord0) (enum 'I_n))); last first. exact: perm_filter_enum_ord. rewrite 2!affine_conv/=; congr addpt. rewrite IH -barycenter_map scalept_barycenter //. rewrite /barycenter 2!big_map [in RHS]big_map. apply eq_bigr => i _. rewrite scaleptA // fdist_delE fdistD1E /=. rewrite (mulrC (fun_of_fin (FDist.f d) (lift ord0 i))). rewrite RmultE mulrA mulrV ?mul1r //. move: (Hd); apply contra; rewrite R0E R1E => /eqP Hd'. by rewrite -onem0 -Hd' onemK. 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