Proof mining for the dual of a Banach space with extensions for uniformly Fréchet differentiable functions

We present a proof-theoretically tame approach for treating the dual space of an abstract Banach space in systems amenable to proof mining metatheorems which quantify and allow for the extraction of the computational content of large classes of theorems about the dual of a Banach space and its corresponding norm, unlocking a major branch of functional analysis as a new area of applications for these methods. The approach relies on using intensional methods to deal with the high quantifier complexity of the predicate defining the dual space as well as on a proof-theoretically tame treatment of suprema over (certain) bounded sets in normed spaces to deal with the norm of the dual. Beyond this, we discuss further possible extensions of this system to deal with convex functions and corresponding Fréchet derivatives and their duality theory through Fenchel conjugates, together with the associated Bregman distances, which provide the logical basis for a range of recent applications of proof mining methods to these branches of nonlinear analysis.