Commit 2022-05-22 11:09 49b68e80

View on Github →

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.

Estimated changes

Created src/analysis/convex/uniform.lean

added theorem exists_forall_closed_ball_dist_add_le_two_mul_sub

added theorem exists_forall_closed_ball_dist_add_le_two_sub

added theorem exists_forall_sphere_dist_add_le_two_sub

Modified src/analysis/inner_product_space/basic.lean

Modified src/analysis/normed/group/basic.lean

added theorem norm_add₃_le

added theorem norm_sub_pos_iff