proposition: Lemma hull_convex X : forall x y, (hull X) x -> (hull X) y -> hull [set x; y] `<=` hull X.
proof: Proof. move=> + + [n][g][d][d0 d1 gX->] [m][h][e][e0 e1 hX ->]. rewrite hull2=>_ _ x [t] /andP. rewrite !bnd_simp -[(_ <= 1)%R]subr_ge0 => [[t0 t1]] <-. exists (n + m)%N, (fun i=> match split i with inl i => g i | inr i => h i end), (fun i=> match split i with inl i => t * (d i) | inr i => (`1- t) * e i end); split. - by move=>i; case: (split i)=>j; apply mulr_ge0. - rewrite big_split_ord/= -{1}(add_onemK t); congr +%R. rewrite -{3}(mulr1 t) -{1}d1 mulr_sumr; apply congr_big=>// i _. case: (splitP (lshift m i)). by move=>j ij; congr (_ * d _); apply val_inj. by move=> k/= ink; move: (ltn_ord i); rewrite ink -ltn_subRL subnn ltn0. rewrite -{2}(mulr1 (`1- t)) -{1}e1 mulr_sumr; apply congr_big=>// i _. case: (splitP (rshift n i))=>/=. by move=> j/= nij; move: (ltn_ord j); rewrite -nij -ltn_subRL subnn ltn0. by move=>j /eqP; rewrite eqn_add2l=>/eqP ij; congr (_ * e _); apply val_inj. - by move=>y/= [i] _; case: split=>j <-; [ apply gX | apply hX ]. - rewrite big_split_ord /conv; congr +%R; rewrite scaler_sumr; apply congr_big => // i _; rewrite scalerA. + case: (splitP (lshift m i)). by move=> j ij; congr (_ * d _ *: g _); apply val_inj. by move=> k/= ink; move: (ltn_ord i); rewrite ink -ltn_subRL subnn ltn0. + case: (splitP (rshift n i)) =>/=. by move=> j/= nij; move: (ltn_ord j); rewrite -nij -ltn_subRL subnn ltn0. by move=> j /eqP; rewrite eqn_add2l => /eqP ij; congr (_ * e _ *: h _); apply val_inj. Qed.
imports: encompass conv mathcomp(all_ssreflect all_algebra vector reals normedtype) mathcomp(classical_sets boolp mathcomp_extra) counterclockwise mathcomp.algebra_tactics(ring) mathcomp.zify(zify)