Commit 2021-11-08 11:43 4dd7ecae

View on Github →

feat(analysis/{seminorm, convex/specific_functions}): A seminorm is convex (#10203) This proves seminorm.convex_on, convex_on_norm (which is morally a special case of the former) and leverages it to golf seminorm.convex_ball. This also fixes the explicitness of arguments of convex_on.translate_left and friends.

Estimated changes

Modified src/analysis/convex/function.lean

modified theorem concave_on.translate_left

modified theorem concave_on.translate_right

modified theorem convex_on.translate_left

modified theorem convex_on.translate_right

modified theorem strict_concave_on.translate_left

modified theorem strict_concave_on.translate_right

modified theorem strict_convex_on.translate_left

modified theorem strict_convex_on.translate_right

Modified src/analysis/convex/specific_functions.lean

added theorem convex_on_norm

Modified src/analysis/seminorm.lean