review request: #12120 (new theorems about Real.rpow)

Stream: PR reviews

[Casavaca]

Could someone review #12120?

[Jireh Loreaux]

Reviewed. Here's an easy way to find the first two lemmas I mentioned:

@loogle Finset.sum, Finset.prod, HPow.hPow, Real

[loogle]

:search: Real.rpow_sum_of_pos, Real.rpow_sum_of_nonneg, and 9 more

[Jireh Loreaux]

And docs#Real.finset_prod_rpow is the fifth hit in:

@loogle Finset.prod, HPow.hPow, Real

[loogle]

:search: Real.rpow_sum_of_pos, Real.rpow_sum_of_nonneg, and 32 more

[Jireh Loreaux]

and checking the results of the following shows that we don't have the second lemma included in your PR:

@loogle Finset.prod, HPow.hPow, Real, HDiv.hDiv

[loogle]

:search: Real.geom_mean_le_arith_mean, integral_sin_pow_even, and 4 more

[Casavaca]

@Jireh Loreaux You are right. I'll close this PR. I need to become better on my searching skills.

[Jireh Loreaux]

@Casavaca The div version is reasonable to have.

[Casavaca]

Cool, I'll open another PR.

[Jireh Loreaux]

For future reference, you didn't need to close that one and create a new one. You could instead just update the old one. Note: even if you already closed it, you can just reopen the PR.

[Casavaca]

Got it. Let me make some modifications. I'll reopen it.