mathlib3

49b68e80 - feat(analysis/convex/uniform): Uniformly convex spaces (#13480)

feat(analysis/convex/uniform): Uniformly convex spaces (#13480) Define uniformly convex spaces and prove the implications `inner_product_space ℝ E → uniform_convex_space E` and `uniform_convex_space E → strict_convex_space ℝ E`.