I need a generalized version of `tendsto_exp_limit_at_top: "((λy. (1 + x / y) powr y) ⤏ exp x) at_top"`

, where a constant `c`

is added to the denominator (I actually only need the case `c=1`

, but I figured might as well):

```
lemma "((λy. (1 + x / (y+c)) powr y) ⤏ exp x) at_top"
```

Is anyone aware if such a lemma already exists? Or can someone give me pointers on how to prove it myself? I tried to look into the proof for the original lemma (to be specific into `tendsto_exp_limit_at_right`

), but to my understanding that depends on the fact that we have a nice derivative at 0 there, which doesn't work in the general case.

Your goal as stated does not restrict the types of `x,y,...`

to `real`

. If you add this constraint (as present in the original tendsto_exp_limit_at_top), Manuel Eberl's `real_asymp`

method (in `HOL-Real_Asymp.Real_Asymp`

) can solve the goal automatically.

Just through `real_asymp`

at everything you have and ask me if you run into any problems.

There's documentation as well in `~~/src/HOL/Real_Asymp/Manual/`

.

Ah, nice. I had the type constraint in the lemma, just forgot to copy it. But thanks a lot for the pointer to `real_asymp`

, it works a treat!

If you publish a paper on whatever it is you're doing, please consider citing this article if it `real_asymp`

ends up being useful: https://doi.org/10.1145/3326229.3326240

Last updated: Dec 07 2023 at 08:19 UTC