Convexity refactor

Stream: mathlib4

[Patrick Massot]

Yaël Dillies said:

I specifically want to explain non-top folders as well. The folders I'm thinking of are typically LinearAlgebra.AffineSpace vs Analysis.Convex. In that case, I'm actually planning on creating a third folder Geometry.Convex and develop the theory of convex spaces axiomatically there, until my refactor is far enough along that this new folder can act as a drop-in replacement for most of Analysis.Convex (where the complement of "most" is the theory of real and complex convex spaces).

Will that include convexity in modules over rings which are not division rings?

[Yaël Dillies]

The hope is "yes". However that means we will need to ungeneralise a bunch of lemmas from (semi)rings to (semi)fields and things like Jensen's theorem will become tautological.

[Patrick Massot]

Nothing becomes tautological, but some things will move to instances instead of lemmas I guess.

[Yaël Dillies]

Well, "Jensen's lemma" won't be a lemma proving that the average of a convex function is less than the average, but a lemma proving that a "binarily convex" function (our current convex) is convex.

[Yaël Dillies]

In fact, I wonder whether we should keep our theory of binary convexity around. On one hand, it's much simpler. On the other hand, it's equal to the general convexity in all cases we care about (citation needed).

[Yaël Dillies]

Thoughts, Patrick?

[Patrick Massot]

I don't this on paper, but what I needed in the sphere eversion project is in this file.

[Yaël Dillies]

The issue with trying to support non-fields is that I can't state any satisfactory associativity axiom.

[Patrick Massot]

The definition in SE is good enough for me.

[Yaël Dillies]

What is it?

[Patrick Massot]

I linked to it.

[Patrick Massot]

https://github.com/leanprover-community/sphere-eversion/blob/master/src/to_mathlib/analysis/convex/basic.lean#L122-L125

[Yaël Dillies]

That's a definition of convexity, not of convex spaces?

[Yaël Dillies]

The associativity axioms I can find are (for $c_\lambda(x, y)$ corresponding to $\lambda y + (1 - \lambda)x$, and $c_{\alpha, \beta}(x, y)$ to $\frac\alpha{\alpha+\beta} x + \frac\beta{\alpha+\beta}y$):

• Wikipedia: $c_\lambda(x,c_\mu(y,z))=c_{\lambda\mu}\left(c_{\frac{\lambda(1-\mu)}{1-\lambda\mu}}(x,y),z\right)$
• Neumann: $c_\lambda(c_\mu(x,y),c_\nu(x,z))=c_\eta\left(x, c_{\frac{\lambda\mu}\eta}(y,z)\right)$ where $\eta = (1 - \lambda)\mu + \lambda\nu$
• Stone: $c_{\alpha+\beta, \gamma}(c_{\alpha, \beta}(x, y), z) = c_{\gamma+\beta, \alpha}(c_{\gamma, \beta}(z, y), x)$
• Fritz: $c_\lambda(c_\mu(x, y), z) = c_{\tilde\lambda}(x, c_{\tilde\mu}(y, z))$ where $\tilde\lambda = \lambda\mu, \tilde\mu = \frac{\lambda(1 - \mu)}{1 - \lambda\mu}$

[Yaël Dillies]

None of these satisfy all our requirement to work without division.

[Yaël Dillies]

Because we want to work without division, we need the finitary version of the combination operator as a primitive. We may also have the binary one for convenience of defeq.

[Yaël Dillies]

And to be clear, I really don't want to do two convexity refactors (or rather three, given that I already did a big one two years ago): I will not generalise the definition of Convex for it to be upturned again in a few months. I would rather start everything from scratch only once.

[Yaël Dillies]

I will take the opportunity to ungeneralise a bunch of convexity results from SMul to Module. Everything we care about really is a module, and I should not have overgeneralised them in the first place two years ago.

[Yaël Dillies]

@Yury G. Kudryashov (sorry for the ping if grading is not done yet), what do you think of fixing the Module → ConvexSpace vs AddTorsor → ConvexSpace diamond by

1. Making Module 𝕜 E → ConvexSpace 𝕜 E an instance
2. Defining a mixin ConvexTorsor [AddTorsor 𝕜 E] [ConvexSpace 𝕜 E] : Prop stating that the convexity agrees with the affine structure

[Eric Wieser]

Yaël Dillies said:

And to be clear, I really don't want to do two convexity refactors (or rather three, given that I already did a big one two years ago): I will not generalise the definition of Convex for it to be upturned again in a few months. I would rather start everything from scratch only once.

