Convexity and concavity over rational

Stream: general

[Yakov Pechersky]

In analysis.convex.basic, we define docs#convex and related things as properties for some E : Type* with [module ℝ E]. Is there a reason why it isn't defined more generally for an R-module where [linear_ordered_semiring R]?

[Johan Commelin]

I guess intuitively we want to apply this to things that are complete. But I agree that it makes sense in a more general setting. Do you have a particular application in mind?

[Yakov Pechersky]

I'm formalizing some texts around tropical algebra/geometry. The evaluation of a tropical polynomial (as seen as

@[simp] def _root_.polynomial.eval_tropical (p : polynomial (tropical (with_top R))) (x : R) :
  tropical (with_top R) :=
  eval (trop (x : with_top R)) p

), is concave. It's defined over a [linear_ordered_semiring R], so it works over the naturals and rationals too, for example. In fact, this concavity leads to the tropical fundamental theorem of algebra showing that tropical polynomials, when seen as functions from R to R, are not unique, but admit a unique "reduced" polynomial. I think that's named minpoly in mathlib?

[Reid Barton]

At least a vector space over an ordered field makes sense

[Sebastien Gouezel]

I guess a reason is that when it's only defined over the reals you don't need to specify the ring. Having the ring defined as an out_param sounds like a bad idea (a module over the reals is also a module over nnreals, so Lean wouldn't know which one to choose), but I guess we can have the general definition specifying the R, and a notation specific to the real case hiding the field, which should be by far the most common situation.

[Reid Barton]

I'd suggest that convexity over the naturals is not a very useful notion (if you just make the obvious change to the definition).

[Yakov Pechersky]

I agree about the naturals. Only with the rationals does it start to become useful =)

[Yaël Dillies]

This is something that's been on many people's minds.

[Yaël Dillies]

See #2910 and #4787

[Yakov Pechersky]

Thanks for those PR pointers. The affine space is an interesting way to express it. Currently, I'm testing loosening the module restriction on the definition to just has_scalar, since the definition requires no laws. I know that the property isn't useful (or even really provable) without the laws. But I'm having issues trying to define concavity on functions of type R -> with_top R, since they can't have module. And if I loosen slightly to distrib_mul_action, then I hit a diamond. I'll make a new thread about that.

[Yaël Dillies]

Ah, concavity on with_top R sounds dope. Is it like concave stuff, infinity, more concave stuff?