Convexity refactor

Stream: general

[Yaël Dillies]

State of the convexity refactor

• port convexity to vector spaces ([module 𝕜 E])
  • redefine segment and open_segment. Done in #9094.
  • redefine convex and convex_hull. See #9058.
  • redefine convex_on and concave_on
  • redefine finset.center_mass
  • redefine std_simplex
  • port the rest of the library
• port convexity to affine spaces ([module 𝕜 V] [affine_space V E]). Very much not done.

[Yaël Dillies]

Little update, #9058 (finally!) compiles. It was much easier to generalize convex and convex_hull than segment and open_segment because somehow their properties are closer to the axioms and require less typeclass fuss.

[Yaël Dillies]

BTw @Yury G. Kudryashov I think you should have your say on this, as you started #4787.

[Yury G. Kudryashov]

I failed to localize my porting efforts, created a huge mess, then failed to make it ready for review. So, I'm not sure that I should have a say on this. ;)

[Yury G. Kudryashov]

IMHO porting to affine spaces is not much harder than porting to modules.

[Yaël Dillies]

Oh that's not kindly worded for yourself! I would rather say that you opened my eyes a PR, sparked the idea in me, warned me of the monstruousity of the refactor, and then let me the opportunity to have a go myself!

[Yaël Dillies]

Yury G. Kudryashov said:

IMHO porting to affine spaces is not much harder than porting to modules.

That's exactly what I thought, but one design decision I have done (which is very easily reversible, though) is that I allow convexity and stuff even the space has no negation.

[Yaël Dillies]

And that's incompatible with affine spaces, right? It looks like generalization of convexity branches here and there's no common ancestor we can generalize to.

[Yury G. Kudryashov]

Here is a problem I can't solve without creating diamonds. You can define convexity_space to be a space with convex combinations ∀ x y : R, 0 ≤ x → 0 ≤ y → x + y = 1 → E → E → E with some natural axioms.

[Yury G. Kudryashov]

Then you have two ways to go from vector_space R E to convexity_space R E.

[Yury G. Kudryashov]

(deleted)

[Yury G. Kudryashov]

One way is to use module structure and treat R as a semiring. Another is to use affine_space structure (but this needs subtraction).

[Yaël Dillies]

Oh, interesting. I will sleep on it.

[Yury G. Kudryashov]

While these two ways result in equal convexity structures, it seems that we can't make these structures defeq.

[Yury G. Kudryashov]

So, only one of the ways can be an instance.

[Yaël Dillies]

Are you saying we should have convexity_space?

[Frédéric Dupuis]

I'm having flashbacks to some old conversations:
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/convexity
https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/3728.3A.20define.20ordered.20semimodules.20and.20generalize.20convexity.2E.2E.2E

[Yury G. Kudryashov]

@Yaël Dillies No, I've described a half-solution to the problem. Since it doesn't solve the problem, I don't suggest we implement it.

[Yury G. Kudryashov]

On the one hand, we can't have a notion of convexity that works both for modules over nnreal and for affine spaces without an abstraction like convexity_space.

[Yury G. Kudryashov]

On the other hand, I'm not sure that we really need both.

[Yaël Dillies]

Frédéric Dupuis said:

I'm having flashbacks to some old conversations:

Pleas have flashbacks more often!

[Yaël Dillies]

If we were to implement your half-solution, Yury, then I feel like the convex operation in a vector space should be inherited from the module side of things, rather than the affine_space one, because it is much closer to the axioms of a vector space.

[Yaël Dillies]

Next up is #9247! It's just splitting analysis.convex.basic further.

[Johan Commelin]

Fantastic! That's easy to review (-;

[Yaël Dillies]

finset.center_mass uses division, which makes it very restrictive. How much do people care about that division being there?

[Yaël Dillies]

From my point of view,
Pros: Doesn't require that the sum of the weights is 1, but merely that it's positive.
Cons: Needs a field. Doesn't follow affine_combination.

[Yury G. Kudryashov]

