convex combinations?

Stream: Is there code for X?

[Kim Morrison]

If I have a b : Real, x y : Set.Icc a b, and s : unitInterval, what is the colloquial way to say s * x + (1 - s) * y as a term in Set.Icc a b?

[Shreyas Srinivas]

Is it meaningful to say x y : Set.ICC a b?

[Shreyas Srinivas]

I just checked Icc and it seems to be a Set

[Snir Broshi]

Does this help?

import Mathlib

lemma foo (a b : ℝ) (x y : Set.Icc a b) (s : unitInterval) :
    (1 - s : ℝ) * y + s * x ∈ Set.Icc a b := by
  wlog h : y.val ≤ x.val
  · sorry
  exact Set.Icc_subset _ y.prop x.prop <|
    segment_eq_Icc h ▸ segment_eq_image ℝ y.val x.val ▸ ⟨s.val, s.prop, rfl⟩

[Snir Broshi]

docs#segment_eq_image

[Kim Morrison]

I've written what I need, I'll link here with a PR number when it's up.

[Yaël Dillies]

This would have come for free if the convexity refactor had been done

[Joseph Myers]

I think we need to figure out a way to do the convexity refactor incrementally (define abstract affine combination spaces in mathlib - convex combinations being the case where all the scalars in the semiring are nonnegative - and gradually generalize existing lemmas / definitions to them) rather than expecting to refactor everything in the affine spaces and convexity parts of mathlib at once.

[Kim Morrison]

What is the obstacle to working incrementally?

[Joseph Myers]

I don't know an obstacle, beyond the general principle that it's hard to know if you have a good, usable formal definition until you've set up enough material on the basis of that definition.

[Kim Morrison]

The things I wanted are now in #31525, just in the special case for unitInterval. I hope we can merge something like this, and someone will make it obsolete soon. :-)

[Kim Morrison]

feat: proposed definition of ConvexSpace #31984

[Anatole Dedecker]

Here is a fun thing that just happened to me while thinking about this:

I've had in mind for a while that there should be a further generalization of this which would allow more notions of convexity (I was thinking at the time about the "convexity" in non-archimedean analysis, but it could also be convex cones, ...). Prompted by this PR (and in particular this comment by @Aaron Liu) I decided to write down precisely the axioms that I would impose for my "convexity model" which would be used to define this generalization of convex spaces.

I spent 45 minutes thinking about it and cleaning the axiomatization... and then burst out laughing when I realized I had just landed on the axioms of a monad :sweat_smile:

So I am now almost seriously considering defining "X is a convex space" as "X is an algebra over the Finite Probability Measure/Standard Simplex monad" :grinning_face_with_smiling_eyes:

(This will all sound very normal to people used to monads, but for me it was a lot of fun landing back on this!)

[Kim Morrison]

I just pushed a new definition, which I agree is nicer.

[Kim Morrison]

/--
A set equipped with an operation of finite convex combinations,
where the coefficients must be non-negative and sum to 1.
-/
class ConvexSpace (R : Type u) (M : Type v)
    [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] where
  /-- Take a convex combination with the given probability distribution over points. -/
  convexCombination (f : StdSimplex R M) : M
  /-- Associativity of convex combination (monadic join law). -/
  assoc (f : StdSimplex R (StdSimplex R M)) :
    convexCombination (f.map convexCombination) = convexCombination f.join
  /-- A convex combination of a single point is that point. -/
  single (x : M) : convexCombination (.single x) = x

[Kim Morrison]

@Anatole Dedecker, any further comments on this? Can we proceed?

[Adam Topaz]

(deleted)

[Oliver Nash]

I propose we merge / delegate #31984 (which contains the above definition). If I hear no objections within the next ~12 hours I will do so.

[Jireh Loreaux]

@Oliver Nash the PR description needs updating, as the names no longer match. I'm on mobile so can't do it easily.

[Kim Morrison]

I've updated the description.