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
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.
real_asymp at everything you have and ask me if you run into any problems.
There's documentation as well in
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