Commit 2021-10-03 01:38 5f803fae

feat(analysis/convex/function): helper lemmas and general cleanup (#9438) This adds

• convex_iff_pairwise_on_pos
• convex_on_iff_forall_pos, concave_on_iff_forall_pos,
• convex_on_iff_forall_pos_ne, concave_on_iff_forall_pos_ne
• convex_on.convex_strict_epigraph, concave_on.convex_strict_hypograph generalizes some instance assumptions:
• convex_on.translate_ didn't need module 𝕜 β but has_scalar 𝕜 β.
• some proofs in analysis.convex.exposed were vestigially using ℝ.

and golfs proofs.