## Stream: general

### Topic: convexity

#### Patrick Massot (Dec 20 2022 at 14:16):

@Yaël Dillies in #9058 you generalized the definition of docs#convex to sets in modules over ordered semi-rings. But your definition doesn't seem to ensure that a barycentric combination of elements of a convex set belong to this convex set. Indeed docs#convex.sum_mem assumes scalars form a linearly ordered field (and the obvious proof on paper certainly also requires inverting stuff). Are you sure this is the definition you wanted? If we switch to have docs#convex.sum_mem as the definition (and a lemma saying that over a field it sufficices to check the weak condition), would we loose any convex set you care about?

#### Yaël Dillies (Dec 20 2022 at 14:27):

Yes, you're catching this definition mid-(a long) refactor. My idea was to define convex spaces with a primitive operation convex_combination, which would generalise both semimodules and affine spaces.

#### Patrick Massot (Dec 20 2022 at 15:07):

I see. It would have been nice to finish this because the current definition is probably not usable at all beyond the field case.

#### Patrick Massot (Dec 20 2022 at 15:09):

I'll try to work around that, but this is digging an even deeper rabbit hole than what I hoped two hours ago :sad:

#### Yaël Dillies (Dec 20 2022 at 15:30):

What are your needs? My original goal was to generalise to scalar semifields, which involved generalising to docs#ordered_semiring because docs#linear_ordered_semifield wasn't yet a thing.

#### Yaël Dillies (Dec 20 2022 at 15:30):

Now that it is, I wonder whether we even want the non-semifield case.

#### Anatole Dedecker (Dec 20 2022 at 15:35):

For the record, I just want to add that I may do another convexity refactor at some point if I figure out ways to nicely unify the usual convexity with convexity over non-archimedean fields. But it is not relevant for the current conversation

#### Patrick Massot (Dec 20 2022 at 15:37):

In my use case the ring of scalars is the ring of germs of smooth functions at a point in a manifold.

#### Patrick Massot (Dec 20 2022 at 15:39):

This is subring of docs#filter.germ

#### Patrick Massot (Dec 20 2022 at 15:41):

The ordered ring instance is missing because people who wrote that file were too focused on ultraproducts so we have docs#filter.germ.linear_ordered_comm_ring but not

instance filter.germ.ordered_comm_ring {α : Type*} (l : filter α) (R : Type*) [ordered_comm_ring R] :
ordered_comm_ring (germ l R) :=
rintros ⟨a⟩ ⟨b⟩ hab ⟨c⟩,
end,
zero_le_one :=  eventually_of_forall (λ x, zero_le_one),
mul_nonneg := begin
rintros ⟨a⟩ ⟨b⟩ ha hb,
exact eventually.mono (ha.and hb) (λ x hx, mul_nonneg hx.1 hx.2)
end,
..filter.germ.partial_order,
..(by apply_instance : comm_ring (germ l R))}


#### Patrick Massot (Dec 20 2022 at 17:29):

I have some fun exercise for people with the right kind of masochistic bias:

import analysis.convex.basic

open_locale big_operators
open function

variables (𝕜 : Type*) {E : Type*} [ordered_semiring 𝕜] [add_comm_monoid E]
[has_smul 𝕜 E]

def really_convex_hull (𝕜 : Type*) {E : Type*} [ordered_semiring 𝕜] [add_comm_monoid E]
[has_smul 𝕜 E] (s : set E) : set E :=
{e | ∃ w : E → 𝕜,  0 ≤ w ∧ support w ⊆ s ∧ ∑ᶠ x, w x = 1 ∧ e = ∑ᶠ x, w x • x}

variable {𝕜}

lemma sum_mem_really_convex_hull {s : set E} {ι : Type*} {t : finset ι} {w : ι → 𝕜}
{z : ι → E} (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i = 1) (hz : ∀ i ∈ t, z i ∈ s) :
∑ i in t, w i • z i ∈ really_convex_hull 𝕜 s :=
sorry


#### Patrick Massot (Dec 20 2022 at 17:31):

The proof on paper is: "What do you mean by proof? Is there anything to prove?", which usually means quite a lot of Lean code.

#### Eric Wieser (Dec 20 2022 at 18:02):

Are you proposing that really_convex_hull replace convex_hull?

#### Eric Wieser (Dec 20 2022 at 18:03):

Because if we're going to use up the community pool of masochistic bias, it would be great to have the affine generalization at the same time, assuming they're not incompatible

#### Patrick Massot (Dec 20 2022 at 18:04):

Yes, I propose some version of really_convex_hull should replace convex_hull (and the analogue change for the definition of convex). This wouldn't be enough to get the affine case as far as I can see, but that would make the current version of convex and convex_hull usable beyond the field case.

#### Patrick Massot (Dec 20 2022 at 18:05):

And I think that proving some form of this lemma will be needed to connect any super abstract version of convexity with something usable in the ordered_ring case.

#### Eric Wieser (Dec 20 2022 at 18:06):

I think my point is that if we did the affine case we'd probably have to throw away that definition and pick a different one (maybe in terms of docs#finset.weighted_vsub); so it might be worth solving both problems at once rather than repeating the work

#### Patrick Massot (Dec 20 2022 at 18:07):

What you are describing sounds nice but it is very unlikely to happen in the coming year while I need this lemma now.

#### Eric Wieser (Dec 20 2022 at 18:07):

Mathlib3 now or mathlib4 now?

#### Patrick Massot (Dec 20 2022 at 18:08):

This is in mathlib3.

#### Patrick Massot (Dec 20 2022 at 18:08):

Actually I'm trying to refactor something from the sphere eversion project.

#### Kevin Buzzard (Dec 20 2022 at 19:34):

@Patrick Massot I assume that I can change [has_smul 𝕜 E] to [module 𝕜 E]? Otherwise I can't prove anything about the sum of w x • x.

#### Yaël Dillies (Dec 20 2022 at 19:34):

Patrick Massot said:

In my use case the ring of scalars is the ring of germs of smooth functions at a point in a manifold.

Amazing! I kind of gave up the refactor halfway through because of the lack of need for the extra generality. But if you need it, I'm getting straight back in.

#### Yaël Dillies (Dec 20 2022 at 19:35):

Disclaimer: I'm painting my house for the next two weeks so my Lean time won't be much.

#### Eric Wieser (Dec 20 2022 at 19:36):

@Patrick Massot: does your use-case need semirings, or would rings be fine?

#### Eric Wieser (Dec 20 2022 at 19:38):

