convexity

Stream: general

[Patrick Massot]

@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]

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.

[Eric Wieser]

The older thread is here

[Patrick Massot]

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]

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]

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]

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

[Anatole Dedecker]

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]

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

[Patrick Massot]

This is subring of docs#filter.germ

[Patrick Massot]

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) :=
{ add_le_add_left := begin
    rintros ⟨a⟩ ⟨b⟩ hab ⟨c⟩,
    exact eventually.mono hab (λ x hx, add_le_add_left hx _),
  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]

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]

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]

Are you proposing that really_convex_hull replace convex_hull?

[Eric Wieser]

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]

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]

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]

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]

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]

Mathlib3 now or mathlib4 now?

[Patrick Massot]

This is in mathlib3.

[Patrick Massot]

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

[Kevin Buzzard]

@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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

(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]

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

[Kevin Buzzard]

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]

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]

You want docs#finset.sum_eq_zero_iff

[Kevin Buzzard]

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

[Yaël Dillies]

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

[Yaël Dillies]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

It's not an iff.

[Yaël Dillies]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Awesome, thank you very much Kevin!

[Patrick Massot]

Eric Wieser said:

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

Rings would be fine.

[Patrick Massot]

(deleted)

[Joseph Myers]

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]

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]

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]

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]

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

[Patrick Massot]

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

[Yaël Dillies]

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]

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]

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]

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.