Commit 2026-03-10 20:55 b3fb4dfd

feat(Analysis): Eliminate a hypothesis on IsTheta.rpow (#36084) A strengthened version of IsTheta.rpow: if $f$ and $g$ are eventually nonnegative functions with $f = \Theta(g)$ and $r \in \mathbb{R}$, then $f^r = \Theta(g^r)$. The previous version had a hypothesis that $r \geq 0$. The present version proves by splitting into two cases; in the case $r < 0$, the lower and upper bounds must be used in reverse order. Since IsTheta.rpow is not used elsewhere in Mathlib, this should be an easy one to merge. (Claude AI was used to help in the golfing.)