3728: define ordered semimodules and generalize convexity...

Stream: PR reviews

[Yury G. Kudryashov]

@Frédéric Dupuis I'm rewriting convexity for affine spaces, and I have a question about your old PR #3728
Many lemmas assume {β : Type*} [ordered_add_comm_monoid β] [ordered_semimodule ℝ β]. Is there any reason to prefer these assumptions to {γ : Type*} [ordered_cancel_add_comm_monoid γ] [ordered_semimodule ℝ γ]? A (semi)module over ℝ can't be just an add_comm_monoid anyway (unless someone forgot to define an instance).

[Yury G. Kudryashov]

It makes sense if you're going to generalize to {β : Type*} [ordered_add_comm_monoid β] [ordered_semimodule nnreal β].

[Yury G. Kudryashov]

Do you need this generalization in some case?

[Johan Commelin]

@Reid Barton and I were just talking about ordered semimodules yesterday :rofl:

[Johan Commelin]

Didn't realise there was a PR :see_no_evil:

[Yury G. Kudryashov]

The PR is already merged!

[Johan Commelin]

/me should learn what is in mathlib!

[Johan Commelin]

That's what you get for going on holidays

[Johan Commelin]

@Yury G. Kudryashov What's your reason for preferring the cancellative version?

[Yury G. Kudryashov]

Copy+paste from wrong line

[Yury G. Kudryashov]

Fixed.

[Yury G. Kudryashov]

I'm going to wait for an answer before porting convex_on.

[Frédéric Dupuis]

I didn't have any particularly good reason -- at the beginning I was hoping it would allow us to define convexity for functions into things like nnreal, but as you say it doesn't work anyway. I'd be happy with just ordered_add_comm_group, it would clean things up a bit.

[Frédéric Dupuis]

Although now that I think about it, [ordered_semimodule nnreal β] might be useful for things like weighting Hermitian matrices by probabilities.