proposition: Lemma caratheodory (A : set (Vector.lmodType E)) x : x \in hull A -> exists (n : nat) (g : 'I_n -> Vector.lmodType E) (d : {fdist 'I_n}), [/\ (n <= (dimv (@fullv R_fieldType E)).+1)%nat, range g `<=` A & x = <|>_d g].
proof: Proof. move=> /set_mem[n [g [d [gA ->]]]]. elim: n => [|n IHn] in g d gA *; first by case: (fdistI0_False d). have [nsgt|nsgt] := leqP n (dimv (@fullv R_fieldType E)). by exists n.+1, g, d. have [mu [muR muE [i mui]]] : exists mu : 'I_n.+1 -> R, [/\ \sum_(i < n.+1) mu i = 0, \sum_(i < n.+1) (mu i) *: g i = 0 & exists i, mu i != 0 ]. rewrite {IHn}. have [sf|/freeN_combination[mu [musum [i mui]]]] := boolP (free [tuple g (lift ord0 i) - g ord0 | i < n]). have : basis_of fullv [tuple g (lift ord0 i) - g ord0 | i < n]. by rewrite basisEfree size_tuple (ltnW nsgt) andbT sf subvf. rewrite in_tupleE basisEdim size_map => /andP[_]. by move=> /leq_ltn_trans => /(_ _ nsgt); rewrite size_tuple ltnn. exists (fun i => if i is @Ordinal _ i.+1 ilt then mu (Ordinal (ltnSE ilt)) else - \sum_i mu i); split. - rewrite big_ord_recl /= addrC; apply/eqP; rewrite subr_eq0; apply/eqP. by apply: eq_bigr => j _; congr mu; exact/val_inj. - rewrite big_ord_recl /= scaleNr addrC scaler_suml -sumrB -{2}musum. apply: eq_bigr => j _; rewrite (nth_map j) ?size_tuple//. rewrite scalerBr; congr (mu _ *: g _ - _); apply/val_inj => //=. by rewrite nth_ord_enum. - by exists (lift ord0 i) => /=; rewrite (_ : Ordinal _ = i)//; exact/val_inj. wlog: mu muR muE mui / mu i > 0. move=> H. have [mui0|mui0] := ltP 0%coqR (mu i); first exact: (H mu). apply (H (fun i => - mu i)). - by rewrite sumrN muR oppr0. - by under eq_bigr do rewrite scaleNr; rewrite sumrN muE oppr0. + by rewrite oppr_eq0. + by rewrite oppr_gt0 lt_neqAle mui. move=>/(@arg_minP _ _ _ i (fun i => 0 < mu i) (fun i => d i / mu i)) [im muip muim] {i mui}. wlog: g d gA mu muR muE im muip muim / (im == ord0)%N. set f := fun i : nat => if i == im :> nat then 0%nat else if i == 0%nat then nat_of_ord im else i. have fcan : cancel f f. move=> m; rewrite /f; have [->|mim] := eqVneq m im. by rewrite eqxx; case: ifPn => // /eqP. have [->|m0] := eqVneq m 0%N; first by rewrite eqxx. by rewrite (negbTE mim) (negbTE m0). have flt (i : 'I_n.+1) : (f i < n.+1)%nat. by rewrite /f; case: ifPn => // iim; case: ifPn. set f' := fun i => Ordinal (flt i). have fcan' : cancel f' f' by move=> [j jlt]; exact/val_inj/fcan. have fbij : bijective f' by exists f'; move=> [j jlt]; exact/fcan'. move=>/(_ (fun i => g (f' i)) (fdistmap f' d)). have gA' : [set g (f' i) | i in [set: 'I_n.+1]] `<=` A. by move=>y [i _ <-]; apply gA; eexists. move=>/(_ gA' (fun i => mu (f' i))). have mu'R : \sum_(i0 < n.+1) mu (f' i0) = 0. rewrite (perm_big _ (perm_map_bij _ fbij)); [| exact nil ]. by rewrite big_map -{4}muR; apply congr_big=>// [[j jlt]] _; congr mu; apply fcan'. move=>/(_ mu'R). have mu'E: \sum_(i0 < n.+1) mu (f' i0) *: g (f' i0) = 0. rewrite (perm_big _ (perm_map_bij _ fbij)); [| exact nil ]. rewrite big_map -{4}muE; apply congr_big=>// j _. by congr (mu _ *: g _); exact/fcan'. move=>/(_ mu'E (f' im)). have muip' : 0 < mu (f' (f' im)) by rewrite fcan'. move=>/(_ muip'). have muim' (j : ordinal_finType n.+1) : 0 < mu (f' j) -> fdistmap f' d (f' im) / mu (f' (f' im)) <= fdistmap f' d j / mu (f' j). move=> /muim. rewrite fcan' fdistmapE (big_pred1 im) /=; last first. move=> i; apply/idP/idP; rewrite !inE; last by move=> /eqP ->. by move=> /eqP /(bij_inj fbij) /eqP. rewrite fdistmapE (big_pred1 (f' j)) //. by move=> /= i; apply/idP/idP; rewrite !inE => /eqP; [move=> <-; rewrite fcan' | move=> ->; rewrite fcan']. move=>/(_ muim'). have im0 : f' im == ord0 by apply/eqP/val_inj => /=; rewrite /f eqxx. move=>/(_ im0) [n' [g' [d' [n'le g'A e]]]]. exists n', g', d'; split=>//; rewrite -e. rewrite 2!avgnrE /avgnr. rewrite (perm_big _ (perm_map_bij _ fbij)); [| exact nil ]. rewrite big_map; apply congr_big=>// j _. rewrite fdistmapE (big_pred1 (f' j))=>// k /=. by rewrite unfold_in=>/=; apply/eqP/eqP=>e'; apply (bij_inj fbij); rewrite fcan'. move=>/eqP ime; move: muip muim; rewrite {im}ime => muip muim. have mu0 : mu ord0 != 0 by apply /eqP=>mu0; move: muip; rewrite mu0 lt0r eq_refl. have k0mu0 : d ord0 / mu ord0 * mu ord0 = d ord0. by rewrite -{2}[mu ord0]divr1 mulf_div [_*1]mulrC -mulf_div divr1 mulfV // mulr1. set ef : 'I_n -> R := finfun (fun i => d (lift ord0 i) - d ord0 / mu ord0 * mu (lift ord0 i)). have ef0 i : (0 <= ef i). rewrite /ef ffunE subr_ge0. have [mujp|mujp] := ltP 0 (mu (lift ord0 i)). by rewrite -ler_pdivlMr // muim. rewrite (@le_trans _ _ 0)//. by rewrite mulr_ge0_le0//= divr_ge0// ltW. have ef1 : (\sum_(a in 'I_n) ef a = 1). rewrite -[1]subr0 -[in RHS](mulr0 (d ord0 / mu ord0)) -(FDist.f1 d) -[in _ * 0]muR mulr_sumr. rewrite -sumrB big_ord_recl k0mu0 subrr add0r. by apply eq_bigr => i _; rewrite /ef ffunE. pose e := FDist.make ef0 ef1. have /IHn - /(_ e): [set g (lift ord0 i) | i in [set: 'I_n]] `<=` A. by move=>y [i _ <-]; exact/gA. move=> -[n' [g' [d' [n'le g'A' gde]]]]. exists n', g', d'; split=> //. rewrite -gde 2!avgnrE /avgnr big_ord_recl -k0mu0 -scalerA. move/eqP: muE; rewrite big_ord_recl addr_eq0 => /eqP ->. rewrite scalerN -scaleNr scaler_sumr -big_split; apply congr_big=>// i _. by rewrite scalerA /= -scalerDl; congr (_ *: _); rewrite addrC mulNr ffunE. 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