Stream: General

Topic: Generalizing exp limit


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Manuel Eberl (May 23 2022 at 13:46):

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

view this post on Zulip 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!

view this post on Zulip 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: Mar 28 2024 at 20:16 UTC