[Merged by Bors] - feat(analysis/convex/function): API for strict convex functions

[YaelDillies]

This provides all the basic API for strict_convex_on and strict_concave_on.

---

• depends on: [Merged by Bors] - feat(analysis/convex/function): helper lemmas and general cleanup #9438
• depends on: [Merged by Bors] - feat(analysis/convex/function): define strictly convex/concave functions #9439

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - feat(analysis/convex/function): helper lemmas and general cleanup #9438
• [Merged by Bors] - feat(analysis/convex/function): define strictly convex/concave functions #9439

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[ocfnash]

Can we drop (hxy : x ≠ y) given that we have (hz : z ∈ open_segment 𝕜 x y)?

[YaelDillies]

Eheh, we actually can because we know that y ≠ z because f y < f z. Well spotted.

[YaelDillies]

Note however that it requires module 𝕜 E while those only require has_scalar 𝕜 E, so I've duplicated all lemmas.

[ocfnash]

I had not realised open_segment 𝕜 x x = {x} when I wrote those words but fortunately you correctly identified the substitute hypothesis f y < f z.

Regarding the duplication, personally I'm not yet convinced it's worth it. Couldn't we just have the module 𝕜 E versions?

I think it's worth having definitions very general but are people ever going to use these lemmas when they don't have a module 𝕜 E structure to hand?

[YaelDillies]

As you want. I agree this makes for many lemmas, of which only one or two are currently used (on my branch sperner-again I think, actually).

[ocfnash]

Very nice work! Just a few minor comments.

[ocfnash]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests