Zulip Chat Archive

Stream: maths

Topic: convexity in the sphere eversion project

Yury G. Kudryashov (Jul 18 2023 at 20:34):

Does really_convex in the sphere eversion project differ from docs#Convex ?

Patrick Massot (Jul 18 2023 at 20:36):

Yes it does. It's what convex should be. There are equivalent in the very special case of a module over a field.

Yury G. Kudryashov (Jul 18 2023 at 23:35):

What is a counterexample?

Yury G. Kudryashov (Jul 18 2023 at 23:59):

I see: if we want to prove that w1 * x1 + w2 * x2 + w3 * x3 ∈ s from docs#Convex, then we need division.

Yury G. Kudryashov (Jul 19 2023 at 00:00):

Should I try to migrate Mathlib to the definition with finsum?

Eric Wieser (Jul 19 2023 at 00:23):

For anyone else with no context, the code is here and is

/-- Generalization of `convex` to semirings. We only add the `s = ∅` clause if `𝕜` is trivial. -/
def really_convex (𝕜 : Type*) {E : Type*} [ordered_semiring 𝕜] [add_comm_monoid E]
  [module 𝕜 E] (s : set E) : Prop :=
  s = ∅ ∨ ∀ w : E → 𝕜, 0 ≤ w → support w ⊆ s → ∑ᶠ x, w x = 1 → ∑ᶠ x, w x • x ∈ s

Eric Wieser (Jul 19 2023 at 00:26):

while docs3#convex and docs3#star_convex are

def star_convex : Prop :=
∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s

/-- Convexity of sets. -/
def convex : Prop := ∀ ⦃x : E⦄, x ∈ s → star_convex 𝕜 x s

Yury G. Kudryashov (Jul 19 2023 at 00:42):

Is there a standard name for docs#Convex ?

Yury G. Kudryashov (Jul 19 2023 at 00:46):

Note: I only care about convexity in modules over $\mathbb R_{\ge0}$ (real vector spaces and measures).

Eric Wieser (Jul 19 2023 at 00:47):

Note that @Yaël Dillies had a refactor in mind that would make it work for affine spaces, which I think is a useful generalization

Yury G. Kudryashov (Jul 19 2023 at 00:47):

Without loosing semirings?

Eric Wieser (Jul 19 2023 at 00:48):

I don't know: but I would speculate that more people expect "convex" to be meaninful in an affine sense than for semirings

Eric Wieser (Jul 19 2023 at 00:49):

docs#Finset.affineCombination indeed needs rings

Yury G. Kudryashov (Jul 19 2023 at 00:57):

AFAIR, the plan was to redefine an affine space as a space with affine combinations instead of an add torsor.

Yury G. Kudryashov (Jul 19 2023 at 00:58):

Then we can have both.

Yury G. Kudryashov (Jul 19 2023 at 00:58):

But this is a large refactor.

Patrick Massot (Jul 19 2023 at 07:14):

In the context of the sphere the ring is the ring of real-valued functions (or more precisely germs of real valued functions). This is the relevant ring when using partitions of unity. Convexity of a set with coefficients in this ring ensures that you can create elements of this set using partitions of unity.

Yury G. Kudryashov (Jul 19 2023 at 12:36):

@Patrick Massot Should I replace docs#Convex with ReallyConvex in Mathlib? If yes, then should I save the current definition under some other name?

Patrick Massot (Jul 19 2023 at 12:38):

I'm not sure mathlib4 is already open to such refactors. And then I don't think the current definition should have another name, there should be a lemma saying that, whenever the scalar ring is a field, the current definition (and its many variants) is sufficient to prove convexity.

Patrick Massot (Jul 19 2023 at 12:39):

I don't think there is any use for the current definition when it is not equivalent to really_convex.

Yury G. Kudryashov (Jul 19 2023 at 12:40):

It's not open for refactors yet.

Scott Morrison (Jul 19 2023 at 12:46):

Soon. :-)

Notification Bot (Jul 19 2023 at 12:46):

22 messages were moved here from #maths > porting the sphere eversion project by Eric Wieser.

Last updated: Dec 20 2023 at 11:08 UTC