Convexity

Stream: maths

[Patrick Massot]

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]

@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]

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

[Patrick Massot]

@Alexander Bentkamp?

[Alexander Bentkamp]

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

[Alexander Bentkamp]

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

[Patrick Massot]

Could you share your file?

[Alexander Bentkamp]

convex.lean

[Alexander Bentkamp]

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]

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]

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

[Alexander Bentkamp]

I am actively working on this

[Alexander Bentkamp]

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

[Patrick Massot]

Then let's prove it!

[Alexander Bentkamp]

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

[Patrick Massot]

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]

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

[Alexander Bentkamp]

Ok, sounds good.

[Patrick Massot]

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

[Patrick Massot]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Alexander Bentkamp]

How would that work exactly?

[Mario Carneiro]

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]

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.

[Mario Carneiro]

@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]

there should be something in ring_theory/algebra.lean

[Mario Carneiro]

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]

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

[Patrick Massot]

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]

ok, sure. I can do that.

[Alexander Bentkamp]

and algebra.of_ring_hom works like a charm!