[Merged by Bors] - feat(analysis/special_functions/pow): tendsto rpow lemma for ennreals #11475
Conversation
JasonKYi
commented
Jan 15, 2022
JasonKYi
commented
JasonKYi
added
awaiting-review
| @@ -1583,6 +1583,11 @@ begin | |||
| exact ennreal.continuous_inv.continuous_at.comp (continuous_at_rpow_const_of_pos z_pos) } | |||
| end | |||
|
|
|||
| protected lemma tendsto.rpow {α : Type*} {f : filter α} {m : α → ℝ≥0∞} {a : ℝ≥0∞} (r : ℝ) | |||
There was a problem hiding this comment.
I see we already have:
filter.tendsto.cpowfilter.tendsto.rpowfilter.tendsto.nnrpowfilter.tendsto.const_cpowfilter.tendsto.rpow_const
Based on this I think we should:
- Rename
filter.tendsto.const_cpowtofilter.tendsto.cpow_const - Call this lemma
filter.tendsto.ennrpow_constrather than the proposedennreal.tendsto.rpow - Add an appropriate lemma named
filter.tendsto.ennrpow
There was a problem hiding this comment.
I don't quite understand why we should change filter.tendsto.const_cpow to filter.tendsto.cpow_const since the lemma is about taking a constant to the power of a function
There was a problem hiding this comment.
Oops you're right; we definitely should not be renaming filter.tendsto.const_cpow.
However it still seems like filter.tendsto.ennrpow_const would be a more consistent name for the new lemma, even bearing in mind that it mixes types by raising an ennreal-valued function to a real.
There was a problem hiding this comment.
I will change the name to what you suggested. I tried to prove filter.tendsto.ennrpow but it seems that we are missing a few continuity lemmas. That should probably belong in another PR.
ocfnash
added
awaiting-author
|
bors d+ |
|
✌️ JasonKYi can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
the
delegated
|
bors r+ |
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
