Christoph Madlener (May 23 2022 at 12:32): 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: Nov 18 2025 at 16:30 UTC