Multiset.sum_lt_sum

Stream: Is there code for X?

[Martin Dvořák]

We have List.sum_lt_sum for lists. Do we have a similar thing for multisets?

import Mathlib

variable {ι M : Type} [AddCommMonoid M] [LinearOrder M]
    [CovariantClass M M (· + ·) (· ≤ ·)]
    [CovariantClass M M (· + ·) (· < ·)]

example {l : List ι} (f g : ι → M)
    (h₁ : ∀ i ∈ l, f i ≤ g i) (h₂ : ∃ i ∈ l, f i < g i) :
  List.sum (List.map f l) < List.sum (List.map g l) :=
List.sum_lt_sum f g h₁ h₂

example {s : Multiset ι} (f g : ι → M)
    (h₁ : ∀ i ∈ s, f i ≤ g i) (h₂ : ∃ i ∈ s, f i < g i) :
  Multiset.sum (Multiset.map f s) < Multiset.sum (Multiset.map g s) :=
sorry

[Alex J. Best]

I think with loogle we can be fairly confident the answer is no https://loogle.lean-lang.org/?q=Multiset.sum%2C+LT.lt

[Martin Dvořák]

Is there a straightforward way to translate the List version to the Multiset version?

[Junyan Xu]

rcases s?

[Notification Bot]

Martin Dvořák has marked this topic as resolved.

[Notification Bot]

Martin Dvořák has marked this topic as unresolved.

[Martin Dvořák]

I just noticed that the Finset.prod_lt_prod' assumes OrderedCancelCommMonoid whereäs the List.prod_lt_prod' assumes [CovariantClass M M (· * ·) (· ≤ ·)] and [CovariantClass M M (Function.swap (· * ·)) (· < ·)] instead. Similar situation for Finset.sum_lt_sum and List.sum_lt_sum respectively.

I think we should first unify the assumptions and then create the Multiset version.

[Yaël Dillies]

You should use OrderedCancelCommMonoid in both cases.

[Martin Dvořák]

I think this is asking for a major refactor of
https://github.com/leanprover-community/mathlib4/blob/baa7aa8c9b30292fb7aa93b5724d0c2ea7c1948b/Mathlib/Data/List/BigOperators/Basic.lean#L267
(until line 377).

[Eric Wieser]

It might be worth checking the mathlib3 history to see if the extra generality was deliberate

[Martin Dvořák]

https://github.com/leanprover-community/mathlib/commits/master/src/data/list/big_operators/basic.lean

[Martin Dvořák]

At least some of them were added in this commit:
https://github.com/leanprover-community/mathlib/commit/2541387ecc6183f4d40a3ff6d059c5dfbdbd5192

[Martin Dvořák]

Now that #8170 has been merged, I would like to refactor the List big-operator lemmas:
https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/List/BigOperators/Basic.lean#L267
Can somebody please confirm that there was no good reason for using CovariantClass instead of our algebraic-hierarchy classes?

[Scott Morrison]

Lemmas are often usefully more general when stated in terms of CovariantClass?

[Martin Dvořák]

Seems @Yaël Dillies and @Scott Morrison have a disagreement.

[Yaël Dillies]

Here I doubt it ever was useful. We're not caring about non-commutative ordered stuff.

[Yaël Dillies]

Certainly it doesn't cost much to leave the lemmas as they are.

[Martin Dvořák]

Martin Dvořák said:

I just noticed that the Finset.prod_lt_prod' assumes OrderedCancelCommMonoid whereäs the List.prod_lt_prod' assumes [CovariantClass M M (· * ·) (· ≤ ·)] and [CovariantClass M M (Function.swap (· * ·)) (· < ·)] instead. Similar situation for Finset.sum_lt_sum and List.sum_lt_sum respectively.

I think we should first unify the assumptions and then create the Multiset version.

As they are?

[Eric Wieser]

Yaël Dillies said:

Here I doubt it ever was useful. We're not caring about non-commutative ordered stuff.

Here's one we should care about: the quaternions under the order induced by the difference of the real part when the imaginary parts agree (aka a docs#StarOrderedRing)

[Eric Wieser]

Though maybe it has no relevant properties here

[Yaël Dillies]

@Martin Dvořák, one reason the assumptions between the List and Finset versions are different is because Finset.sum requires commutativity while List.sum doesn't.

[Martin Dvořák]

Got it.
However, you claimed that I should use OrderedCancelCommMonoid in both cases.
Do you no longer have this opinion?
Either way, for the Multiset version, I will use the same setting as the Finset version has.

[Martin Dvořák]

Can we make a decision? Should the big-operator lemmas for List stay as they are?

[Martin Dvořák]

#8707