The simplest Hahn-Banach extension theorem in Hilbert space $X$ avoids the use of the axiom of choice by virtue of the Riesz representation theorem. But what about the version of the theorem where the sought-for linear functional is required to remain below a given sub-linear or convex function? Also, to which extent can we separate 2 disjoint convex sets by a hyperplane without Zorn? Can we assert that any hyperplane $H\subset X$ has a translate that is tangent (*) to a given bounded closed convex subset $C\subset X$?

This question has an identical counterpart on stackexchange.

(*) "tangent" means that the linear bounded function whose kernel represents the hyperplane is non-negative on $C$ but not strictly positive.