## Stream: maths

### Topic: Convexity

#### Patrick Massot (Mar 08 2019 at 13:37):

Because of calculus, I realized we don't have anything about convexity in mathlib. I started something, but filling the holes in the API (including the interval API) will be very tedious, so I'd like feedback before moving on: https://gist.github.com/PatrickMassot/6b03a8cd63c44cac510e2abeb2ea710f

#### Patrick Massot (Mar 08 2019 at 13:39):

@Mario Carneiro do you understand why https://gist.github.com/PatrickMassot/6b03a8cd63c44cac510e2abeb2ea710f#file-convex-lean-L116-L120 can't be shrinked to one line containing only abel?

#### Mario Carneiro (Mar 08 2019 at 17:48):

I believe Alexander Bentkamp has been working on convexity, although I don't know if he is ready to release anything

#### Patrick Massot (Mar 08 2019 at 18:18):

@Alexander Bentkamp?

#### Alexander Bentkamp (Mar 08 2019 at 18:22):

Yes, I have started working on convexity, too. What I have is only slightly larger than yours so far.

#### Alexander Bentkamp (Mar 08 2019 at 18:24):

We should probably merge our efforts. My definition is a bit different from yours, but I think they are equivalent.

convex.lean

#### Alexander Bentkamp (Mar 08 2019 at 18:29):

I have been working along the Isabelle theory on convexity: http://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Convex_Euclidean_Space.html

#### Patrick Massot (Mar 08 2019 at 18:45):

Nice! I think we'll need to define segments anyway. For instance we want to be able to state the mean value inequality in terms of a bound on the derivative on the relevant segment. The chosen definition of is_convex itself is not very import, we will have many equivalent formulations anyway (like in you file). About convexity of intervals, I think we need to fill in the intervals API anyway. And once we get inclusion criterion for all kinds of intervals then the convexity of intervals will come for free (from the caracterisation of convexity by inclusion of segments, and the fact that a segment in R is a closed interval). About half spaces in C, why don't you use the fact that re and im are real-linear forms and use the general result you proved above?

#### Patrick Massot (Mar 08 2019 at 18:45):

Are you currently working on this, or is it dormant?

#### Alexander Bentkamp (Mar 08 2019 at 19:00):

I am actively working on this

#### Alexander Bentkamp (Mar 08 2019 at 19:01):

Concerning the halfspaces in C, I haven't found lemmas stating that re and im are real-linear forms...

#### Patrick Massot (Mar 08 2019 at 19:04):

Then let's prove it!

#### Alexander Bentkamp (Mar 08 2019 at 19:06):

Well, that's essentially what I did, but you are right that we should have a lemma explicitly stating that fact.

#### Patrick Massot (Mar 08 2019 at 19:07):

Since you are actively working on this, here is what I propose. I'll open a PR adding stuff to intervals.lean, filling the missing intervals and adding all lemmas stating precisely when a non-empty Icc is contained in another interval. Then you can take everything you want from my convexity gist. I really think we want the segment definition, but then I don't care what is the official definition of convexity, as long as we have many lemmas giving caracterisations.

#### Patrick Massot (Mar 08 2019 at 19:08):

And I say that convexity of all intervals will follow trivially from my interval lemmas

Ok, sounds good.

#### Patrick Massot (Mar 08 2019 at 19:10):

https://github.com/leanprover-community/mathlib/pull/805

#### Patrick Massot (Mar 08 2019 at 19:20):

So you can take this intervals file, remove the corresponding bits from my convexity file, and move from there. Actually I think your symmetric descriptions of segments may be pretty convenient in the ball proofs

#### Patrick Massot (Mar 08 2019 at 19:24):

By the way, it means that you should find a way to make sure your proofs of different conditions for convexity also prove the corresponding descriptions of segments. It only means you should state them as conditions about being in a segment, and then transfer to convexity condition.

#### Patrick Massot (Mar 08 2019 at 19:34):

