Convexity properties of inner product spaces #
Main results #
InnerProductSpace.toUniformConvexSpace: an inner product space is a uniformly convex space.
Tags #
inner product space, Hilbert space, norm
@[instance 100]
instance InnerProductSpace.toUniformConvexSpace {F : Type u_1} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] :