I understand you personally not wanting to do this, but it might still be a good use of someone else's time; if an intermediate refactor is still "wrong" but is enough to unblock SE and some other people's projects, it might be worth paying the cost of churn to have it sooner

[Yaël Dillies]

(aaah, SE means Sphere Eversion, not Stack Exchange :bulb:)

[Yaël Dillies]

Yeah sure, it's just that I am currently in one of the most intensive maths masters in the world and don't have time to perform this intermediate (and short-lived) refactor.

[Eric Wieser]

Does docs#ConvexSpace currently exist? What are you actually referring to?

[Yaël Dillies]

No it doesn't. The plan of the refactor is to define it as an axiomatic description of convex sets types, redevelop most of the theory of convexity in that setting, and then move everything to the new setup all at once.

[Yaël Dillies]

My point here is that convexity notions have been developed in mathlib in a random order, and I need to make primitive a bunch of definitions that are currently derived. Hence any attempt at refactoring in place will result in huge (and overlapping across PRs) diffs.

[Jireh Loreaux]

Yaël, what are you claiming is wrong with the really_convex notion from SE?

[Eric Wieser]

I think @Yaël Dillies needs generalized interpolation elsewhere

[Eric Wieser]

And that once we have that, then the "correct" definition of convex is "closed under generalized interpolation"

[Jireh Loreaux]

I understand that, I guess I meant with really_convex adapted to a type. I don't see where division is necessary.

[Yaël Dillies]

It's not wrong, but you can't just replace Convex by ReallyConvex. You will also have to instantly ungeneralise a bunch of results from OrderedRing to LinearOrderedField before my refactor comes by and regeneralises (most of) them.

[Eric Wieser]

Do you have a prototype of ConvexSpace without the associativity?

[Yaël Dillies]

Let me fetch that quick

[Eric Wieser]

It would be good to create a tracking issue for this, and list the motivations there

[Yaël Dillies]

Jireh Loreaux said:

I don't see where division is necessary.

The problem happens when you try to talk about more than two points. You can't write a • x + b • y + c • z as a binary combination of binary combinations unless you can divide by eg a + b to make that (a + b) • ((a/(a + b)) • x + (b/(a + b)) • y) + c • z.

[Yury G. Kudryashov]

I've just finished grading this exam. I like the "mixin" idea. I didn't think about all possible diamonds yet. What instances do you suggest? BTW, do you plan to work over a ring or a semiring? In the latter case we can speak about, e.g., convexity of sets of measures.

[Yury G. Kudryashov]

E.g., the set of measures invariant under a given map is convex.

[Yaël Dillies]

Yeah I remember this example. Over a semifield was my original target (hence my original idea of just using a binary operation) but Patrick's example shows we should aim for semiring instead.

[Eric Wieser]

Does this work for associativity?

import Mathlib.Algebra.Module.Basic
import Mathlib.Data.Finset.Basic

class ConvexSpace (R M) [Semiring R] [AddCommMonoid M] [Module R M] where
  interp (s : Multiset (R × M)) : M
  interp_assoc (ss : Multiset (R × Multiset (R × M))) :
    interp (ss.map fun s => (s.1, interp s.2)) =
      interp (ss.bind fun rs => rs.2.map <| Prod.map (· * rs.1) id)

[Yaël Dillies]

Here's my definition without associativity:

import Mathlib.Algebra.IndicatorFunction

open Function Set
open scoped BigOperators

variable (𝕜 E : Type*) [OrderedSemiring 𝕜] [AddCommMonoid E] [DecidableEq E] [Module 𝕜 E]

namespace Convexity

structure ConvexSpace :=
  protected convexCombo : (E → 𝕜) → Finset E → E
  protected segmentMap : 𝕜 → 𝕜 → E → E → E
  protected convexCombo_singleton (w : E → 𝕜) (x : E) (hw : w x = 1) : convexCombo w {x} = x
  protected segmentMap_eq_convexCombo (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1)
    (x y : E) : segmentMap a b x y = convexCombo (indicator {x} (const _ a)) {x, y}

[Jireh Loreaux]

But Yaël, isn't it just a fact of life that iterative applications of binary convexity may not yield all convex (finite index set) combinations? For example if you work over ℤ[1/3] and you take your convex space to be the one generatd by ℤ³ in ℚ³, then (1/3, 1/3, 1/3) lies in this space, but (I think) you can't get this from repeated applications of binary convexity to points in ℤ³.

