A version of add_le_add for indexed sums

Stream: new members

[Ryan Smith]

I have been trying to find this result with leanexplore and moogle but without luck:

I have a finite set s of complex numbers and for each z \in s I have an inequality |z| \le |w|. Isn't there a version of add_le_add for an indexed sum?

∑ z ∈ s, ‖z‖ \le ∑ z ∈ s, ‖w‖

[Eric Wieser]

@loogle "sum_le_sum"

[loogle]

:search: List.Forall₂.sum_le_sum, List.sum_le_sum, and 22 more

[Eric Wieser]

From that list, docs#Finset.sum_le_sum is what you want

[Eric Wieser]

A better query would have been

@loogle: ∑ z ∈ ?s, _ ≤ ∑ z ∈ ?s, _

[loogle]

:search: Finset.sum_le_sum, Finset.exists_le_of_sum_le, and 19 more

[Ryan Smith]

Thanks, I need to get comfortable with loogle since it seems quite powerful for finding results.