[Merged by Bors] - feat(algebra/module): define ordered semimodules and generalize convexity of functions

[dupuisf]

---

This defines a new typeclass for ordered semimodules, in which both the semiring and the semimodule are ordered, and where the scalar product respects the order relations. This is then used to generalize the definition of convexity for functions, enabling (in the long term) to define operator convexity.

I also plan to connect this to convex cones, which define an order on the vector space and vice-versa.

[dupuisf]

Hmm, even with the implicit a b c, it still wants the λ _ _ _...

[dupuisf]

No problem -- thanks a lot for the suggestions!

[eric-wieser]

Can this not be generalized to β because β has no max?

[dupuisf]

Yeah. The other option would be to generalize it to a β with a linear order (and a semimodule with ℝ as the ring), so basically pretty much just ℝ...

[semorrison]

Maybe add a doc-string to this effect?

[eric-wieser]

The other option would be to generalize it to a β with a linear order (and a semimodule with ℝ as the ring), so basically pretty much just ℝ...

Hmm, what if I defined a lexicographic ordering on pairs β = (ℝ, ℝ), and gave them the obvious semimodule structure.

This lemma would then hold even though β is not ℝ, right, meaning we could generalize as something like the following?

Suggested change

	lemma convex_on.le_on_segment {f : E → ℝ} (hf : convex_on s f) {x y z : E}
	(hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ [x, y]) :
	f z ≤ max (f x) (f y) :=
	lemma convex_on.le_on_segment [linear_order β] {f : E → β} (hf : convex_on s f) {x y z : E}
	(hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ [x, y]) :
	f z ≤ max (f x) (f y) :=

[dupuisf]

Done!

[dupuisf]

Oops -- sorry @eric-wieser, I think you must have added this comment at the same time as I confirmed the merger. I think it's probably simpler now to keep this in mind for the next PR on the subject: I'll be defining concave_on next, so I'll have to make another pass on these lemmas anyway.

[eric-wieser]

Yeah, not a big deal - its not like you actively removed a generalization, you just missed one that could be added :)

[semorrison]

Otherwise, LGTM.

[semorrison]

bors d+

[bors]

✌️ dupuisf can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[dupuisf]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests