## Stream: General

### Topic: Generalizing exp limit

#### Christoph Madlener (May 23 2022 at 12:32):

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.

#### Simon Roßkopf (May 23 2022 at 12:50):

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.

#### Manuel Eberl (May 23 2022 at 13:45):

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

#### Manuel Eberl (May 23 2022 at 13:46):

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

#### Christoph Madlener (May 23 2022 at 14:19):

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!

#### Manuel Eberl (May 23 2022 at 14:32):

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