(I ask because docs#add_torsor is currently only defined for add_comm_group, and given the choice I'd rather we prioritize a) your use case b) affine spaces c) semirings instead of a) your use case b) semirings c) affine spaces)

#### Johan Commelin (Dec 20 2022 at 19:38):

If it's only the germs of smooth functions that Patrick mentioned above, then I'm pretty sure rings is good enough.

#### Kevin Buzzard (Dec 20 2022 at 19:39):

yeah, Patrick is doing mathematics, so semirings are unlikely to be involved :-) (yes yes I know the naturals are a semiring, but he's a topologist)

#### Kevin Buzzard (Dec 20 2022 at 19:39):

I've reduced it to a lemma which I don't know a good name for, modulo changing has_smul to module:

import analysis.convex.basic

open_locale big_operators
open function

variables (𝕜 : Type*) {E : Type*} [ordered_semiring 𝕜] [add_comm_monoid E]
[module 𝕜 E] -- changed from original question

def really_convex_hull (𝕜 : Type*) {E : Type*} [ordered_semiring 𝕜] [add_comm_monoid E]
[has_smul 𝕜 E] (s : set E) : set E :=
{e | ∃ w : E → 𝕜,  0 ≤ w ∧ support w ⊆ s ∧ ∑ᶠ x, w x = 1 ∧ e = ∑ᶠ x, w x • x}

variable {𝕜}

-- https://xkcd.com/927/
lemma finsum.exists_ne_zero_of_sum_ne_zero {β α : Type*} {s : finset α} {f : α → β}
[add_comm_monoid β] : ∑ᶠ x ∈ s, f x ≠ 0 → (∃ (a : α) (H : a ∈ s), f a ≠ 0) :=
begin
rw finsum_mem_finset_eq_sum,
exact finset.exists_ne_zero_of_sum_ne_zero,
end

lemma foo {α β M : Type*} [add_comm_monoid M] (f : β → α) (s : finset β) [decidable_eq α]
(g : β → M) :
∑ᶠ (x : α), ∑ (y : β) in finset.filter (λ (j : β), f j = x) s, g y = ∑ k in s, g k :=
begin
sorry
end

lemma sum_mem_really_convex_hull {s : set E} {ι : Type*} {t : finset ι} {w : ι → 𝕜}
{z : ι → E} (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i = 1) (hz : ∀ i ∈ t, z i ∈ s) :
∑ i in t, w i • z i ∈ really_convex_hull 𝕜 s :=
begin
classical,
refine ⟨λ e, (∑ᶠ i ∈ t.filter (λ j, z j = e), w i), _, _, _, _⟩,
{ rw pi.le_def,
intro e,
apply finsum_nonneg (λ i, _),
exact finsum_nonneg (λ hi, h₀ _ (finset.mem_of_mem_filter i hi)), },
{ intros e he,
rw mem_support at he,
obtain ⟨a, h, ha⟩ := finsum.exists_ne_zero_of_sum_ne_zero he,
rw finset.mem_filter at h,
rcases h with ⟨h, rfl⟩,
exact hz a h, },
{ rw ← h₁,
simp_rw finsum_mem_finset_eq_sum,
rw foo z _ _, },
{ simp_rw [finsum_mem_finset_eq_sum, finset.sum_smul],
rw ← foo z,
congr',
ext x,
rw finset.sum_congr rfl,
intros y hy,
rw finset.mem_filter at hy,
rw hy.2, },
end


#### Yaël Dillies (Dec 20 2022 at 19:43):

You want docs#finset.sum_eq_zero_iff

#### Kevin Buzzard (Dec 20 2022 at 19:43):

Not for this lemma, right? Oh -- are you responding to Eric?

#### Yaël Dillies (Dec 20 2022 at 19:44):

or rather the of_nonneg version (and you're missing the non-negativity assumption in your lemma)

#### Yaël Dillies (Dec 20 2022 at 19:45):

No no, I'm responding to you. The more API way to state your lemma is sum ... = 0 iff forall ...

#### Kevin Buzzard (Dec 20 2022 at 19:46):

Are you talking about finsum.exists_ne_zero_of_sum_ne_zero? This needs no non-negativity assumptions.

It's not an iff.

#### Yaël Dillies (Dec 20 2022 at 19:47):

Ah sorry my phone wouldn't display the unicode. Then you want the contrapositive of docs#finset.sum_eq_zero

#### Kevin Buzzard (Dec 20 2022 at 19:48):

Oh lol I know exactly that situation, my phone does that too :-/

#### Kevin Buzzard (Dec 20 2022 at 19:56):

import analysis.convex.basic

open_locale big_operators
open function

variables (𝕜 : Type*) {E : Type*} [ordered_semiring 𝕜] [add_comm_monoid E]
[module 𝕜 E] -- note to Patrick: I needed this at some point

def really_convex_hull (𝕜 : Type*) {E : Type*} [ordered_semiring 𝕜] [add_comm_monoid E]
[has_smul 𝕜 E] (s : set E) : set E :=
{e | ∃ w : E → 𝕜,  0 ≤ w ∧ support w ⊆ s ∧ ∑ᶠ x, w x = 1 ∧ e = ∑ᶠ x, w x • x}

variable {𝕜}

-- https://xkcd.com/927/
lemma finsum.exists_ne_zero_of_sum_ne_zero {β α : Type*} {s : finset α} {f : α → β}
[add_comm_monoid β] : ∑ᶠ x ∈ s, f x ≠ 0 → (∃ (a : α) (H : a ∈ s), f a ≠ 0) :=
begin
rw finsum_mem_finset_eq_sum,
exact finset.exists_ne_zero_of_sum_ne_zero,
end

lemma foo {α β M : Type*} [add_comm_monoid M] (f : β → α) (s : finset β) [decidable_eq α]
(g : β → M) :
∑ᶠ (x : α), ∑ (y : β) in finset.filter (λ (j : β), f j = x) s, g y = ∑ k in s, g k :=
begin
rw finsum_eq_finset_sum_of_support_subset _ (show _ ⊆ ↑(s.image f), from _),
{ rw finset.sum_image',
intros,
refl, },
{ intros x hx,
rw mem_support at hx,
obtain ⟨a, h, ha⟩ := finset.exists_ne_zero_of_sum_ne_zero hx,
simp at ⊢ h,
exact ⟨a, h⟩,
},
end

lemma sum_mem_really_convex_hull {s : set E} {ι : Type*} {t : finset ι} {w : ι → 𝕜}
{z : ι → E} (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i = 1) (hz : ∀ i ∈ t, z i ∈ s) :
∑ i in t, w i • z i ∈ really_convex_hull 𝕜 s :=
begin
classical,
refine ⟨λ e, (∑ᶠ i ∈ t.filter (λ j, z j = e), w i), _, _, _, _⟩,
{ rw pi.le_def,
intro e,
apply finsum_nonneg (λ i, _),
exact finsum_nonneg (λ hi, h₀ _ (finset.mem_of_mem_filter i hi)), },
{ intros e he,
rw mem_support at he,
obtain ⟨a, h, ha⟩ := finsum.exists_ne_zero_of_sum_ne_zero he,
rw finset.mem_filter at h,
rcases h with ⟨h, rfl⟩,
exact hz a h, },
{ rw ← h₁,
simp_rw finsum_mem_finset_eq_sum,
rw foo z _ _, },
{ simp_rw [finsum_mem_finset_eq_sum, finset.sum_smul],
rw ← foo z,
congr',
ext x,
rw finset.sum_congr rfl,
intros y hy,
rw finset.mem_filter at hy,
rw hy.2, },
end


@Patrick Massot (note the module change -- is it OK?)

#### Patrick Massot (Dec 20 2022 at 20:35):

Awesome, thank you very much Kevin!

#### Patrick Massot (Dec 20 2022 at 20:36):

Eric Wieser said:

does your use-case need semirings, or would rings be fine?

Rings would be fine.

(deleted)

#### Joseph Myers (Dec 21 2022 at 00:47):

I think we concluded in one of the past discussions that to cover both the semiring/semifield case (more precisely, the case where the module is only an add_comm_monoid not an add_comm_group) and the add_torsor case, while avoiding diamonds, we'd need both the class for abstract affine combination spaces and the class that inherits from both that and add_torsor for a module and asserts that the two affine combination operations are equal. And then ensure that the instances are set up so that modules get the affine combination operation expressed to be defeq to the version expressed as a linear combination in the obvious way (and only propositionally equal, not defeq, to the version derived from the add_torsor instance for the module over itself).

#### Yaël Dillies (Dec 21 2022 at 07:30):

How did we conclude that? Thinking about it yesterday I reached the conclusion that it was enough for affine_space to extend convex_space (and make defaults for the convex_space fields).

#### Yaël Dillies (Dec 21 2022 at 10:04):

I was also wondering: Do we want to base convexity on a type of convex combinations? By that I mean a type of finitely supported nonnegative functions whose sum is 1. This is basically docs#std_simplex.

#### Yaël Dillies (Dec 21 2022 at 10:07):

The advantage is that operations on
this type encode operations on any space without needing us to supply repetitive nonnegativity and sum = 1 obligations.

#### Yaël Dillies (Dec 21 2022 at 10:08):

Oh my, is there some initial object hiding in there?

#### Patrick Massot (Dec 21 2022 at 10:14):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Convexity.20refactor/near/253773652

#### Yaël Dillies (Dec 21 2022 at 10:16):

Yeah I'm not believing Yury's argument anymore. If the affine_space instance contains the convex_space one, everything is still defeq.

#### Yaël Dillies (Dec 21 2022 at 10:18):

The defeq we lose is between the new primitive convex_combination and docs#affine_space.weighted_vsub. This in my opinion is better than losing the defeq with docs#finset.sum. But really I think both are breakable without too much trouble.

#### Joseph Myers (Dec 21 2022 at 13:19):

Affine spaces do not need the ring to be ordered and so should not extend anything involving an order on the ring. They can extend a class that has all affine combinations (with sum of weights 1), but not a class that depends on the ring being ordered. (The first step in any case for setting up abstract affine combination spaces is probably to remove the affine_space notation for add_torsor; the vast bulk of the existing affine space API involves vectors and subtraction and genuinely depends on having a torsor rather than just affine combinations.)

#### Yaël Dillies (Dec 21 2022 at 16:00):

Right, I missed this. And I totally agree that affine_space will mean something different after the refactor and that the rename is basically the first thing we need to do.

Last updated: Aug 03 2023 at 10:10 UTC