feat(Data/Multiset/Order): add Dershowitz-Manna Ordering and Theorem

[haitian-yuki]

add Dershowitz-Manna Ordering and Theorem for Multisets

Co-authored-by: Malvin Gattinger [email protected]

---

• depends on: [Merged by Bors] - feat: Multiset lemmas #15645

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Dershowitz-Manna.20Ordering.20theorem/near/434390710

[github-actions]

PR summary dbd9cbbc82

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Data.Multiset.DershowitzManna (new file)	390

---

Declarations diff

+ IsDershowitzMannaLT
+ IsDershowitzMannaLT.trans
+ instWellFoundedisDershowitzMannaLT
+ wellFounded_isDershowitzMannaLT

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[riccardobrasca]

Can you please mark this PR WIP or awaiting-review? Thanks!

[Rida-Hamadani]

Thank you! Some comments are general and need to be applied in other places in PR (instead of just committing the suggested portions).

[kim-em]

Obviously my review is far from complete, but I'm not an expert here so hopefully someone else will come along, but these will give you something to start with.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: Multiset lemmas #15645
  By Dependent Issues (🤖). Happy coding!

[YaelDillies]

I mean replacing def/lemma by private def/private lemma

[YaelDillies]

I wouldn't mention this since it's private

Suggested change

	- `Multiset.TransLT_eq_isDershowitzMannaLT` : two definitions of the `Dershowitz-Manna ordering`
	are equivalent.

[YaelDillies]

I have just pushed a golf. I am running out of time today, but you should feel free to have a look for yourself at my commit and try golfing further using the tricks you will have learned. 😃

[haitian-yuki]

I have just pushed a golf. I am running out of time today, but you should feel free to have a look for yourself at my commit and try golfing further using the tricks you will have learned. 😃

Hi Thanks for showing some of the golfing tricks;-) @YaelDillies . I tried golfing a little bit more and maybe now it is in a better form. One thing that I am still unsure about is whether I am allowed to use aesop in the proof as long as it doesn't show 'time run out' thing? Is that what you meant by 'so long as performance is not too terrible'? Thanks!

Ah I just saw some checks were not successful and I'm trying to understand what happened to the branch...

[Rida-Hamadani]

To answer the question regarding aesop, you can write #count_heartbeats in 1 line before a lemma to see how much of a difference using aesop changes, relevant scale for heartbeats is 200000.

[YaelDillies]

Can you please merge master to get rid of the obscure CI error?

[haitian-yuki]

Thanks again for another golf @YaelDillies ! I have to say it looks pretty clean to me now and I cannot see much to improve here ;-) Does it mean the PR is done now? Thanks!