[Jireh Loreaux]

(I could be wrong, I haven't thought about it very deeply.)

[Eric Wieser]

I think that's sort of the point; and the claim is that only the finite-index case is interesting, not the binary one

[Yaël Dillies]

Uh, isn't it just 2/3 • 0 + 1/3 • 1?

[Jireh Loreaux]

Switch ℤ to ℕ+ everywhere :wink:

[Yaël Dillies]

Yaël Dillies said:

Here's my definition without associativity:
...

(aside: isn't it bad that import Mathlib.Algebra.IndicatorFunction is enough to define this?)

[Eric Wieser]

I think your version with the indexed family is going to be more annoying to state associativity for than my version with multisets

[Eric Wieser]

Because you need to deal with when an element of the module appears multiple times in the expression

[Jireh Loreaux]

This was somehow the message I failed to read which made me confused (because I didn't read it):
Yaël Dillies said:

The issue with trying to support non-fields is that I can't state any satisfactory associativity axiom.

[Mario Carneiro]

By the way there is a simple cheat you can use to eliminate the divisions: make all the coefficients on the RHS variables too and take a hypothesis which asserts that the new coefficients and the old coefficients are in some relation (for which you can clear denominators)

[Anatole Dedecker]

IIRC the answer is no but let me check: this proposed convexity refactor won't allow us to unify covexity with nonarchimedean convexity, right?

[Yaël Dillies]

Damn I didn't know there was a third generalisation of convexity to care about :rofl:

[Eric Wieser]

The answer to the question in the second half of that message

[Yaël Dillies]

My brain interpreted that colon as a period. Edited.

[Eric Wieser]

Should we be writing this for the affine case rather than for modules?

[Yaël Dillies]

I genuinely can't parse your message, Eric. What's "this"? Too many things were talked about here.

[Yaël Dillies]

Anatole Dedecker said:

this proposed convexity refactor won't allow us to unify convexity with nonarchimedean convexity, right?

I think it actually can? I don't know much about valuation rings (where does one learn about them?) but if my understanding is correct, then $ℝ$ with the usual valuation has $𝒪 = [0, 1]$. Then it's a matter of hiding ValuationRing.ValueGroup deep inside the API.

The only thing I'm unsure of is that docs#ValuationRing currently requires CommRing R. Is it mathematically necessary or just mathematically convenient?

[Yaël Dillies]

At any rate, if the generalisation to valuation rings is actually a generalisation, then it can be performed at a later time with not too much hassle.

[Kevin Buzzard]

Valuation rings were probably developed as part of the perfectoid project and back then we were firmly focussed on commutative algebra. They're certainly an important tool in comm alg and alg geom where commutativity is everywhere but I don't know about the noncommutative case, we were just formalising what we needed for adic spaces.

[Yaël Dillies]

Just to make clear, I don't think we care about convexity over non-commutative rings (please no one interject :pray:). However we do care about convexity over semirings, as Yury's example shows.

[Antoine Chambert-Loir]

Well, there are people studying orders in quaternion algebras over p-adic fields…

[Eric Wieser]

Yaël Dillies said:

I genuinely can't parse your message, Eric. What's "this"? Too many things were talked about here.

Convex spaces.

[Yaël Dillies]

The problem with affine spaces is that they require a negation. We're trying to avoid that here.

[Eric Wieser]

Where does your structure above actually use the module structure?

[Eric Wieser]

I don't see any uses of assumptions on E

[Yaël Dillies]

Sorry, it doesn't of course: I'm trying to generalise away from modules!

[Patrick Massot]

I didn't follow everything but certainly affine spaces over real numbers should be included in this convexity thing. They are a lot less exotic than many other things mentioned here.

[Jireh Loreaux]

Yaël, there is a notion of noncommutative convexity, but it is sufficiently different that we shouldn't try to unify them.

[Yaël Dillies]

Don't worry, Patrick, affine spaces will be covered.

[Yaël Dillies]

@Anatole Dedecker said:

IIRC the answer is no but let me check: this proposed convexity refactor won't allow us to unify convexity with nonarchimedean convexity, right?

Thinking about it more, I highly doubt so: Consider Proposition 2.6 of this paper:

Any set closed under (non-archimedean) 3-element combinations is (non-archimedean) convex

I am pretty sure the corresponding theorem for eg ℕ-convexity is just not true.