## Stream: maths

### Topic: Definition of convex_on

#### Frédéric Dupuis (Aug 05 2020 at 04:09):

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 (Aug 05 2020 at 04:11):

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 (Aug 05 2020 at 07:04):

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 (Aug 05 2020 at 14:09):

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 (Aug 05 2020 at 22:53):

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

#### Yury G. Kudryashov (Aug 05 2020 at 22:54):

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

#### Yury G. Kudryashov (Aug 05 2020 at 22:56):

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 (Aug 06 2020 at 00:26):

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 (Aug 06 2020 at 00:30):

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 (Aug 07 2020 at 00:29):

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 (Aug 07 2020 at 02:47):

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 (Aug 07 2020 at 02:53):

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 (Aug 07 2020 at 03:44):

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

#### Frédéric Dupuis (Aug 07 2020 at 03:44):

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

#### Yury G. Kudryashov (Aug 07 2020 at 05:12):

AFAIK, there is no such class yet.

#### Frédéric Dupuis (Aug 07 2020 at 22:42):

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!

Last updated: May 18 2021 at 08:14 UTC