Zulip Chat Archive

Stream: maths

Topic: Convexity


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Patrick Massot (Mar 08 2019 at 18:18):

@Alexander Bentkamp?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Mar 08 2019 at 18:25):

Could you share your file?

view this post on Zulip Alexander Bentkamp (Mar 08 2019 at 18:27):

convex.lean

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Mar 08 2019 at 18:45):

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

view this post on Zulip Alexander Bentkamp (Mar 08 2019 at 19:00):

I am actively working on this

view this post on Zulip 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...

view this post on Zulip Patrick Massot (Mar 08 2019 at 19:04):

Then let's prove it!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Mar 08 2019 at 19:08):

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

view this post on Zulip Alexander Bentkamp (Mar 08 2019 at 19:09):

Ok, sounds good.

view this post on Zulip Patrick Massot (Mar 08 2019 at 19:10):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Alexander Bentkamp (Mar 08 2019 at 20:31):

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

view this post on Zulip Alexander Bentkamp (Mar 08 2019 at 20:33):

How would that work exactly?

view this post on Zulip 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

view this post on Zulip 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   := {
 smul_add := λ _ _ _, mul_add _ _ _,
 add_smul :=
  begin
    assume _ _ _,
    unfold has_scalar.smul,
    rw [complex.of_real_add],
    exact add_mul _ _ _,
  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.

view this post on Zulip 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

view this post on Zulip Kenny Lau (Mar 08 2019 at 20:36):

there should be something in ring_theory/algebra.lean

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Alexander Bentkamp (Mar 08 2019 at 21:04):

ok, sure. I can do that.

view this post on Zulip 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