Searching for a statement about finset sum of positive terms

Stream: new members

[Ryan Smith]

I tried moogle, leanexplore and even loogle (which is not the most beginner friendly) but I can't find what must be a standard result. I could use help with the specific theorem but also with what did I miss when searching for results?

lemma sum_eq (s : Finset ℂ) (hbd : ∀ z ∈ s, ‖z‖ ≤ 1) (heq : ∑ z ∈ s, ‖z‖ = ∑ _ ∈ s, 1) :
    ∀ z ∈ s, ‖z‖ = 1 :=
  by sorry

[Jireh Loreaux]

@loogle ∑ x ∈ ?s, ?f x = ∑ x ∈ ?s, ?g x

[loogle]

:search: Equiv.Perm.sum_comp, Equiv.Perm.sum_comp', and 58 more

[Weiyi Wang]

I haven't found it yet, but the first step is to realize this lemma can actually be generalized

lemma sum_eq (s : Finset a) (f : a -> b)  (bound : b) (hbd : ∀ z ∈ s, f z ≤ bound)
(heq : ∑ z ∈ s, f z = ∑ _ ∈ s, bound) :
∀ z ∈ s, f z = bound

(pseudo code)

[Jireh Loreaux]

The ~10th hit is: docs#Finset.sum_eq_sum_iff_of_le which is what you want.

[Jireh Loreaux]

I chose this pattern for loogle because it seemed the most specific of the expressions involved, but then I abstracted away the details to get more hits for this pattern.

[Ryan Smith]

Jireh Loreaux said:

loogle ∑ x ∈ ?s, ?f x = ∑ x ∈ ?s, ?g x

That's amazing, you found it?! So when we are searching with loogle I take it ?s is a placeholder and you're just looking for search results where we have equality between two sums over the same set but arbitrary expressions within them to see what it comes up with?

[Jireh Loreaux]

And actually, if you add another expression, you get only one hit: @loogle ∀ x, ?h x ≤ ?j x, ∑ x ∈ ?s, ?f x = ∑ x ∈ ?s, ?g x

[loogle]

:search: Finset.sum_eq_sum_iff_of_le

[Jireh Loreaux]

In the above, morally and in your head h = f and j = g, but it's not necessary in this case to reduce the search space sufficiently.