It was written before affine_combination.

[Yaël Dillies]

This looks as if we had taken docs#convex_iff_div to be the definition of convexity.

[Yury G. Kudryashov]

Feel free to change it.

[Yaël Dillies]

Okay :smile:

[Yaël Dillies]

What do you think about renaming it linear_combination?

[Yury G. Kudryashov]

You can also introduce a proper type for {x : ι →₀ R | (∀ i, 0 ≤ x i) ∧ x.sum (λ i, id)}.

[Yury G. Kudryashov]

This is the free object in the category of convex spaces.

[Yury G. Kudryashov]

See what we do about linear combinations in linear algebra.

[Yaël Dillies]

Yury G. Kudryashov said:

This is the free object in the category of convex spaces.

Erhm... will look that up :sweat:

[Yury G. Kudryashov]

I mean that for any convex space and a map f : ι → E you have a unique map from g : {x : ι →₀ R | (∀ i, 0 ≤ x i) ∧ x.sum (λ i, id)} to E such that g (single i x) = f x.

[Yury G. Kudryashov]

You can ignore the category theory language.

[Yaël Dillies]

Ah! Did you mean to add an = 1?

[Yaël Dillies]

I was stuck typechecking.

[Yaël Dillies]

Yury G. Kudryashov said:

I mean that for any convex space and a map f : ι → E you have a unique map from g : {x : ι →₀ R | (∀ i, 0 ≤ x i) ∧ x.sum (λ i, id)} to E such that g (single i x) = f x.

Is this not exactly docs#std_simplex?

[Yaël Dillies]

Aaah, →₀ is finsupp.

[Yaël Dillies]

Time for me to learn what that does.

[Yury G. Kudryashov]

This is one of the ways to speak about sums indexed by an infinite type.

[Yaël Dillies]

Ah so that's actually a generalization of std_simplex!

[Yury G. Kudryashov]

Basically, we have

• docs#finsupp;
• docs#dfinsupp - a dependent and more computable version;
• docs#finsum;
• docs#finset.sum.

[Yury G. Kudryashov]

Yes.

[Yury G. Kudryashov]

You allow ι to be infinite but require f to be zero outside of a finite set.

[Yaël Dillies]

Unrelatingly, what do you think about defining strict_convex_on/strict_concave_on?

[Yury G. Kudryashov]

I have no time to do this. Feel free to define them.

[Yury G. Kudryashov]

Then you'll get a better version of mean inequalities for free.

[Yaël Dillies]

Will do!

[Yaël Dillies]

#9264 is ready. It takes care of is_extreme and is_exposed.

[Yaël Dillies]

@Scott Morrison, you should have warned me about #9298 :confused:

[Yaël Dillies]

Next up is #9268! It takes care of std_simplex (yes, just as #9298) and finset.center_mass, which I'm renaming to finset.linear_combination. Ultimately, docs#finset.linear_combination and docs#finset.affine_combination will take in docs#finsupp and drop their finset. namespace.

[Yury G. Kudryashov]

We already have linear combinations with finsupp. They're used all over the place in linear_independent

[Yaël Dillies]

Wait, are they defined, or are they used ad hoc? I couldn't find the relevant declaration.

[Yaël Dillies]

What do you think I should do, then?

[Scott Morrison]

Yaël Dillies said:

Scott Morrison, you should have warned me about #9298 :confused:

Sorry about that. I was worried there were other PRs going on but I hadn't been following closely. :-(

[Scott Morrison]

If it's made a mess of a bigger PR we can back it out.

[Yury G. Kudryashov]

docs#linear_independent uses docs#finsupp.total

[Yury G. Kudryashov]

We can bundle it even more into (α → M) →ₗ[R] ((α →₀ R) →ₗ[R] M)

[Yury G. Kudryashov]

