mathlib3

5f803fae - feat(analysis/convex/function): helper lemmas and general cleanup (#9438)

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.