Commit 2022-03-26 20:22 434a938b

View on Github →

feat(analysis/convex/strict_convex_space): Strictly convex spaces (#11794) Define strictly_convex_space, a Prop-valued mixin to state that a normed space is strictly convex.

Estimated changes

Modified src/analysis/convex/integral.lean

added theorem ae_eq_const_or_norm_integral_lt_of_norm_le_const

deleted theorem strict_convex.ae_eq_const_or_norm_integral_lt_of_norm_le_const

Modified src/analysis/convex/strict.lean

Created src/analysis/convex/strict_convex_space.lean

added theorem combo_mem_ball_of_ne

added theorem dist_add_dist_eq_iff

added theorem norm_add_lt_of_not_same_ray

added theorem norm_combo_lt_of_ne

added theorem open_segment_subset_ball_of_ne

added theorem same_ray_iff_norm_add

added theorem strict_convex_closed_ball

added theorem strict_convex_space.of_norm_add

added theorem strict_convex_space.of_strict_convex_closed_unit_ball

Modified src/analysis/convex/topology.lean

added theorem dist_add_dist_of_mem_segment

Modified src/analysis/inner_product_space/basic.lean

Modified src/analysis/normed_space/basic.lean

added theorem inv_norm_smul_mem_closed_unit_ball