For convexity, you actually need the restriction of this map to the standard simplex (which should be defined as {x : α →₀ R | (∀ a, 0 ≤ x a) ∧ x.sum (λ a, id) = 1}.

[Joseph Myers]

I expect you may need to add quite a few definitions / lemmas about finsupp to make manipulations of finsupp as convenient as those of unbundled functions and finset.sum (i.e., so that none of the existing proofs involving affine combinations become any more complicated as a result of using finsupp). I certainly expect a definition of affine_combination using finsupp will turn out to be cleaner in the end, but finsupp seemed harder to use than unbundled functions and finset.sum when I was originally defining affine_combination.

There might be a question of whether affine_combination should use the affine subspace of finsupp where the sum of the weights is 1 (as opposed to using an arbitrary finsupp and a separate hypothesis about the sum of the weights on those lemmas that need it), but that could complicate things and I don't know if it would bring much practical benefit.

[Yaël Dillies]

Scott Morrison said:

If it's made a mess of a bigger PR we can back it out.

No, that's fine. I will just look petty by changing the name of the variable everywhere :rofl:

[Yaël Dillies]

Yury G. Kudryashov said:

docs#linear_independent uses docs#finsupp.total

Okay, so what is supposed to be the point of linear_combination? If it's really just finsupp.total without finsupp, maybe we can drop it altogether?

[Eric Wieser]

Part of the problem I suspect is that finsupp.total is hard to find vs docs#finset.linear_combination which has a clearer name.

[Eric Wieser]

I'm confused, what linear_combination are you even talking about?

[Yaël Dillies]

I renamed docs#finset.center_mass. See #9268

[Yaël Dillies]

Thanks for inadvertently affirming this choice :grinning_face_with_smiling_eyes:

[Yaël Dillies]

Okay so #9356 (convex_on, concave_on is also ready for review. It's independent of #9268 (std_simplex, finset.center_mass/finset.linear_combination) except for Jensen's inequality. If we could just decide what to do with finset.center_mass, this one could go through rather easily.

[Oliver Nash]

I'll take a look at these this afternoon.

[Yaël Dillies]

Thanks!

[Oliver Nash]

@Yaël Dillies I just spent some time looking over #9268 and left this comment.

[Oliver Nash]

I have not looked at #9356 beyond noting that it has a huge diff and technically does depend on #9268. I note that you say that "it's not much work to make it independent". I suggest doing this work as it will make me review it!

[Yaël Dillies]

@Oliver Nash, you have it!

[Yaël Dillies]

It won't compile for the Jensen inequality part. I'll fix that tomorrow morning. The rest won't be affected and can be reviewed already.

[Johan Commelin]

https://github.com/leanprover-community/mathlib/pull/9268#discussion_r715692515 is still an open remark. Are there further comments for #9268 ? Otherwise I think that one should be mergeable soonish.

[Oliver Nash]

For me a resolution of https://github.com/leanprover-community/mathlib/pull/9268#pullrequestreview-763215418 would help decide.

[Oliver Nash]

But I agree, this PR is certainly close.

[Yaël Dillies]

To be honest, I think there are two options now:

• Merge as is and I'll change to using finsupp.total in another PR
• Change everything to use finsupp.total

[Oliver Nash]

What's wrong with writing s.sum (w • p) instead of finset.linear_combination p w everywhere?

[Yaël Dillies]

Missing glue :grimacing:

[Yaël Dillies]

I also think that #9356 should be merged before now that it's been made independent from #9268.

[Oliver Nash]

Yaël Dillies said:

Missing glue :grimacing:

Maybe I'm begin dense but your proposed definition is:

def linear_combination {𝕜 E ι : Type*} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E]
  (s : finset ι) (p : ι → E) (w : ι → 𝕜) : E :=
∑ i in s, w i • p i

Isn't that defeq to s.sum (w • p)?

[Oliver Nash]

Basically we avoided making this definition in the linear algebra part of the library so introducing it here (with restrictive typeclasses) seems wrong to me.

[Yaël Dillies]

Ah wait, you're still having s : finset ι. I thought you meant to switch to finsupp.

[Yaël Dillies]

But what's docs#finsupp.total then?

[Oliver Nash]

