proposition: Lemma fconvex_max_ext (C: {convex_set E}) (x: E): fconvex_strict -> x \in C -> f x < +oo -> (forall y, y \in C -> f y <= f x) -> x \in ext C.
proof: Proof. move=> fconv xC fxoo xmax. rewrite in_setE/ext/= =>u v /xmax uC /xmax vC /set_mem [t] _ xE; subst x. move: (prob_ge0 t)=>/RleP; rewrite le0r=>/orP; case. by move=>/eqP/val_inj ->; right; rewrite conv0. move=>t0. move: (prob_le1 t)=>/RleP; rewrite -subr_ge0 le0r=>/orP; case. have->: Rdefinitions.IZR (BinNums.Zpos 1%AC) = Prob.p (1%R)%:pr by []. by rewrite subr_eq0=>/eqP/val_inj <-; left; rewrite conv1. rewrite subr_gt0=>t1. have t01: ssrR.ltRb (Rdefinitions.IZR BinNums.Z0) t && ssrR.ltRb t (Rdefinitions.IZR (BinNums.Zpos 1%AC)). by apply/andP; split; apply/ssrR.ltRP/RltP. have [->|/eqP uv] := eqVneq u v; first by rewrite convmm; left. move:(fconv u v (OProb.mk t01) uv)=>/=. have fle: (Prob.p t)%:E * f u + (onem (Prob.p t))%:E * f v <= f (u <|t|> v). have ->: f (u <|t|> v) = (Prob.p t)%:E * f (u <|t|> v) + (onem (Prob.p t))%:E * f (u <|t|> v). rewrite -ge0_muleDl ?lee_fin /onem ?RminusE -?EFinD. - by rewrite addrCA subrr addr0 mul1e. - by apply ltW. - by rewrite subr_ge0; apply/RleP/prob_le1. apply (@lee_add R_realDomainType); rewrite (@lee_pmul2l R_realDomainType)//= lte_fin. by rewrite subr_gt0. by move=>/(Order.POrderTheory.le_lt_trans fle); rewrite ltxx. Qed.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets boolp Rstruct) infotheo(convex Reals_ext) preliminaries Reals