The Isabelle file is really large. I like the way they state that distance to a fixed point is convex instead of hiding it inside the proof of convexity of balls like I did.

#### Alexander Bentkamp (Mar 08 2019 at 20:16):

By the way, it means that you should find a way to make sure your proofs of different conditions for convexity also prove the corresponding descriptions of segments. It only means you should state them as conditions about being in a segment, and then transfer to convexity condition.

I am not sure what you mean here. Do you just mean that I should prove that my definition is eqivalent to how you defined convexity?

#### Mario Carneiro (Mar 08 2019 at 20:18):

re: re and im linearity, I don't think this exact statement is there but it's a direct application of lemmas that should be there (i.e. re (x + y) = re x + re y, re (r * x) = r * re x)

#### Alexander Bentkamp (Mar 08 2019 at 20:21):

Yes, but I also needed to instantiate C as a R-vector space and then show that (c • x).re = c • x.re. That's around 30 lines that should probably be put into complex/basic.lean at some point.

#### Mario Carneiro (Mar 08 2019 at 20:29):

Oh, I expected these to be in there but they were missing:

lemma smul_re (r : ℝ) (z : ℂ) : (↑r * z).re = r * z.re := by simp
lemma smul_im (r : ℝ) (z : ℂ) : (↑r * z).im = r * z.im := by simp


The stuff about having C as an R vector space and instantiating coe and re as linear functions should go somewhere else, maybe somewhere in ring_theory?

#### Mario Carneiro (Mar 08 2019 at 20:31):

I'm pretty sure we have a method for obtaining a vector space from a ring hom (coe), so that part should be easy, and the linearity conditions should should all be defeq to existing lemmas

#### Alexander Bentkamp (Mar 08 2019 at 20:31):

Oh, then I probably did it the hard way...

#### Alexander Bentkamp (Mar 08 2019 at 20:33):

How would that work exactly?

#### Mario Carneiro (Mar 08 2019 at 20:34):

You can define an instance of vector_space E F given a field hom f : E -> F where you define the smul as a \bu x = f a * x

#### Alexander Bentkamp (Mar 08 2019 at 20:34):

This is how I did it:

instance : has_scalar ℝ ℂ := { smul := λ r c, ↑r * c}

noncomputable instance : vector_space ℝ ℂ := {
begin
assume _ _ _,
unfold has_scalar.smul,
end,
mul_smul :=
begin
unfold has_scalar.smul,
assume r s c, rw [complex.of_real_mul r s],
exact mul_assoc _ _ _
end,
one_smul := λ _, one_mul _,
zero_smul := λ _, zero_mul _,
smul_zero := λ _, mul_zero _,
}


What you wrote sounds much easier than that.

#### Mario Carneiro (Mar 08 2019 at 20:35):

@Kenny Lau will know the state of this - I've seen various versions of it float by the chat but I'm not sure what's made it into mathlib

#### Kenny Lau (Mar 08 2019 at 20:36):

there should be something in ring_theory/algebra.lean

#### Mario Carneiro (Mar 08 2019 at 20:38):

yes, algebra.of_ring_hom looks like it will work, although you have to get the module part out and upgrade it to a vector_space

#### Mario Carneiro (Mar 08 2019 at 20:38):

But I guess it's not a bad thing knowing that actually C is a R-algebra rather than just a module

#### Patrick Massot (Mar 08 2019 at 21:04):

By the way, it means that you should find a way to make sure your proofs of different conditions for convexity also prove the corresponding descriptions of segments. It only means you should state them as conditions about being in a segment, and then transfer to convexity condition.

I am not sure what you mean here. Do you just mean that I should prove that my definition is eqivalent to how you defined convexity?

Yes, I think so

#### Alexander Bentkamp (Mar 08 2019 at 21:04):

ok, sure. I can do that.

#### Alexander Bentkamp (Mar 08 2019 at 21:14):

and algebra.of_ring_hom works like a charm!

Last updated: May 19 2021 at 02:10 UTC