The finitely-supported version.

[Yaël Dillies]

Okay so I have branch#std_simplex_finsupp (currently a mess, feel free to help!) to change docs#std_simplex to a set of finsupps, hence relaxing the fintype assumption.

[Oliver Nash]

I should say that even as it stands I think this PR is a net positive so if others want to merge it as it stands, I will support that.

[Yaël Dillies]

And I think that affine_combination and liner_combination shoudl be changed to using finsupp too.

[Oliver Nash]

Scope creep can destroy the best intentions. My 2c is to focus on one thing at a time.

[Yaël Dillies]

Yes sure. So I think the answer here is to merge #9268

[Oliver Nash]

I'm keen to see this merged but question about finset.linear_combination is still unresolved, right?

[Oliver Nash]

I think you'll need to convince someone else to merge it or convince me that it is non-trivial to start writing s.sum (w • p) instead of s.linear_combination p w.

[Yaël Dillies]

I'm fine with dropping finset.linear_combination altogether and use s.sum (w • p). Then we can use finsupp.total when we want to switch to finsupp.

[Oliver Nash]

Right, I see the role of finsupp as completely orthogonal to the concerns of this PR.

[Yaël Dillies]

The space of refactors is of high dimension :upside_down:

[Oliver Nash]

@Yaël Dillies I've just been looking over #9356 and I think it can be merged but I think the title is out of date because you already split out the generalisation of convexity (concavity) of functions.

[Oliver Nash]

Do you feel something along the lines of "reorganise lemmas about convexity (concavity) of functions and generalise Jensen" is about right?

[Yaël Dillies]

What about adding plainly "in lemmas"?

[Oliver Nash]

Go for it!

[Oliver Nash]

I pulled the trigger.

[Yaël Dillies]

Scary!

[Yaël Dillies]

Now that #9356 is merged, I'll clean up #9268 tomorrow and hopefully it is mergeable soon.

[Yaël Dillies]

