Proving a limit

Stream: new members

[Michał Mrugała]

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]

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

[Michał Mrugała]

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]

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]

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

[Heather Macbeth]

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