proposition: Lemma supporting_hyperplan_face (A : {convex_set E}) (f: {linear E -> R^o}) (a: R_ringType) : supporting_hyperplane A f a <-> (exists x, x \in A /\ f x = a) /\ face A (A `&` (f @^-1` [set a])).
proof: Proof. split; move=>[hex hface]; split=>//. wlog: f a hex hface / (forall x : E, x \in A -> f x <= a). move=>h; move: (hface); case=>hf. by apply (h f a). move: h=>/(_ (GRing.comp_linear f (GRing.opp_linear E)) (- a)). have hf' (x : E) : x \in A -> GRing.comp_linear f (GRing.opp_linear E) x <= - a. by move=> xA /=; rewrite -scaleN1r linearZZ scaleN1r ler_oppl opprK; apply hf. have hex': exists x : E, x \in A /\ GRing.comp_linear f (GRing.opp_linear E) x = - a. by move: hex=>[x [xA fx]]; exists x; split=>//=; rewrite -fx -scaleN1r linearZZ scaleN1r. move=>/(_ hex' (or_introl hf') hf'); congr (face A (A `&` _)). by rewrite eqEsubset; split=>x /= /eqP; rewrite -scaleN1r linearZZ scaleN1r; [ rewrite eqr_opp | rewrite -eqr_opp ]=>/eqP. move=> hf; apply face'P; split; [ by apply subIsetl | |]. exact: (is_convex_setI _ (convex_set_of (is_convex_set_preimage _ (convex_set_of (is_convex_set1 (a : GRing.regular_lmodType R_ringType)))))). move=> x u v /set_mem [xA xa] uA vA /set_mem [t _ tx] xv; apply mem_set; (split; [ by apply set_mem |]); apply /eqP; rewrite -lte_anti; apply /andP; (split; [ by apply hf |]). have t0 : (t : R_ringType) != 0. by apply/eqP=>/val_inj t0; subst t; move: tx xv; rewrite conv0 => ->; rewrite eqxx. have tgt : 0 < (t : R_ringType) by rewrite lt0r t0=>/=; exact/RleP. move: tx=>/(f_equal (fun x=> (t : R_ringType)^-1 *: (x - (onem t) *: v))). rewrite -addrA subrr addr0 scalerA mulVf // scale1r=>->. rewrite linearZZ linearD xa -scaleNr linearZZ ler_pdivl_mull// addrC -subr_ge0 -addrA -mulNr -{1}[a]mul1r -mulrDl scaleNr -scalerN -mulrDr; apply mulr_ge0. exact/RleP. by rewrite addrC Num.Internals.subr_ge0; apply hf. have : forall x y, x \in A -> y \in A -> f x < a -> a < f y -> False. move=> u v uA vA fua afv. move: (Order.POrderTheory.lt_trans fua afv); rewrite -subr_gt0=>fufv. have t01: ssrR.leRb (Rdefinitions.IZR BinNums.Z0) ((f v - a) / (f v - f u))%R && ssrR.leRb ((f v - a) / (f v - f u))%R (Rdefinitions.IZR (BinNums.Zpos 1%AC)). apply/andP; split; apply/ssrR.leRP/RleP. by apply divr_ge0; apply ltW=>//; rewrite subr_gt0. rewrite ler_pdivr_mulr// mul1r -subr_ge0 opprB addrAC addrCA subrr addr0 subr_ge0. by apply ltW. move: hface=>/face'P [_ _ /(_ (u <| Prob.mk t01 |> v) u v)]. have inuv: u <| Prob.mk t01 |> v \in segment u v. by apply mem_set; exists (Prob.mk t01). have uva: f (u <| Prob.mk t01 |> v) = a. rewrite/= affine_conv/=/conv/=. move: fufv; rewrite lt0r=>/andP [fufv _]. apply (mulfI fufv). rewrite/GRing.regular_lmodType/GRing.scale/=. rewrite mulrDr mulrAC mulrCA mulrAC divff// mulr1. rewrite [onem _ * _]mulrBl mul1r mulrBr mulrAC mulrCA mulrAC divff// mulr1. rewrite -mulrBl opprB addrAC addrCA subrr addr0. rewrite 2!mulrBl mulrC addrAC addrCA subrr addr0. by rewrite -mulrBr mulrC. have Aa: u <| Prob.mk t01 |> v \in (A `&` f @^-1` [set a])%classic. apply mem_set; split=>//. by move:(convex_setP A)=>/asboolP; apply; rewrite -in_setE. move=>/(_ Aa uA vA inuv). have nev: u <|{| Prob.p := ((f v - a) / (f v - f u))%R; Prob.Op1 := t01 |}|> v != v. rewrite -subr_eq0 -{4}(scale1r v) -addrA -scalerBl addrAC subrr add0r scaleNr -scalerBr scaler_eq0 subr_eq0. apply/negP=>/orP; case=>/eqP. move=>/= t0. move:uva; rewrite/conv/= t0 scale0r add0r onem0 scale1r=>fva. by move:afv; rewrite fva ltxx. by move=>uv; move:fufv; rewrite uv subrr ltxx. by move=>/(_ nev) /set_mem [_ /= fuae]; move: fua; rewrite fuae -subr_gt0 lt0r subrr eq_refl. move=>h. move: (boolp.EM (exists x: E, x \in A /\ f x < a)); case. move: (boolp.EM (exists x: E, x \in A /\ a < f x)); case. by move=>[y [yA afy]] [x [xA fxa]]; elim (h x y xA yA fxa afy). by move=>allge _; left=> x xA; rewrite leNgt; apply /negP=>fxa; apply allge; exists x; split. by move=>allge; right=> x xA; rewrite leNgt; apply /negP=>fxa; apply allge; exists x; split. Qed.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets boolp Rstruct) infotheo(convex Reals_ext) preliminaries Reals