In parallel (strictly speaking, this isn't part of the refactor), I'll define strict_convex_on and strict_concave_on.

[Yaël Dillies]

Good thing that we split off analysis.convex.function. Strict convex/concave functions are about to inflate the number of line to 1.1k!

[Yaël Dillies]

I've just opened

• #9438 (+194, −137): general cleanup of analysis.convex.function
• #9439 (+18, −6): define strictly convex/concave functions
• #9437 (+531, −123) : provide all the API for strictly convex/concave functions
  The first two are independent and can be merged simultaneously.

[Oliver Nash]

I just noticed that #9356 relaxed some add_comm_group typeclass assumptions to add_comm_monoid. I think we should possibly undo this because these monoids have a scalar action of a ring (in fact a linear_ordered_field) so they're actually groups and so this is not a more general situation and is just a bit more awkward.

[Oliver Nash]

For example:

import algebra.order.field
import algebra.module.basic

variables {R E : Type*} [linear_ordered_field R] [add_comm_monoid E] [module R E]

example : add_comm_group E := module.add_comm_monoid_to_add_comm_group R

[Oliver Nash]

For an example of why this is more awkward note that I had to fix this bors failure with this commit.

[Oliver Nash]

However I claim the right fix is to revert add_comm_monoid E back to add_comm_group E here

[Oliver Nash]

Do I have support to carry out this reversion?

[Yaël Dillies]

Oh okay, as soon as you have ring R... That's interesting.

[Yaël Dillies]

Go for it. It might also simplify the structure of the files.

[Oliver Nash]

Exactly, x - y = x + (-1)•y.

[Oliver Nash]

OK I'll push that fix for this file as part of #9103

[Oliver Nash]

Would you be available to hunt down any other examples of this introduced in #9356?

[Oliver Nash]

Actually I think that was the only instance of this (introduced in #9356) so once #9103 lands all should be well again :tada:

This looks suspicious: https://github.com/leanprover-community/mathlib/pull/9356/files#diff-2c41777d2dc24191912a0713d599feb75a13f1f12ad4978dbba711b15e5d228bR461

[Oliver Nash]

And this https://github.com/leanprover-community/mathlib/pull/9356/files#diff-2c41777d2dc24191912a0713d599feb75a13f1f12ad4978dbba711b15e5d228bR605

[Oliver Nash]

Last one I think: https://github.com/leanprover-community/mathlib/pull/9356/files#diff-2c41777d2dc24191912a0713d599feb75a13f1f12ad4978dbba711b15e5d228bR644

[Oliver Nash]

I should have flagged these in review. Sorry about that.

[Yaël Dillies]

Sorry these links are broken. What did you mean to show me?

[Oliver Nash]

I think they work if you click “Load diff” on the file analysis/convex/function.lean. If you like you can ignore this and I’ll create a PR tomorrow morning!

[Yaël Dillies]

Okay, I'll wait for the PR!

[Yaël Dillies]

Just so you know, this should be an easy fix as I've structured the files according to the instance on 𝕜. So the fix should be as simple as looking for section ordered_ring, section linear_ordered_field, ... and modifying the variables that comes just after.

[Oliver Nash]

Great, that should make it very easy.

[Yaël Dillies]

Or just look for add_comm_monoid E, add_comm_monoid F. Also very easy.

[Scott Morrison]

Would it make sense to put all the material about strictly convex functions in a new file?

[Oliver Nash]

Yaël Dillies said:

Okay, I'll wait for the PR!

I just created #9442 for this. In the end I left the monoids appearing here https://github.com/leanprover-community/mathlib/blob/d7abdff7d5abd82d0fbdf795e2a0766150e06c42/src/analysis/convex/function.lean#L461-L467 unchanged because there is no compatibility between the action of the scalars and the structure on the types E, β (which incidentally suggests to me that there's room for improvement here).

[Yaël Dillies]

Great!

[Yaël Dillies]

The room for improvement you're talking about is replacing add_comm_monoid E by has_zero E,has_add E (and same in the definition of convex), I think.

[Yaël Dillies]

Scott Morrison said:

Would it make sense to put all the material about strictly convex functions in a new file?

I don't think so. The stuff is really similar and all the variants of the same lemma deserve to be a few lines apart. Instead, we could split along other criteria, like Jensen's stuff + maximum principle can earn its own file (albeit it's not many lines).

[Yaël Dillies]

Without Jensen and maximum principle, we're at 993 lines. If we further remove the slope stuff (which is used for convexity from positive second derivative), we get down to 792.

[Yaël Dillies]

For comparison, analysis.convex.basic was 1723 lines long before I started the refactor :scream:

[Yaël Dillies]

Just opened #9444 (+114, −104) and #9445 (+128, −102)! They do exactly the two splits I just proposed.

[Johan Commelin]

Thanks! #9445 currently has merge conflicts.

[Yaël Dillies]

Solved :tools:

[Yaël Dillies]

Does it make sense to move convex_hull to something like analysis.convex.hull?

[Yaël Dillies]

or do we declare that analysis.convex.basic is short enough?

[Johan Commelin]

1066 is of course a very important number, but I don't think it hurts to make that file a bit shorter still. So yes, please split it further.

[Yaël Dillies]

I'm doing convex cones now.

[Oliver Nash]

@Yaël Dillies I was just having a quick look at #9268 again but I see you've marked it WIP (I guess till you fix the build). So I'm going to wait for now unless you'd like more input right now. OK?

[Yaël Dillies]

Yeah, I'm still pondering. Sorry I should have marked it WIP a bit earlier.

[Oliver Nash]

No problem at all! I'll be ready when you are.

[Oliver Nash]

Incidentally I've just created #9499 which will conflict but not much.

[Yaël Dillies]

Oh yeah, maybe merge that before I do anything.

[Oliver Nash]

I'm happy either way, the conflicts will be simple to fix.

[Oliver Nash]

Proving convex_hull_range_eq_exists_affine_combination in #9499 almost convinced me to attempt my own version of #9268 where we nuke center_mass and replace it affine_combination but in the end I decided that can wait.

[Yaël Dillies]

So long as you are there, could you prove the following lemma?

lemma (𝕜 : Type u_1) {E : Type u_2} {ι : Type u_3} [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] (p : ι → E) :
  affine_independent 𝕜 p = ∀ (s : set ι) (x : ι), p x ∈ affine_span 𝕜 (p '' s) → x ∈ s := sorry

[Oliver Nash]

:laughing: Let me see. I'm about to head out for a run but I'll give it a go!

[Yaël Dillies]

This is the definition of docs#convex_independent, but made affine.

[Yaël Dillies]

Once we have it, I can make affine.independent.convex_independent a one-liner!

[Yaël Dillies]

(feel free to change to change the typeclasses, they are probably not the full generality)

[Oliver Nash]

OK I've fired up VSCode and I'll see what I think. Here it is again in MWE form:

import linear_algebra.affine_space.independent

lemma foo (𝕜 E ι : Type*) [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] (p : ι → E) :
  affine_independent 𝕜 p ↔ ∀ (s : set ι) (x : ι), p x ∈ affine_span 𝕜 (p '' s) → x ∈ s :=
begin
  sorry,
end

[Oliver Nash]

Sorry, outatime for now!

[Yaël Dillies]

Here, @Oliver Nash, @Yakov Pechersky

[Yaël Dillies]

What would be your definition of convex space?

[Oliver Nash]

Well, if we decided we could restrict to the case of needing negation I think the following:

[Oliver Nash]

import linear_algebra.affine_space.combination

open_locale affine

variables (k : Type*) {V P : Type*}

variables [ordered_ring k] [add_comm_group V] [module k V] [affine_space V P]
include V

def convex (s : set P) :=
  ∀ ⦃x y : P⦄, x ∈ s → y ∈ s → ∀ ⦃a : k⦄, 0 ≤ a → a ≤ 1 → affine_map.line_map x y a ∈ s

[Yaël Dillies]

No, I meant a convex space :smile:

[Yaël Dillies]

Am I right in thinking there isn't one kind of convex space but a hierarchy of them? Supposedly every kind of scalar action between has_scalar and module gives rise to a different kind of convex space.

[Oliver Nash]

What's a convex space?

[Yaël Dillies]

A space where you can define convexity.

[Yaël Dillies]

I don't have many references. That's the problem. Here's something on ncatlab: https://ncatlab.org/nlab/show/convex+space

[Oliver Nash]

Oh I see.

[Oliver Nash]

So basically it's a space which has line_map.

[Oliver Nash]

Then my definition would be the same!

[Yaël Dillies]

More like a segment_map because you don't care about what's not between the points.

[Oliver Nash]

Right.

[Yaël Dillies]

Do you think we should put convex combinations as a field of convex_space or construct it from segment_map?

[Oliver Nash]

I don't know. My null hypothesis would be to construct it from segment_map but I would not have a strong view here.

[Yury G. Kudryashov]

I think that the main difficulty with convex_space is not to define it and provide instances for an affine_space and a module. The main difficulty is that we unavoidably get a TC diamond for a convex_space real E: the instance going through affine_space can't be defeq to the instance going through module.

[Yury G. Kudryashov]

So, only one of these instances can be a global instance.

[Yury G. Kudryashov]

And more diamonds: probably you want to define a convex_space structure on the product of two spaces etc. If you get the product of two modules (or affine spaces), then probably the segment_map coming from prod won't be defeq to the segment_map coming from module/affine_space.

[Yaël Dillies]

Oh, I hadn't thought about prod. The module instance for prod is well-behaved, right? I know you probably want affine_space -> convex_space to be the global instance instead of module -> convex_space, but I have the instinct that the module -> convex_space instance is cleaner.

[Yury G. Kudryashov]

The best way to verify this is to make a one-field typeclass (just segment_map, no axioms), add instances, and try prove equality by rfl.

[Yaël Dillies]

Will do!