proposition: Lemma ext_carac (A : {convex_set E}) (x: E): x \in A -> [<-> x \in ext A; forall u v, u \in A -> v \in A -> x = u <| probinvn 1 |> v -> u = v; is_convex_set (A `\ x)%classic; face A [set x]].
proof: Proof. move=>xA. have ne20: (2 : R_ringType) != 0 by rewrite intr_eq0. have ge20: (0 : R_ringType) <= 2 by apply mulrz_ge0=>//; exact ler01. split. move=>xext u v uA vA xe. move: xext=>/set_mem /(_ u v uA vA). have xuv: x \in segment u v. by apply mem_set; subst x; exists (probinvn 1). move=>{uA} {vA} /(_ xuv) {xuv}. wlog: u v xe / x = u. move=> h; case=> xe'. by apply h=>//; left. apply /esym; apply h=>//; last by left. rewrite xe convC; congr (v <| _ |> u). apply val_inj=>/=. rewrite probinvn1 /onem. by apply/eqP; rewrite subr_eq -(div1r 2) -splitr. move: xe=> -> + _. move=> /(congr1 (fun x => 2 *: x)). rewrite scalerDr probinvn1 onem_half 2!scalerA divff// 2!scale1r. by rewrite -pmulrn mulr2n scalerDl scale1r=>/addrI/esym. split. move=>xext. apply/asboolP=>u v t [uA ux] [vA vx]. split; first by move:(convex_setP A)=>/asboolP; apply. wlog: u v t xext xA uA ux vA vx / (t : R_ringType) <= 2^-1. move=>h. have [tle|tle] := leP (t : R_ringType) (2^-1); first exact: (h u v t). rewrite convC. apply (h v u (onem t)%:pr)=>//. rewrite -onem_half; apply ler_sub=>//. exact/ltW. move=>tle. have t01: ssrR.leRb (Rdefinitions.IZR BinNums.Z0) (2%:R*(t : R_ringType)) && ssrR.leRb (2*(t : R_ringType)) (Rdefinitions.IZR (BinNums.Zpos 1%AC)). apply/andP; split; apply/ssrR.leRP/RleP. apply mulr_ge0=>//. by apply/RleP/prob_ge0. by move:tle=>/(ler_wpmul2l ge20); rewrite divff. move=>/esym xE. move: xext=>/(_ (u <| Prob.mk t01 |> v) v). rewrite -convA' convmm. have ->: p_of_rs (Prob.mk t01) (probinvn 1) = t. apply val_inj. rewrite/= p_of_rsE/=. have tE: (2*(t : R_ringType))/2 = t. by rewrite mulrAC divff// mul1r. rewrite -{2}tE. congr Rdefinitions.RbaseSymbolsImpl.Rmult. rewrite/R_unitRing/GRing.inv/=/Rinvx. case:ifP=>//. by rewrite ne20. have wA: u <| Prob.mk t01 |> v \in A. by apply mem_set; move:(convex_setP A)=>/asboolP; apply. move: vA=>/mem_set vA /(_ wA vA xE) /(congr1 (fun x => x-v)). rewrite subrr /conv/= -addrA -{2}(scale1r v) -scalerBl addrAC subrr add0r scaleNr -scalerBr. apply /eqP; rewrite scaler_eq0; apply /negP=>/orP; case. rewrite mulf_eq0 pnatr_eq0/= =>/eqP t0. move:xE. have ->: t = 0%:pr by apply val_inj. by rewrite conv0=>/esym. rewrite subr_eq0=>/eqP uv; subst v. by move:xE; rewrite convmm=>/esym. split. move=>/asboolP Axconv. split; [ by move=>u /= ->; apply set_mem | by apply is_convex_set1 | ]=> y u v /set_mem -> /set_mem uA /set_mem vA /set_mem [p _ xE] xu xv; exfalso. have uAx: (A `\ x)%classic u by split=>//= ux; subst u; move: xu; rewrite eq_refl. have vAx: (A `\ x)%classic v by split=>//= vx; subst v; move: xv; rewrite eq_refl. have: (A `\ x)%classic x by rewrite -{2}xE; apply (Axconv _ _ _ uAx vAx). by move=>[_ /= f]. move=>xface; apply /mem_set=>u v uA vA xuv. suff: (x == u) || (x == v) by move=>/orP; case=> /eqP ->; [ left | right ]. apply /negP=>/negP; rewrite negb_or=>/andP [xu xv]. move: xface=> [_ _ /(_ x u v)]. have xx: x \in [set x]%classic by apply /mem_set. move=>/(_ xx uA vA xuv xu xv) [/set_mem /= ux /set_mem /= vx]; subst u. by move: xu; rewrite eq_refl. Qed.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets boolp Rstruct) infotheo(convex Reals_ext) preliminaries Reals