Definition of convex_on

Stream: maths

[Frédéric Dupuis]

Currently convexity for functions is only defined for functions of type E → ℝ. Would anyone object if I were to generalize this to E → β with [add_comm_monoid β] [preorder β] [semimodule ℝ β]? The main drawback is that some multiplications would be replaced by smuls, but it turns out that it involves very few changes in the code.

[Frédéric Dupuis]

And the reason I wanted to do that is that I would like to introduce concave_on for concave functions, and it doesn't seem possible to use order_dual if ℝ is hardcoded.

[Scott Morrison]

Is there any case other than β = order_dual ℝ that you have in mind? It seems a lot of work relative to just talking about the convexity of -f.

[Frédéric Dupuis]

Not in the short term, but there is the concept of "operator convex" functions that I've worked with quite a bit, where we say that A ≤ B for A and B Hermitian operators when B-A is positive semidefinite, and define convexity of functions based on that.

[Yury G. Kudryashov]

I think it's OK to have smul instead of mul.

[Yury G. Kudryashov]

I know nothing about "operator convex" functions and their applications.

[Yury G. Kudryashov]

Could you please post some links?

[Yury G. Kudryashov]

I mean, I don't care too much about smul vs mul but it's good to know what are the advantages of the new definition.

[Frédéric Dupuis]

The definitions are on Wikipedia here: https://en.wikipedia.org/wiki/Trace_inequality

This goes a bit more in depth, in section 5.3:
http://www-m5.ma.tum.de/foswiki/pub/M5/Allgemeines/MichaelWolf/QChannelLecture.pdf

Otherwise, there's the book "Matrix Analysis" by Rajendra Bhatia:
https://www.springer.com/gp/book/9780387948461

[Frédéric Dupuis]

As far as applications go, there are quite a few in quantum information theory, where positive semidefinite matrices can be interpreted as quantum states, and the theory built around operator convexity allows us to prove all kinds of results about quantum channels and information measures.

[Frédéric Dupuis]

I've thought about this some more, and I think the natural thing to do would be to define convexity for functions of type E → β with β being an ordered semimodule (in the sense of https://en.wikipedia.org/wiki/Ordered_vector_space), so that we would have
x ≤ y → x + z ≤ y + z and y ≤ x → a • y ≤ a • x. Declaring [ordered_add_comm_group β] [semimodule ℝ β] gives me the first condition, but is there a typeclass that would give me the second one?

[Heather Macbeth]

Would it work to assume [topological_module ℝ β] [order_topology β]? Here order_topology is the statement that the order-induced topology on β is the same as the lurking topology from the topological_module structure.

[Heather Macbeth]

You should have that scalar multiplication by nonzero a is both continuous and injective. I haven't thought it through, but under appropriate hypotheses on the order (intermediate value theorem?) this might be enough to get that it is strictly monotone.

[Frédéric Dupuis]

Sounds plausible, but it feels like a bit of overkill to introduce a topology in the picture just for this...

[Frédéric Dupuis]

(and the proof would likely be more work than defining the class I want if it doesn't exist!)

[Yury G. Kudryashov]

AFAIK, there is no such class yet.

[Frédéric Dupuis]

I gave it a shot in this branch I just pushed:
https://github.com/leanprover-community/mathlib/compare/generalized_convex_on

I introduced the class

class ordered_semimodule (R β : Type*)
  [ordered_semiring R] [ordered_add_comm_monoid β] extends semimodule R β :=
(smul_lt_smul_of_pos : ∀ a b : β, a < b → ∀ c : R, 0 < c → c • a < c • b)
(lt_of_smul_lt_smul_of_nonneg : ∀ a b : β, ∀ c : R, c • a < c • b → 0 ≤ c → a < b)

and generalized most definitions about convexity of functions in analysis/convex/basic.lean to work on an ordered_semimodule ℝ β. It went through pretty smoothly I think -- hopefully I haven't made any basic mistake in defining the new class though!

[Yaël Dillies]

@Frédéric Dupuis, how far have you gone? I'm about to generalize {E : Type*} [add_comm_group E] [module ℝ E] to (k : Type*) {E : Type*} [ordered_semiring k] [add_comm_group E] [module k E] and I wanted to check your branch but it doesn't exist anymore.

[Yaël Dillies]

Why is convex_on taking convex s as an hypothesis? It seems like the right thing here would be to make it total (or at least totaller) by allowing any set, even if that means the function isn't really convex on s anymore, but rather convex on convex_hull s.

[Frédéric Dupuis]

@Yaël Dillies I haven't worked any further in that direction since last year. You can go ahead with that change, I think it's a good idea!

[Frédéric Dupuis]

Yaël Dillies said:

Why is convex_on taking convex s as an hypothesis? It seems like the right thing here would be to make it total (or at least totaller) by allowing any set, even if that means the function isn't really convex on s anymore, but rather convex on convex_hull s.

That makes sense to me. The potential downside is that we would then have to include an extra convex s assumption in too many lemmas, but maybe it's still worth it.