Zulip Chat Archive

Stream: new members

Topic: Proving a limit


Michał Mrugała (Sep 29 2022 at 13:55):

Hello everyone,
I'm having trouble finding the relevant lemmas in mathlib to prove the following limit:

example {c : } (hc : 0 < c) : filter.tendsto (λ n : , (1 + (n : )*c)^(1 / (n : ))) filter.at_top (nhds 1) := sorry

I've previously proven:

example {N : } (hN : 0 < N) : filter.tendsto (λ n : , N ^ (1 / (n : ))) filter.at_top (nhds 1) := sorry

Would anyone have an idea for how to deal with this?

Filippo A. E. Nuccio (Sep 29 2022 at 13:59):

Have you tried combining docs#filter.tendsto.const_add and docs#filter.tendsto.mul_const ?

Michał Mrugała (Sep 29 2022 at 14:03):

I can't see how these two lemmas would be helpful in this case, since addition and multiplication happens before introducing the exponent.

Filippo A. E. Nuccio (Sep 29 2022 at 14:11):

Ah, sorry, I have not seen you also had an exponent. Does docs#filter.tendsto.of_tendsto_comp help, together with the above two?

Michał Mrugała (Sep 29 2022 at 14:20):

I'd be surprised, since the expression we're applying the exponent to diverges.

Heather Macbeth (Sep 29 2022 at 14:26):

You can probably use docs#tendsto_rpow_div_mul_add composed with the continuity of a linear function and the nat-to-real coercion.


Last updated: Dec 20 2023 at 11:08 UTC