proposition: Lemma hullX (F : convType) (C : set E) (D : set F) : hull (C `*` D) = hull C `*` hull D.
proof: Proof. rewrite eqEsubset; split. move=>+ [n][g][d][gCD]-> =>_. rewrite Convn_pair; split=>/=; exists n; [exists (fst \o g) | exists (snd \o g)]; exists d; split=> // + [i] _ <- =>_ /=; (suff: ((C `*` D) (g i)) by move=>[]); by apply gCD; exists i. move=>[+ +][]/=[n][g][d][gC->][m][f][e][fD->]=>_ _. exists (n * m)%N, (fun i=> let (i, j) := split_prod i in (g i, f j)), (fdistmap (unsplit_prod (n:=m)) (d `x e)%fdist); split. move=>+ [i] _ <- =>_. by case: (split_prod i)=>a b; split; [apply gC | apply fD]. rewrite Convn_pair/comp/=; congr pair; apply S1_inj; rewrite !S1_Convn big_prod_ord/=. apply eq_big => // i _. rewrite -(scale1pt (scalept _ _)) scaleptA// -(FDist.f1 e). move: (@mulr_suml R_ringType _ (index_enum [finType of 'I_m]) (mem 'I_m) (fun i => nneg_ff e i) (nneg_ff d i)); rewrite -RmultE => ->. simple refine (let h : nneg_fun 'I_m := _ in _). exists (fun j => nneg_ff e j * nneg_ff d i)%coqR=>j. exact: ssrR.mulR_ge0. have -> : (\sum_(j in 'I_m) (nneg_ff e j) * (nneg_ff d i) = \sum_(i in 'I_m) nneg_f h i)%coqR. by apply eq_big => // j _; rewrite fdist_prodE. rewrite scalept_sum; apply eq_big=>// j _. rewrite /h /= fdistmapE. have -> : (\sum_(a in [finType of 'I_n * 'I_m] | a \in preim (@unsplit_prod _ m) (pred1 (Ordinal (unsplit_prodp i j)))) nneg_ff (fdist_prod d (fun=> e)) a = \sum_(a in [finType of 'I_n * 'I_m] | a \in pred1 (i, j)) nneg_ff (fdist_prod d (fun=> e)) a)%coqR. apply eq_big=>// k; congr andb; rewrite 3!inE. by apply: (eqtype.inj_eq _ k (i, j)); exact: (can_inj (@unsplit_prodK _ _)). rewrite (big_pred1 (i, j))// fdist_prodE/= ssrR.mulRC; congr (scalept _ (S1 (g _))). by move: (unsplit_prodK (i, j)) => /(congr1 fst)/esym. rewrite (exchange_big_dep xpredT)//=; apply: eq_bigr => j _. rewrite -(scale1pt (scalept _ _)) scaleptA// -(FDist.f1 d). move: (@mulr_suml R_ringType _ (index_enum [finType of 'I_n]) (mem 'I_n) (fun i=> nneg_ff d i) (nneg_ff e j)); rewrite -RmultE => ->. simple refine (let h : nneg_fun 'I_n := _ in _). exists (fun i=> nneg_ff d i * nneg_ff e j)%coqR => i. exact: ssrR.mulR_ge0. have -> : (\sum_(i in 'I_n) nneg_ff d i * nneg_ff e j = \sum_(i in 'I_n) nneg_f h i)%coqR. by apply eq_big=>// i _; rewrite fdist_prodE. rewrite scalept_sum; apply: eq_big => // i _. rewrite /h/= fdistmapE. have -> : (\sum_(a in [finType of 'I_n * 'I_m] | a \in preim (unsplit_prod (n:=m)) (pred1 (Ordinal (unsplit_prodp i j)))) nneg_ff (fdist_prod d (fun=> e)) a = \sum_(a in [finType of 'I_n * 'I_m] | a \in pred1 (i, j)) nneg_ff (FDist.f (fdist_prod d (fun=> e))) a)%coqR. apply: eq_big=>// k; congr andb; rewrite 3!inE. by apply: (eqtype.inj_eq _ k (i, j)); exact (can_inj (@unsplit_prodK _ _)). rewrite (big_pred1 (i, j))// fdist_prodE/= ssrR.mulRC; congr (scalept _ (S1 (f _))). by move:(unsplit_prodK (i, j))=>/(congr1 snd)/esym. Qed.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets boolp Rstruct) infotheo(convex Reals_ext) preliminaries Reals