Minkowski sums

Stream: Is there code for X?

[Nick Decroos]

Is there already code for taking Minkowski sums of a finite collection of sets? I am looking for this, since I am working on the Shapley-Folkman lemma.

If there isn't, maybe this is something to add in mathlib4.

There is Mathlib/Analysis/Convex/Hull.lean, and convex hulls can be related to Minkowski addition, but I don't see Minkowski addition directly defined there (maybe I need to look better).

Maybe it is interesting to prove that the operations of Minkowski summation and of forming convex hulls are commuting operations. If this isn't already in Lean4, this seems to me like an interesting little project I'd like to work on.

[Nick Decroos]

(deleted)

[Daniel Weber]

There's docs#Finset.add (or docs#Set.add if your sets themselves aren't Finsets), and I believe you should be able to use the usual docs#Finset.sum notation for this

[Yaël Dillies]

Nick Decroos said:

Maybe it is interesting to prove that the operations of Minkowski summation and of forming convex hulls are commuting operations

This is docs#convexHull_add

[Yaël Dillies]

In general, Minkowski sums and products are available once you open scoped Pointwise