Sorting and applying

Stream: general

[Yaël Dillies]

I have n naturals a₁, ..., aₙ(not necessarily distinct) and I want to define b₁/1 + ... + bₙ/n where the bs are the as in ascending order. What's the best way to do that? I don't have strong restrictions on the representation of a₁, ..., aₙ, so it can be list ℕ, vector ℕ n, fin n → ℕ...

[Kevin Buzzard]

I'm pretty sure there's something like docs#list.sort

[Kevin Buzzard]

Dammit the community website search doesn't work on my phone

[Adam Topaz]

I think it's docs#list.sorted ?

[Adam Topaz]

Oh no that's the prop. I guess docs#list.merge_sort

[Adam Topaz]

Do we have docs#list.quick_sort ?

[Adam Topaz]

Or docs#list.insertion_sort

[Kevin Buzzard]

They're dupes

[Kevin Buzzard]

Haven't you heard of functional extensionality? ;-)

[Yakov Pechersky]

docs#finset.sort

[Yakov Pechersky]

or, since you have not-necessarily distinct nats, docs#multiset.sort

[Yaël Dillies]

Yeah, or docs#list.merge_sort, but how do I then divide by a different number everytime?

[Yakov Pechersky]

after you sort, list.zip_with (/) (sorted_list) ((list.range _).map _)

[Yaël Dillies]

Is list.zip_with the same as list.map₂?

[Yaël Dillies]

Here's what I tried.

def energy (pos : vector ℕ n) : ℕ :=
list.sum (list.map₂ (λ a b, b/a) (list.range n) (list.merge_sort (≤) pos.1))

but I wonder whether it will unfold nicely.

[Yaël Dillies]

And also, how can I define a constant vector?